Metamath Proof Explorer


Theorem erngfplus-rN

Description: Ring addition operation. (Contributed by NM, 9-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 erngfplus-rN ( ( 𝐾𝑉𝑊𝐻 ) → + = ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) )

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 erngset-rN ( ( 𝐾𝑉𝑊𝐻 ) → 𝐷 = { ⟨ ( Base ‘ ndx ) , 𝐸 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑡𝑠 ) ) ⟩ } )
7 6 fveq2d ( ( 𝐾𝑉𝑊𝐻 ) → ( +g𝐷 ) = ( +g ‘ { ⟨ ( Base ‘ ndx ) , 𝐸 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑡𝑠 ) ) ⟩ } ) )
8 3 fvexi 𝐸 ∈ V
9 8 8 mpoex ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ∈ V
10 eqid { ⟨ ( Base ‘ ndx ) , 𝐸 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑡𝑠 ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐸 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑡𝑠 ) ) ⟩ }
11 10 rngplusg ( ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ∈ V → ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) = ( +g ‘ { ⟨ ( Base ‘ ndx ) , 𝐸 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑡𝑠 ) ) ⟩ } ) )
12 9 11 ax-mp ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) = ( +g ‘ { ⟨ ( Base ‘ ndx ) , 𝐸 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑡𝑠 ) ) ⟩ } )
13 7 5 12 3eqtr4g ( ( 𝐾𝑉𝑊𝐻 ) → + = ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) )