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	$⊢ \underset{˙}{\cdot} = \cdot_{A}$
Assertion	mattposvs	$⊢ (X \in K \land Y \in B) \to tpos (X \underset{˙}{\cdot} Y) = X \underset{˙}{\cdot} 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	$⊢ \underset{˙}{\cdot} = \cdot_{A}$
5	1 2	matrcl	$⊢ Y \in B \to (N \in Fin \land R \in V)$
6	5	simpld	$⊢ Y \in B \to N \in Fin$
7		sqxpexg	$⊢ N \in Fin \to N \times N \in V$
8	6 7	syl	$⊢ Y \in B \to N \times N \in V$
9		snex	$⊢ \{X\} \in V$
10		xpexg	$⊢ (N \times N \in V \land \{X\} \in V) \to (N \times N) \times \{X\} \in V$
11	8 9 10	sylancl	$⊢ Y \in B \to (N \times N) \times \{X\} \in V$
12		oftpos	$⊢ ((N \times N) \times \{X\} \in V \land Y \in B) \to tpos (((N \times N) \times \{X\}) {\cdot_{R}}_{f} Y) = tpos ((N \times N) \times \{X\}) {\cdot_{R}}_{f} tpos Y$
13	11 12	mpancom	$⊢ Y \in B \to tpos (((N \times N) \times \{X\}) {\cdot_{R}}_{f} Y) = tpos ((N \times N) \times \{X\}) {\cdot_{R}}_{f} tpos Y$
14		tposconst	$⊢ tpos ((N \times N) \times \{X\}) = (N \times N) \times \{X\}$
15	14	oveq1i	$⊢ tpos ((N \times N) \times \{X\}) {\cdot_{R}}_{f} tpos Y = ((N \times N) \times \{X\}) {\cdot_{R}}_{f} tpos Y$
16	13 15	eqtrdi	$⊢ Y \in B \to tpos (((N \times N) \times \{X\}) {\cdot_{R}}_{f} Y) = ((N \times N) \times \{X\}) {\cdot_{R}}_{f} tpos Y$
17	16	adantl	$⊢ (X \in K \land Y \in B) \to tpos (((N \times N) \times \{X\}) {\cdot_{R}}_{f} Y) = ((N \times N) \times \{X\}) {\cdot_{R}}_{f} tpos Y$
18		eqid	$⊢ \cdot_{R} = \cdot_{R}$
19		eqid	$⊢ N \times N = N \times N$
20	1 2 3 4 18 19	matvsca2	$⊢ (X \in K \land Y \in B) \to X \underset{˙}{\cdot} Y = ((N \times N) \times \{X\}) {\cdot_{R}}_{f} Y$
21	20	tposeqd	$⊢ (X \in K \land Y \in B) \to tpos (X \underset{˙}{\cdot} Y) = tpos (((N \times N) \times \{X\}) {\cdot_{R}}_{f} Y)$
22	1 2	mattposcl	$⊢ Y \in B \to tpos Y \in B$
23	1 2 3 4 18 19	matvsca2	$⊢ (X \in K \land tpos Y \in B) \to X \underset{˙}{\cdot} tpos Y = ((N \times N) \times \{X\}) {\cdot_{R}}_{f} tpos Y$
24	22 23	sylan2	$⊢ (X \in K \land Y \in B) \to X \underset{˙}{\cdot} tpos Y = ((N \times N) \times \{X\}) {\cdot_{R}}_{f} tpos Y$
25	17 21 24	3eqtr4d	$⊢ (X \in K \land Y \in B) \to tpos (X \underset{˙}{\cdot} Y) = X \underset{˙}{\cdot} tpos Y$

Metamath Proof Explorer

Theorem mattposvs

Proof