case h
R₁ : Type u_6
R₂ : Type u_1
R₃ : Type u_2
inst✝¹⁷ : Semiring R₁
inst✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_5
inst✝¹⁴ : TopologicalSpace M₁
inst✝¹³ : AddCommMonoid M₁
M'₁ : Type ?u.510286
inst✝¹² : TopologicalSpace M'₁
inst✝¹¹ : AddCommMonoid M'₁
M₂ : Type u_3
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
M₃ : Type u_4
inst✝⁸ : TopologicalSpace M₃
inst✝⁷ : AddCommMonoid M₃
M₄ : Type ?u.510313
inst✝⁶ : TopologicalSpace M₄
inst✝⁵ : AddCommMonoid M₄
inst✝⁴ : Module R₁ M₁
inst✝³ : Module R₁ M'₁
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
g : M₂ →SL[σ₂₃] M₃
x✝ : M₁
⊢ ↑(comp g 0) x✝ = ↑0 x✝
R₁ : Type u_6
R₂ : Type u_1
R₃ : Type u_2
inst✝¹⁷ : Semiring R₁
inst✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_5
inst✝¹⁴ : TopologicalSpace M₁
inst✝¹³ : AddCommMonoid M₁
M'₁ : Type ?u.510286
inst✝¹² : TopologicalSpace M'₁
inst✝¹¹ : AddCommMonoid M'₁
M₂ : Type u_3
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
M₃ : Type u_4
inst✝⁸ : TopologicalSpace M₃
inst✝⁷ : AddCommMonoid M₃
M₄ : Type ?u.510313
inst✝⁶ : TopologicalSpace M₄
inst✝⁵ : AddCommMonoid M₄
inst✝⁴ : Module R₁ M₁
inst✝³ : Module R₁ M'₁
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
g : M₂ →SL[σ₂₃] M₃
⊢ comp g 0 = 0
ext
no goals
case h
R₁ : Type u_6
R₂ : Type u_1
R₃ : Type u_2
inst✝¹⁷ : Semiring R₁
inst✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_5
inst✝¹⁴ : TopologicalSpace M₁
inst✝¹³ : AddCommMonoid M₁
M'₁ : Type ?u.510286
inst✝¹² : TopologicalSpace M'₁
inst✝¹¹ : AddCommMonoid M'₁
M₂ : Type u_3
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
M₃ : Type u_4
inst✝⁸ : TopologicalSpace M₃
inst✝⁷ : AddCommMonoid M₃
M₄ : Type ?u.510313
inst✝⁶ : TopologicalSpace M₄
inst✝⁵ : AddCommMonoid M₄
inst✝⁴ : Module R₁ M₁
inst✝³ : Module R₁ M'₁
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
g : M₂ →SL[σ₂₃] M₃
x✝ : M₁
⊢ ↑(comp g 0) x✝ = ↑0 x✝
simp