This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ A = N Mat R
mattposvs.b ⊢ B = Base A
mattposvs.k ⊢ K = Base R
mattposvs.v ⊢ · ˙ = ⋅ A
Assertion mattposvs ⊢ X ∈ K ∧ Y ∈ B → tpos X · ˙ Y = X · ˙ tpos Y

Proof

Step Hyp Ref Expression
1 mattposvs.a ⊢ A = N Mat R
2 mattposvs.b ⊢ B = Base A
3 mattposvs.k ⊢ K = Base R
4 mattposvs.v ⊢ · ˙ = ⋅ A
5 1 2 matrcl ⊢ Y ∈ B → N ∈ Fin ∧ R ∈ V
6 5 simpld ⊢ Y ∈ B → N ∈ Fin
7 sqxpexg ⊢ N ∈ Fin → N × N ∈ V
8 6 7 syl ⊢ Y ∈ B → N × N ∈ V
9 snex ⊢ X ∈ V
10 xpexg ⊢ N × N ∈ V ∧ X ∈ V → N × N × X ∈ V
11 8 9 10 sylancl ⊢ Y ∈ B → N × N × X ∈ V
12 oftpos ⊢ N × N × X ∈ V ∧ Y ∈ B → tpos N × N × X ⋅ R f Y = tpos N × N × X ⋅ R f tpos Y
13 11 12 mpancom ⊢ Y ∈ B → tpos N × N × X ⋅ R f Y = tpos N × N × X ⋅ R f tpos Y
14 tposconst ⊢ tpos N × N × X = N × N × X
15 14 oveq1i ⊢ tpos N × N × X ⋅ R f tpos Y = N × N × X ⋅ R f tpos Y
16 13 15 eqtrdi ⊢ Y ∈ B → tpos N × N × X ⋅ R f Y = N × N × X ⋅ R f tpos Y
17 16 adantl ⊢ X ∈ K ∧ Y ∈ B → tpos N × N × X ⋅ R f Y = N × N × X ⋅ R f tpos Y
18 eqid ⊢ ⋅ R = ⋅ R
19 eqid ⊢ N × N = N × N
20 1 2 3 4 18 19 matvsca2 ⊢ X ∈ K ∧ Y ∈ B → X · ˙ Y = N × N × X ⋅ R f Y
21 20 tposeqd ⊢ X ∈ K ∧ Y ∈ B → tpos X · ˙ Y = tpos N × N × X ⋅ R f Y
22 1 2 mattposcl ⊢ Y ∈ B → tpos Y ∈ B
23 1 2 3 4 18 19 matvsca2 ⊢ X ∈ K ∧ tpos Y ∈ B → X · ˙ tpos Y = N × N × X ⋅ R f tpos Y
24 22 23 sylan2 ⊢ X ∈ K ∧ Y ∈ B → X · ˙ tpos Y = N × N × X ⋅ R f tpos Y
25 17 21 24 3eqtr4d ⊢ X ∈ K ∧ Y ∈ B → tpos X · ˙ Y = X · ˙ tpos Y