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 𝐻 = ( LHyp ‘ 𝐾 )
erngset.t-r 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
erngset.e-r 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
erngset.d-r 𝐷 = ( ( EDRingR𝐾 ) ‘ 𝑊 )
erng.p-r + = ( +g𝐷 )
Assertion erngplus-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 erngfplus-rN ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → + = ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑔𝑇 ↦ ( ( 𝑠𝑔 ) ∘ ( 𝑡𝑔 ) ) ) ) )
7 6 oveqd ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( 𝑈 + 𝑉 ) = ( 𝑈 ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑔𝑇 ↦ ( ( 𝑠𝑔 ) ∘ ( 𝑡𝑔 ) ) ) ) 𝑉 ) )
8 eqid ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑔𝑇 ↦ ( ( 𝑠𝑔 ) ∘ ( 𝑡𝑔 ) ) ) ) = ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑔𝑇 ↦ ( ( 𝑠𝑔 ) ∘ ( 𝑡𝑔 ) ) ) )
9 8 2 tendopl ( ( 𝑈𝐸𝑉𝐸 ) → ( 𝑈 ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑔𝑇 ↦ ( ( 𝑠𝑔 ) ∘ ( 𝑡𝑔 ) ) ) ) 𝑉 ) = ( 𝑓𝑇 ↦ ( ( 𝑈𝑓 ) ∘ ( 𝑉𝑓 ) ) ) )
10 7 9 sylan9eq ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑉𝐸 ) ) → ( 𝑈 + 𝑉 ) = ( 𝑓𝑇 ↦ ( ( 𝑈𝑓 ) ∘ ( 𝑉𝑓 ) ) ) )