Theorem erngmul-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.m-r	⊢ · = ( .r ‘ 𝐷 )
Assertion	erngmul-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 5	erngfmul-rN	⊢ ( ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) → · = ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑡 ∘ 𝑠 ) ) )
7	6	adantr	⊢ ( ( ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) → · = ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑡 ∘ 𝑠 ) ) )
8	7	oveqd	⊢ ( ( ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) → ( 𝑈 · 𝑉 ) = ( 𝑈 ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑡 ∘ 𝑠 ) ) 𝑉 ) )
9		coexg	⊢ ( ( 𝑉 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ) → ( 𝑉 ∘ 𝑈 ) ∈ V )
10	9	ancoms	⊢ ( ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) → ( 𝑉 ∘ 𝑈 ) ∈ V )
11		coeq2	⊢ ( 𝑠 = 𝑈 → ( 𝑡 ∘ 𝑠 ) = ( 𝑡 ∘ 𝑈 ) )
12		coeq1	⊢ ( 𝑡 = 𝑉 → ( 𝑡 ∘ 𝑈 ) = ( 𝑉 ∘ 𝑈 ) )
13		eqid	⊢ ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑡 ∘ 𝑠 ) ) = ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑡 ∘ 𝑠 ) )
14	11 12 13	ovmpog	⊢ ( ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑉 ∘ 𝑈 ) ∈ V ) → ( 𝑈 ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑡 ∘ 𝑠 ) ) 𝑉 ) = ( 𝑉 ∘ 𝑈 ) )
15	10 14	mpd3an3	⊢ ( ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) → ( 𝑈 ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑡 ∘ 𝑠 ) ) 𝑉 ) = ( 𝑉 ∘ 𝑈 ) )
16	15	adantl	⊢ ( ( ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) → ( 𝑈 ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑡 ∘ 𝑠 ) ) 𝑉 ) = ( 𝑉 ∘ 𝑈 ) )
17	8 16	eqtrd	⊢ ( ( ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ) → ( 𝑈 · 𝑉 ) = ( 𝑉 ∘ 𝑈 ) )