mattposm

Description: Multiplying two transposed matrices results in the transposition of the product of the two matrices. (Contributed by Stefan O'Rear, 17-Jul-2018)

	Ref	Expression
Hypotheses	mattposm.a	$⊢ A = N Mat R$
	mattposm.b	$⊢ B = {Base}_{A}$
	mattposm.t	$⊢ \underset{˙}{\cdot} = \cdot_{A}$
Assertion	mattposm	$⊢ (R \in CRing \land X \in B \land Y \in B) \to tpos (X \underset{˙}{\cdot} Y) = tpos Y \underset{˙}{\cdot} tpos X$

Proof

Step	Hyp	Ref	Expression
1		mattposm.a	$⊢ A = N Mat R$
2		mattposm.b	$⊢ B = {Base}_{A}$
3		mattposm.t	$⊢ \underset{˙}{\cdot} = \cdot_{A}$
4		eqid	$⊢ R maMul ⟨N, N, N⟩ = R maMul ⟨N, N, N⟩$
5		eqid	$⊢ {Base}_{R} = {Base}_{R}$
6		simp1	$⊢ (R \in CRing \land X \in B \land Y \in B) \to R \in CRing$
7	1 2	matrcl	$⊢ Y \in B \to (N \in Fin \land R \in V)$
8	7	simpld	$⊢ Y \in B \to N \in Fin$
9	8	3ad2ant3	$⊢ (R \in CRing \land X \in B \land Y \in B) \to N \in Fin$
10	1 5 2	matbas2i	$⊢ X \in B \to X \in ({Base}_{R}^{(N \times N)})$
11	10	3ad2ant2	$⊢ (R \in CRing \land X \in B \land Y \in B) \to X \in ({Base}_{R}^{(N \times N)})$
12	1 5 2	matbas2i	$⊢ Y \in B \to Y \in ({Base}_{R}^{(N \times N)})$
13	12	3ad2ant3	$⊢ (R \in CRing \land X \in B \land Y \in B) \to Y \in ({Base}_{R}^{(N \times N)})$
14	4 4 5 6 9 9 9 11 13	mamutpos	$⊢ (R \in CRing \land X \in B \land Y \in B) \to tpos (X (R maMul ⟨N, N, N⟩) Y) = tpos Y (R maMul ⟨N, N, N⟩) tpos X$
15	1 4	matmulr	$⊢ (N \in Fin \land R \in CRing) \to R maMul ⟨N, N, N⟩ = \cdot_{A}$
16	9 6 15	syl2anc	$⊢ (R \in CRing \land X \in B \land Y \in B) \to R maMul ⟨N, N, N⟩ = \cdot_{A}$
17	3 16	eqtr4id	$⊢ (R \in CRing \land X \in B \land Y \in B) \to \underset{˙}{\cdot} = R maMul ⟨N, N, N⟩$
18	17	oveqd	$⊢ (R \in CRing \land X \in B \land Y \in B) \to X \underset{˙}{\cdot} Y = X (R maMul ⟨N, N, N⟩) Y$
19	18	tposeqd	$⊢ (R \in CRing \land X \in B \land Y \in B) \to tpos (X \underset{˙}{\cdot} Y) = tpos (X (R maMul ⟨N, N, N⟩) Y)$
20	17	oveqd	$⊢ (R \in CRing \land X \in B \land Y \in B) \to tpos Y \underset{˙}{\cdot} tpos X = tpos Y (R maMul ⟨N, N, N⟩) tpos X$
21	14 19 20	3eqtr4d	$⊢ (R \in CRing \land X \in B \land Y \in B) \to tpos (X \underset{˙}{\cdot} Y) = tpos Y \underset{˙}{\cdot} tpos X$

Metamath Proof Explorer

Theorem mattposm

Proof