mamutpos

Description: Behavior of transposes in matrix products, see also the statement in Lang p. 505. (Contributed by Stefan O'Rear, 9-Jul-2018)

	Ref	Expression
Hypotheses	mamutpos.f	$⊢ F = R maMul ⟨M, N, P⟩$
	mamutpos.g	$⊢ G = R maMul ⟨P, N, M⟩$
	mamutpos.b	$⊢ B = {Base}_{R}$
	mamutpos.r	$⊢ φ \to R \in CRing$
	mamutpos.m	$⊢ φ \to M \in Fin$
	mamutpos.n	$⊢ φ \to N \in Fin$
	mamutpos.p	$⊢ φ \to P \in Fin$
	mamutpos.x	$⊢ φ \to X \in (B^{(M \times N)})$
	mamutpos.y	$⊢ φ \to Y \in (B^{(N \times P)})$
Assertion	mamutpos	$⊢ φ \to tpos (X F Y) = tpos Y G tpos X$

Proof

Step	Hyp	Ref	Expression
1		mamutpos.f	$⊢ F = R maMul ⟨M, N, P⟩$
2		mamutpos.g	$⊢ G = R maMul ⟨P, N, M⟩$
3		mamutpos.b	$⊢ B = {Base}_{R}$
4		mamutpos.r	$⊢ φ \to R \in CRing$
5		mamutpos.m	$⊢ φ \to M \in Fin$
6		mamutpos.n	$⊢ φ \to N \in Fin$
7		mamutpos.p	$⊢ φ \to P \in Fin$
8		mamutpos.x	$⊢ φ \to X \in (B^{(M \times N)})$
9		mamutpos.y	$⊢ φ \to Y \in (B^{(N \times P)})$
10		eqid	$⊢ (j \in M, i \in P ⟼ \underset{k \in N}{\sum_{R}} ((j X k) \cdot_{R} (k Y i))) = (j \in M, i \in P ⟼ \underset{k \in N}{\sum_{R}} ((j X k) \cdot_{R} (k Y i)))$
11	10	tposmpo	$⊢ tpos (j \in M, i \in P ⟼ \underset{k \in N}{\sum_{R}} ((j X k) \cdot_{R} (k Y i))) = (i \in P, j \in M ⟼ \underset{k \in N}{\sum_{R}} ((j X k) \cdot_{R} (k Y i)))$
12		simpl1	$⊢ ((φ \land i \in P \land j \in M) \land k \in N) \to φ$
13	12 4	syl	$⊢ ((φ \land i \in P \land j \in M) \land k \in N) \to R \in CRing$
14		elmapi	$⊢ X \in (B^{(M \times N)}) \to X : M \times N ⟶ B$
15	12 8 14	3syl	$⊢ ((φ \land i \in P \land j \in M) \land k \in N) \to X : M \times N ⟶ B$
16		simpl3	$⊢ ((φ \land i \in P \land j \in M) \land k \in N) \to j \in M$
17		simpr	$⊢ ((φ \land i \in P \land j \in M) \land k \in N) \to k \in N$
18	15 16 17	fovrnd	$⊢ ((φ \land i \in P \land j \in M) \land k \in N) \to j X k \in B$
19		elmapi	$⊢ Y \in (B^{(N \times P)}) \to Y : N \times P ⟶ B$
20	12 9 19	3syl	$⊢ ((φ \land i \in P \land j \in M) \land k \in N) \to Y : N \times P ⟶ B$
21		simpl2	$⊢ ((φ \land i \in P \land j \in M) \land k \in N) \to i \in P$
22	20 17 21	fovrnd	$⊢ ((φ \land i \in P \land j \in M) \land k \in N) \to k Y i \in B$
23		eqid	$⊢ \cdot_{R} = \cdot_{R}$
24	3 23	crngcom	$⊢ (R \in CRing \land j X k \in B \land k Y i \in B) \to (j X k) \cdot_{R} (k Y i) = (k Y i) \cdot_{R} (j X k)$
25	13 18 22 24	syl3anc	$⊢ ((φ \land i \in P \land j \in M) \land k \in N) \to (j X k) \cdot_{R} (k Y i) = (k Y i) \cdot_{R} (j X k)$
26		ovtpos	$⊢ i tpos Y k = k Y i$
27		ovtpos	$⊢ k tpos X j = j X k$
28	26 27	oveq12i	$⊢ (i tpos Y k) \cdot_{R} (k tpos X j) = (k Y i) \cdot_{R} (j X k)$
29	25 28	eqtr4di	$⊢ ((φ \land i \in P \land j \in M) \land k \in N) \to (j X k) \cdot_{R} (k Y i) = (i tpos Y k) \cdot_{R} (k tpos X j)$
30	29	mpteq2dva	$⊢ (φ \land i \in P \land j \in M) \to (k \in N ⟼ (j X k) \cdot_{R} (k Y i)) = (k \in N ⟼ (i tpos Y k) \cdot_{R} (k tpos X j))$
31	30	oveq2d	$⊢ (φ \land i \in P \land j \in M) \to \underset{k \in N}{\sum_{R}} ((j X k) \cdot_{R} (k Y i)) = \underset{k \in N}{\sum_{R}} ((i tpos Y k) \cdot_{R} (k tpos X j))$
32	31	mpoeq3dva	$⊢ φ \to (i \in P, j \in M ⟼ \underset{k \in N}{\sum_{R}} ((j X k) \cdot_{R} (k Y i))) = (i \in P, j \in M ⟼ \underset{k \in N}{\sum_{R}} ((i tpos Y k) \cdot_{R} (k tpos X j)))$
33	11 32	syl5eq	$⊢ φ \to tpos (j \in M, i \in P ⟼ \underset{k \in N}{\sum_{R}} ((j X k) \cdot_{R} (k Y i))) = (i \in P, j \in M ⟼ \underset{k \in N}{\sum_{R}} ((i tpos Y k) \cdot_{R} (k tpos X j)))$
34	1 3 23 4 5 6 7 8 9	mamuval	$⊢ φ \to X F Y = (j \in M, i \in P ⟼ \underset{k \in N}{\sum_{R}} ((j X k) \cdot_{R} (k Y i)))$
35	34	tposeqd	$⊢ φ \to tpos (X F Y) = tpos (j \in M, i \in P ⟼ \underset{k \in N}{\sum_{R}} ((j X k) \cdot_{R} (k Y i)))$
36		tposmap	$⊢ Y \in (B^{(N \times P)}) \to tpos Y \in (B^{(P \times N)})$
37	9 36	syl	$⊢ φ \to tpos Y \in (B^{(P \times N)})$
38		tposmap	$⊢ X \in (B^{(M \times N)}) \to tpos X \in (B^{(N \times M)})$
39	8 38	syl	$⊢ φ \to tpos X \in (B^{(N \times M)})$
40	2 3 23 4 7 6 5 37 39	mamuval	$⊢ φ \to tpos Y G tpos X = (i \in P, j \in M ⟼ \underset{k \in N}{\sum_{R}} ((i tpos Y k) \cdot_{R} (k tpos X j)))$
41	33 35 40	3eqtr4d	$⊢ φ \to tpos (X F Y) = tpos Y G tpos X$

Metamath Proof Explorer

Theorem mamutpos

Proof