Theorem erngfmul-rN

Description: Ring multiplication 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.m-r	⊢ · = ( .r ‘ 𝐷 )
Assertion	erngfmul-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.m-r	⊢ · = ( .r ‘ 𝐷 )
6	1 2 3 4	erngset-rN	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → 𝐷 = { ⟨ ( 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	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → · = ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑡 ∘ 𝑠 ) ) )