Theorem mendvsca

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

	Ref	Expression
Hypotheses	mendvscafval.a	⊢ 𝐴 = ( MEndo ‘ 𝑀 )
	mendvscafval.v	⊢ · = ( ·𝑠 ‘ 𝑀 )
	mendvscafval.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	mendvscafval.s	⊢ 𝑆 = ( Scalar ‘ 𝑀 )
	mendvscafval.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
	mendvscafval.e	⊢ 𝐸 = ( Base ‘ 𝑀 )
	mendvsca.w	⊢ ∙ = ( ·𝑠 ‘ 𝐴 )
Assertion	mendvsca	⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∙ 𝑌 ) = ( ( 𝐸 × { 𝑋 } ) ∘f · 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		mendvscafval.a	⊢ 𝐴 = ( MEndo ‘ 𝑀 )
2		mendvscafval.v	⊢ · = ( ·𝑠 ‘ 𝑀 )
3		mendvscafval.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
4		mendvscafval.s	⊢ 𝑆 = ( Scalar ‘ 𝑀 )
5		mendvscafval.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
6		mendvscafval.e	⊢ 𝐸 = ( Base ‘ 𝑀 )
7		mendvsca.w	⊢ ∙ = ( ·𝑠 ‘ 𝐴 )
8		sneq	⊢ ( 𝑥 = 𝑋 → { 𝑥 } = { 𝑋 } )
9	8	xpeq2d	⊢ ( 𝑥 = 𝑋 → ( 𝐸 × { 𝑥 } ) = ( 𝐸 × { 𝑋 } ) )
10		id	⊢ ( 𝑦 = 𝑌 → 𝑦 = 𝑌 )
11	9 10	oveqan12d	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ( 𝐸 × { 𝑥 } ) ∘f · 𝑦 ) = ( ( 𝐸 × { 𝑋 } ) ∘f · 𝑌 ) )
12	1 2 3 4 5 6	mendvscafval	⊢ ( ·𝑠 ‘ 𝐴 ) = ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( ( 𝐸 × { 𝑥 } ) ∘f · 𝑦 ) )
13	7 12	eqtri	⊢ ∙ = ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( ( 𝐸 × { 𝑥 } ) ∘f · 𝑦 ) )
14		ovex	⊢ ( ( 𝐸 × { 𝑋 } ) ∘f · 𝑌 ) ∈ V
15	11 13 14	ovmpoa	⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∙ 𝑌 ) = ( ( 𝐸 × { 𝑋 } ) ∘f · 𝑌 ) )