Metamath Proof Explorer


Theorem erngfmul

Description: Ring multiplication operation. (Contributed by NM, 9-Jun-2013)

Ref Expression
Hypotheses erngset.h 𝐻 = ( LHyp ‘ 𝐾 )
erngset.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
erngset.e 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
erngset.d 𝐷 = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 )
erng.m · = ( .r𝐷 )
Assertion erngfmul ( ( 𝐾𝑉𝑊𝐻 ) → · = ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑠𝑡 ) ) )

Proof

Step Hyp Ref Expression
1 erngset.h 𝐻 = ( LHyp ‘ 𝐾 )
2 erngset.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 erngset.e 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
4 erngset.d 𝐷 = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 )
5 erng.m · = ( .r𝐷 )
6 1 2 3 4 erngset ( ( 𝐾𝑉𝑊𝐻 ) → 𝐷 = { ⟨ ( Base ‘ ndx ) , 𝐸 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑠𝑡 ) ) ⟩ } )
7 6 fveq2d ( ( 𝐾𝑉𝑊𝐻 ) → ( .r𝐷 ) = ( .r ‘ { ⟨ ( 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 rngmulr ( ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑠𝑡 ) ) ∈ V → ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑠𝑡 ) ) = ( .r ‘ { ⟨ ( Base ‘ ndx ) , 𝐸 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑠𝑡 ) ) ⟩ } ) )
12 9 11 ax-mp ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑠𝑡 ) ) = ( .r ‘ { ⟨ ( Base ‘ ndx ) , 𝐸 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑠𝑡 ) ) ⟩ } )
13 7 5 12 3eqtr4g ( ( 𝐾𝑉𝑊𝐻 ) → · = ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑠𝑡 ) ) )