[GOAL]
ι : Type u_1
R : Type u_2
R₂ : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R₂ M₂
inst✝³ : TopologicalSpace M
inst✝² : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝¹ : RingHomInvPair σ σ'
inst✝ : RingHomInvPair σ' σ
f : ι → M
φ : M →SL[σ] M₂
x : M
hf : HasSum f x
⊢ HasSum (fun b => ↑φ (f b)) (↑φ x)
[PROOFSTEP]
simpa only using hf.map φ.toLinearMap.toAddMonoidHom φ.continuous
[GOAL]
ι : Type u_1
R : Type u_2
R₂ : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R₂ M₂
inst✝³ : TopologicalSpace M
inst✝² : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝¹ : RingHomInvPair σ σ'
inst✝ : RingHomInvPair σ' σ
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
h : HasSum (fun b => ↑e (f b)) y
⊢ HasSum f (↑(ContinuousLinearEquiv.symm e) y)
[PROOFSTEP]
simpa only [e.symm.coe_coe, e.symm_apply_apply] using h.mapL (e.symm : M₂ →SL[σ'] M)
[GOAL]
ι : Type u_1
R : Type u_2
R₂ : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R₂ M₂
inst✝³ : TopologicalSpace M
inst✝² : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝¹ : RingHomInvPair σ σ'
inst✝ : RingHomInvPair σ' σ
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
h : HasSum f (↑(ContinuousLinearEquiv.symm e) y)
⊢ HasSum (fun b => ↑e (f b)) y
[PROOFSTEP]
simpa only [e.coe_coe, e.apply_symm_apply] using (e : M →SL[σ] M₂).hasSum h
[GOAL]
ι : Type u_1
R : Type u_2
R₂ : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R₂ M₂
inst✝³ : TopologicalSpace M
inst✝² : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝¹ : RingHomInvPair σ σ'
inst✝ : RingHomInvPair σ' σ
f : ι → M
e : M ≃SL[σ] M₂
x : M
⊢ HasSum (fun b => ↑e (f b)) (↑e x) ↔ HasSum f x
[PROOFSTEP]
rw [e.hasSum, ContinuousLinearEquiv.symm_apply_apply]
[GOAL]
ι : Type u_1
R : Type u_2
R₂ : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
⊢ ∑' (z : ι), ↑e (f z) = y ↔ ∑' (z : ι), f z = ↑(ContinuousLinearEquiv.symm e) y
[PROOFSTEP]
by_cases hf : Summable f
[GOAL]
case pos
ι : Type u_1
R : Type u_2
R₂ : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : Summable f
⊢ ∑' (z : ι), ↑e (f z) = y ↔ ∑' (z : ι), f z = ↑(ContinuousLinearEquiv.symm e) y
[PROOFSTEP]
exact
  ⟨fun h => (e.hasSum.mp ((e.summable.mpr hf).hasSum_iff.mpr h)).tsum_eq, fun h =>
    (e.hasSum.mpr (hf.hasSum_iff.mpr h)).tsum_eq⟩
[GOAL]
case neg
ι : Type u_1
R : Type u_2
R₂ : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f
⊢ ∑' (z : ι), ↑e (f z) = y ↔ ∑' (z : ι), f z = ↑(ContinuousLinearEquiv.symm e) y
[PROOFSTEP]
have hf' : ¬Summable fun z => e (f z) := fun h => hf (e.summable.mp h)
[GOAL]
case neg
ι : Type u_1
R : Type u_2
R₂ : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f
hf' : ¬Summable fun z => ↑e (f z)
⊢ ∑' (z : ι), ↑e (f z) = y ↔ ∑' (z : ι), f z = ↑(ContinuousLinearEquiv.symm e) y
[PROOFSTEP]
rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hf']
[GOAL]
case neg
ι : Type u_1
R : Type u_2
R₂ : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f
hf' : ¬Summable fun z => ↑e (f z)
⊢ 0 = y ↔ 0 = ↑(ContinuousLinearEquiv.symm e) y
[PROOFSTEP]
refine ⟨?_, fun H => ?_⟩
[GOAL]
case neg.refine_1
ι : Type u_1
R : Type u_2
R₂ : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f
hf' : ¬Summable fun z => ↑e (f z)
⊢ 0 = y → 0 = ↑(ContinuousLinearEquiv.symm e) y
[PROOFSTEP]
rintro rfl
[GOAL]
case neg.refine_1
ι : Type u_1
R : Type u_2
R₂ : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
hf : ¬Summable f
hf' : ¬Summable fun z => ↑e (f z)
⊢ 0 = ↑(ContinuousLinearEquiv.symm e) 0
[PROOFSTEP]
simp
[GOAL]
case neg.refine_2
ι : Type u_1
R : Type u_2
R₂ : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f
hf' : ¬Summable fun z => ↑e (f z)
H : 0 = ↑(ContinuousLinearEquiv.symm e) y
⊢ 0 = y
[PROOFSTEP]
simpa using congr_arg (fun z => e z) H
[GOAL]
ι : Type u_1
R : Type u_2
R₂ : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
⊢ ↑e (∑' (z : ι), f z) = ∑' (z : ι), ↑e (f z)
[PROOFSTEP]
refine' symm (e.tsum_eq_iff.mpr _)
[GOAL]
ι : Type u_1
R : Type u_2
R₂ : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
⊢ ∑' (z : ι), f z = ↑(ContinuousLinearEquiv.symm e) (↑e (∑' (z : ι), f z))
[PROOFSTEP]
rw [e.symm_apply_apply _]
