Metamath Proof Explorer

Theorem erngplus-rN

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

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

Proof

Step Hyp Ref Expression
1 erngset.h-r ⊢ H = LHyp ⁡ K
2 erngset.t-r ⊢ T = LTrn ⁡ K ⁡ W
3 erngset.e-r ⊢ E = TEndo ⁡ K ⁡ W
4 erngset.d-r ⊢ D = EDRing R ⁡ K ⁡ W
5 erng.p-r ⊢ + ˙ = + D
6 1 2 3 4 5 erngfplus-rN ⊢ 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