Metamath Proof Explorer

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 𝑌 ) )