mamures

Description: Rows in a matrix product are functions only of the corresponding rows in the left argument. (Contributed by SO, 9-Jul-2018)

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

Proof

Step	Hyp	Ref	Expression
1		mamures.f	$⊢ F = R maMul ⟨M, N, P⟩$
2		mamures.g	$⊢ G = R maMul ⟨I, N, P⟩$
3		mamures.b	$⊢ B = {Base}_{R}$
4		mamures.r	$⊢ φ \to R \in V$
5		mamures.m	$⊢ φ \to M \in Fin$
6		mamures.n	$⊢ φ \to N \in Fin$
7		mamures.p	$⊢ φ \to P \in Fin$
8		mamures.i	$⊢ φ \to I \subseteq M$
9		mamures.x	$⊢ φ \to X \in (B^{(M \times N)})$
10		mamures.y	$⊢ φ \to Y \in (B^{(N \times P)})$
11		ssidd	$⊢ φ \to P \subseteq P$
12		resmpo	$⊢ (I \subseteq M \land P \subseteq P) \to {(i \in M, j \in P ⟼ \underset{k \in N}{\sum_{R}} ((i X k) \cdot_{R} (k Y j))) ↾}_{(I \times P)} = (i \in I, j \in P ⟼ \underset{k \in N}{\sum_{R}} ((i X k) \cdot_{R} (k Y j)))$
13	8 11 12	syl2anc	$⊢ φ \to {(i \in M, j \in P ⟼ \underset{k \in N}{\sum_{R}} ((i X k) \cdot_{R} (k Y j))) ↾}_{(I \times P)} = (i \in I, j \in P ⟼ \underset{k \in N}{\sum_{R}} ((i X k) \cdot_{R} (k Y j)))$
14		ovres	$⊢ (i \in I \land k \in N) \to i ({X ↾}_{(I \times N)}) k = i X k$
15	14	3ad2antl2	$⊢ ((φ \land i \in I \land j \in P) \land k \in N) \to i ({X ↾}_{(I \times N)}) k = i X k$
16	15	eqcomd	$⊢ ((φ \land i \in I \land j \in P) \land k \in N) \to i X k = i ({X ↾}_{(I \times N)}) k$
17	16	oveq1d	$⊢ ((φ \land i \in I \land j \in P) \land k \in N) \to (i X k) \cdot_{R} (k Y j) = (i ({X ↾}_{(I \times N)}) k) \cdot_{R} (k Y j)$
18	17	mpteq2dva	$⊢ (φ \land i \in I \land j \in P) \to (k \in N ⟼ (i X k) \cdot_{R} (k Y j)) = (k \in N ⟼ (i ({X ↾}_{(I \times N)}) k) \cdot_{R} (k Y j))$
19	18	oveq2d	$⊢ (φ \land i \in I \land j \in P) \to \underset{k \in N}{\sum_{R}} ((i X k) \cdot_{R} (k Y j)) = \underset{k \in N}{\sum_{R}} ((i ({X ↾}_{(I \times N)}) k) \cdot_{R} (k Y j))$
20	19	mpoeq3dva	$⊢ φ \to (i \in I, j \in P ⟼ \underset{k \in N}{\sum_{R}} ((i X k) \cdot_{R} (k Y j))) = (i \in I, j \in P ⟼ \underset{k \in N}{\sum_{R}} ((i ({X ↾}_{(I \times N)}) k) \cdot_{R} (k Y j)))$
21	13 20	eqtrd	$⊢ φ \to {(i \in M, j \in P ⟼ \underset{k \in N}{\sum_{R}} ((i X k) \cdot_{R} (k Y j))) ↾}_{(I \times P)} = (i \in I, j \in P ⟼ \underset{k \in N}{\sum_{R}} ((i ({X ↾}_{(I \times N)}) k) \cdot_{R} (k Y j)))$
22		eqid	$⊢ \cdot_{R} = \cdot_{R}$
23	1 3 22 4 5 6 7 9 10	mamuval	$⊢ φ \to X F Y = (i \in M, j \in P ⟼ \underset{k \in N}{\sum_{R}} ((i X k) \cdot_{R} (k Y j)))$
24	23	reseq1d	$⊢ φ \to {(X F Y) ↾}_{(I \times P)} = {(i \in M, j \in P ⟼ \underset{k \in N}{\sum_{R}} ((i X k) \cdot_{R} (k Y j))) ↾}_{(I \times P)}$
25	5 8	ssfid	$⊢ φ \to I \in Fin$
26		elmapi	$⊢ X \in (B^{(M \times N)}) \to X : M \times N ⟶ B$
27	9 26	syl	$⊢ φ \to X : M \times N ⟶ B$
28		xpss1	$⊢ I \subseteq M \to I \times N \subseteq M \times N$
29	8 28	syl	$⊢ φ \to I \times N \subseteq M \times N$
30	27 29	fssresd	$⊢ φ \to ({X ↾}_{(I \times N)}) : I \times N ⟶ B$
31	3	fvexi	$⊢ B \in V$
32	31	a1i	$⊢ φ \to B \in V$
33		xpfi	$⊢ (I \in Fin \land N \in Fin) \to I \times N \in Fin$
34	25 6 33	syl2anc	$⊢ φ \to I \times N \in Fin$
35	32 34	elmapd	$⊢ φ \to ({X ↾}_{(I \times N)} \in (B^{(I \times N)}) \leftrightarrow ({X ↾}_{(I \times N)}) : I \times N ⟶ B)$
36	30 35	mpbird	$⊢ φ \to {X ↾}_{(I \times N)} \in (B^{(I \times N)})$
37	2 3 22 4 25 6 7 36 10	mamuval	$⊢ φ \to ({X ↾}_{(I \times N)}) G Y = (i \in I, j \in P ⟼ \underset{k \in N}{\sum_{R}} ((i ({X ↾}_{(I \times N)}) k) \cdot_{R} (k Y j)))$
38	21 24 37	3eqtr4d	$⊢ φ \to {(X F Y) ↾}_{(I \times P)} = ({X ↾}_{(I \times N)}) G Y$

Metamath Proof Explorer

Theorem mamures

Proof