Metamath Proof Explorer

Theorem erngplus

Description: Ring addition operation. (Contributed by NM, 10-Jun-2013)

Ref Expression
Hypotheses erngset.h ⊢ H = LHyp ⁡ K
erngset.t ⊢ T = LTrn ⁡ K ⁡ W
erngset.e ⊢ E = TEndo ⁡ K ⁡ W
erngset.d ⊢ D = EDRing ⁡ K ⁡ W
erng.p ⊢ + ˙ = + D
Assertion erngplus ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E → U + ˙ V = f ∈ T ⟼ U ⁡ f ∘ V ⁡ f

Proof

Step Hyp Ref Expression
1 erngset.h ⊢ H = LHyp ⁡ K
2 erngset.t ⊢ T = LTrn ⁡ K ⁡ W
3 erngset.e ⊢ E = TEndo ⁡ K ⁡ W
4 erngset.d ⊢ D = EDRing ⁡ K ⁡ W
5 erng.p ⊢ + ˙ = + D
6 1 2 3 4 5 erngfplus ⊢ K ∈ HL ∧ W ∈ H → + ˙ = s ∈ E , t ∈ E ⟼ g ∈ T ⟼ s ⁡ g ∘ t ⁡ g
7 6 oveqd ⊢ K ∈ HL ∧ W ∈ H → U + ˙ V = U s ∈ E , t ∈ E ⟼ g ∈ T ⟼ s ⁡ g ∘ t ⁡ g V
8 eqid ⊢ s ∈ E , t ∈ E ⟼ g ∈ T ⟼ s ⁡ g ∘ t ⁡ g = s ∈ E , t ∈ E ⟼ g ∈ T ⟼ s ⁡ g ∘ t ⁡ g
9 8 2 tendopl ⊢ U ∈ E ∧ V ∈ E → U s ∈ E , t ∈ E ⟼ g ∈ T ⟼ s ⁡ g ∘ t ⁡ g V = f ∈ T ⟼ U ⁡ f ∘ V ⁡ f
10 7 9 sylan9eq ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E → U + ˙ V = f ∈ T ⟼ U ⁡ f ∘ V ⁡ f