Metamath Proof Explorer


Theorem erngplus2-rN

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

Ref Expression
Hypotheses erngset.h-r 𝐻 = ( LHyp ‘ 𝐾 )
erngset.t-r 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
erngset.e-r 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
erngset.d-r 𝐷 = ( ( EDRingR𝐾 ) ‘ 𝑊 )
erng.p-r + = ( +g𝐷 )
Assertion erngplus2-rN ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑉𝐸𝐹𝑇 ) ) → ( ( 𝑈 + 𝑉 ) ‘ 𝐹 ) = ( ( 𝑈𝐹 ) ∘ ( 𝑉𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 erngset.h-r 𝐻 = ( LHyp ‘ 𝐾 )
2 erngset.t-r 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 erngset.e-r 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
4 erngset.d-r 𝐷 = ( ( EDRingR𝐾 ) ‘ 𝑊 )
5 erng.p-r + = ( +g𝐷 )
6 1 2 3 4 5 erngplus-rN ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑉𝐸 ) ) → ( 𝑈 + 𝑉 ) = ( 𝑓𝑇 ↦ ( ( 𝑈𝑓 ) ∘ ( 𝑉𝑓 ) ) ) )
7 6 3adantr3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑉𝐸𝐹𝑇 ) ) → ( 𝑈 + 𝑉 ) = ( 𝑓𝑇 ↦ ( ( 𝑈𝑓 ) ∘ ( 𝑉𝑓 ) ) ) )
8 fveq2 ( 𝑓 = 𝐹 → ( 𝑈𝑓 ) = ( 𝑈𝐹 ) )
9 fveq2 ( 𝑓 = 𝐹 → ( 𝑉𝑓 ) = ( 𝑉𝐹 ) )
10 8 9 coeq12d ( 𝑓 = 𝐹 → ( ( 𝑈𝑓 ) ∘ ( 𝑉𝑓 ) ) = ( ( 𝑈𝐹 ) ∘ ( 𝑉𝐹 ) ) )
11 10 adantl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑉𝐸𝐹𝑇 ) ) ∧ 𝑓 = 𝐹 ) → ( ( 𝑈𝑓 ) ∘ ( 𝑉𝑓 ) ) = ( ( 𝑈𝐹 ) ∘ ( 𝑉𝐹 ) ) )
12 simpr3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑉𝐸𝐹𝑇 ) ) → 𝐹𝑇 )
13 fvex ( 𝑈𝐹 ) ∈ V
14 fvex ( 𝑉𝐹 ) ∈ V
15 13 14 coex ( ( 𝑈𝐹 ) ∘ ( 𝑉𝐹 ) ) ∈ V
16 15 a1i ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑉𝐸𝐹𝑇 ) ) → ( ( 𝑈𝐹 ) ∘ ( 𝑉𝐹 ) ) ∈ V )
17 7 11 12 16 fvmptd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑉𝐸𝐹𝑇 ) ) → ( ( 𝑈 + 𝑉 ) ‘ 𝐹 ) = ( ( 𝑈𝐹 ) ∘ ( 𝑉𝐹 ) ) )