Theorem mendmulr

Description: A specific multiplication in the module endormoprhism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015)

	Ref	Expression
Hypotheses	mendmulrfval.a	⊢ 𝐴 = ( MEndo ‘ 𝑀 )
	mendmulrfval.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	mendmulr.q	⊢ · = ( .r ‘ 𝐴 )
Assertion	mendmulr	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 · 𝑌 ) = ( 𝑋 ∘ 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		mendmulrfval.a	⊢ 𝐴 = ( MEndo ‘ 𝑀 )
2		mendmulrfval.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		mendmulr.q	⊢ · = ( .r ‘ 𝐴 )
4		coexg	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∘ 𝑌 ) ∈ V )
5		coeq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∘ 𝑦 ) = ( 𝑋 ∘ 𝑦 ) )
6		coeq2	⊢ ( 𝑦 = 𝑌 → ( 𝑋 ∘ 𝑦 ) = ( 𝑋 ∘ 𝑌 ) )
7	1 2	mendmulrfval	⊢ ( .r ‘ 𝐴 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ∘ 𝑦 ) )
8	3 7	eqtri	⊢ · = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ∘ 𝑦 ) )
9	5 6 8	ovmpog	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∘ 𝑌 ) ∈ V ) → ( 𝑋 · 𝑌 ) = ( 𝑋 ∘ 𝑌 ) )
10	4 9	mpd3an3	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 · 𝑌 ) = ( 𝑋 ∘ 𝑌 ) )