Theorem mattposvs

Description: The transposition of a matrix multiplied with a scalar equals the transposed matrix multiplied with the scalar, see also the statement in Lang p. 505. (Contributed by Stefan O'Rear, 17-Jul-2018)

	Ref	Expression
Hypotheses	mattposvs.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	mattposvs.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	mattposvs.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	mattposvs.v	⊢ · = ( ·𝑠 ‘ 𝐴 )
Assertion	mattposvs	⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → tpos ( 𝑋 · 𝑌 ) = ( 𝑋 · tpos 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		mattposvs.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		mattposvs.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		mattposvs.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
4		mattposvs.v	⊢ · = ( ·𝑠 ‘ 𝐴 )
5	1 2	matrcl	⊢ ( 𝑌 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
6	5	simpld	⊢ ( 𝑌 ∈ 𝐵 → 𝑁 ∈ Fin )
7		sqxpexg	⊢ ( 𝑁 ∈ Fin → ( 𝑁 × 𝑁 ) ∈ V )
8	6 7	syl	⊢ ( 𝑌 ∈ 𝐵 → ( 𝑁 × 𝑁 ) ∈ V )
9		snex	⊢ { 𝑋 } ∈ V
10		xpexg	⊢ ( ( ( 𝑁 × 𝑁 ) ∈ V ∧ { 𝑋 } ∈ V ) → ( ( 𝑁 × 𝑁 ) × { 𝑋 } ) ∈ V )
11	8 9 10	sylancl	⊢ ( 𝑌 ∈ 𝐵 → ( ( 𝑁 × 𝑁 ) × { 𝑋 } ) ∈ V )
12		oftpos	⊢ ( ( ( ( 𝑁 × 𝑁 ) × { 𝑋 } ) ∈ V ∧ 𝑌 ∈ 𝐵 ) → tpos ( ( ( 𝑁 × 𝑁 ) × { 𝑋 } ) ∘f ( .r ‘ 𝑅 ) 𝑌 ) = ( tpos ( ( 𝑁 × 𝑁 ) × { 𝑋 } ) ∘f ( .r ‘ 𝑅 ) tpos 𝑌 ) )
13	11 12	mpancom	⊢ ( 𝑌 ∈ 𝐵 → tpos ( ( ( 𝑁 × 𝑁 ) × { 𝑋 } ) ∘f ( .r ‘ 𝑅 ) 𝑌 ) = ( tpos ( ( 𝑁 × 𝑁 ) × { 𝑋 } ) ∘f ( .r ‘ 𝑅 ) tpos 𝑌 ) )
14		tposconst	⊢ tpos ( ( 𝑁 × 𝑁 ) × { 𝑋 } ) = ( ( 𝑁 × 𝑁 ) × { 𝑋 } )
15	14	oveq1i	⊢ ( tpos ( ( 𝑁 × 𝑁 ) × { 𝑋 } ) ∘f ( .r ‘ 𝑅 ) tpos 𝑌 ) = ( ( ( 𝑁 × 𝑁 ) × { 𝑋 } ) ∘f ( .r ‘ 𝑅 ) tpos 𝑌 )
16	13 15	eqtrdi	⊢ ( 𝑌 ∈ 𝐵 → tpos ( ( ( 𝑁 × 𝑁 ) × { 𝑋 } ) ∘f ( .r ‘ 𝑅 ) 𝑌 ) = ( ( ( 𝑁 × 𝑁 ) × { 𝑋 } ) ∘f ( .r ‘ 𝑅 ) tpos 𝑌 ) )
17	16	adantl	⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → tpos ( ( ( 𝑁 × 𝑁 ) × { 𝑋 } ) ∘f ( .r ‘ 𝑅 ) 𝑌 ) = ( ( ( 𝑁 × 𝑁 ) × { 𝑋 } ) ∘f ( .r ‘ 𝑅 ) tpos 𝑌 ) )
18		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
19		eqid	⊢ ( 𝑁 × 𝑁 ) = ( 𝑁 × 𝑁 )
20	1 2 3 4 18 19	matvsca2	⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 · 𝑌 ) = ( ( ( 𝑁 × 𝑁 ) × { 𝑋 } ) ∘f ( .r ‘ 𝑅 ) 𝑌 ) )
21	20	tposeqd	⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → tpos ( 𝑋 · 𝑌 ) = tpos ( ( ( 𝑁 × 𝑁 ) × { 𝑋 } ) ∘f ( .r ‘ 𝑅 ) 𝑌 ) )
22	1 2	mattposcl	⊢ ( 𝑌 ∈ 𝐵 → tpos 𝑌 ∈ 𝐵 )
23	1 2 3 4 18 19	matvsca2	⊢ ( ( 𝑋 ∈ 𝐾 ∧ tpos 𝑌 ∈ 𝐵 ) → ( 𝑋 · tpos 𝑌 ) = ( ( ( 𝑁 × 𝑁 ) × { 𝑋 } ) ∘f ( .r ‘ 𝑅 ) tpos 𝑌 ) )
24	22 23	sylan2	⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 · tpos 𝑌 ) = ( ( ( 𝑁 × 𝑁 ) × { 𝑋 } ) ∘f ( .r ‘ 𝑅 ) tpos 𝑌 ) )
25	17 21 24	3eqtr4d	⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → tpos ( 𝑋 · 𝑌 ) = ( 𝑋 · tpos 𝑌 ) )