Metamath Proof Explorer

Theorem erngplus2

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 erngplus2 ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T → U + ˙ V ⁡ F = 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 erngplus ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E → U + ˙ V = f ∈ T ⟼ U ⁡ f ∘ V ⁡ f
7 6 3adantr3 ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T → U + ˙ V = f ∈ T ⟼ U ⁡ f ∘ V ⁡ f
8 fveq2 ⊢ f = F → U ⁡ f = U ⁡ F
9 fveq2 ⊢ f = F → V ⁡ f = V ⁡ F
10 8 9 coeq12d ⊢ f = F → U ⁡ f ∘ V ⁡ f = U ⁡ F ∘ V ⁡ F
11 10 adantl ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T ∧ f = F → U ⁡ f ∘ V ⁡ f = U ⁡ F ∘ V ⁡ F
12 simpr3 ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T → F ∈ T
13 fvex ⊢ U ⁡ F ∈ V
14 fvex ⊢ V ⁡ F ∈ V
15 13 14 coex ⊢ U ⁡ F ∘ V ⁡ F ∈ V
16 15 a1i ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T → U ⁡ F ∘ V ⁡ F ∈ V
17 7 11 12 16 fvmptd ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T → U + ˙ V ⁡ F = U ⁡ F ∘ V ⁡ F