mamucl

Description: Operation closure of matrix multiplication. (Contributed by Stefan O'Rear, 2-Sep-2015) (Proof shortened by AV, 23-Jul-2019)

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

Proof

Step	Hyp	Ref	Expression
1		mamucl.b	$⊢ B = {Base}_{R}$
2		mamucl.r	$⊢ φ \to R \in Ring$
3		mamucl.f	$⊢ F = R maMul ⟨M, N, P⟩$
4		mamucl.m	$⊢ φ \to M \in Fin$
5		mamucl.n	$⊢ φ \to N \in Fin$
6		mamucl.p	$⊢ φ \to P \in Fin$
7		mamucl.x	$⊢ φ \to X \in (B^{(M \times N)})$
8		mamucl.y	$⊢ φ \to Y \in (B^{(N \times P)})$
9		eqid	$⊢ \cdot_{R} = \cdot_{R}$
10	3 1 9 2 4 5 6 7 8	mamuval	$⊢ φ \to X F Y = (i \in M, k \in P ⟼ \underset{j \in N}{\sum_{R}} ((i X j) \cdot_{R} (j Y k)))$
11		ringcmn	$⊢ R \in Ring \to R \in CMnd$
12	2 11	syl	$⊢ φ \to R \in CMnd$
13	12	adantr	$⊢ (φ \land (i \in M \land k \in P)) \to R \in CMnd$
14	5	adantr	$⊢ (φ \land (i \in M \land k \in P)) \to N \in Fin$
15	2	ad2antrr	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in N) \to R \in Ring$
16		elmapi	$⊢ X \in (B^{(M \times N)}) \to X : M \times N ⟶ B$
17	7 16	syl	$⊢ φ \to X : M \times N ⟶ B$
18	17	ad2antrr	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in N) \to X : M \times N ⟶ B$
19		simplrl	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in N) \to i \in M$
20		simpr	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in N) \to j \in N$
21	18 19 20	fovrnd	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in N) \to i X j \in B$
22		elmapi	$⊢ Y \in (B^{(N \times P)}) \to Y : N \times P ⟶ B$
23	8 22	syl	$⊢ φ \to Y : N \times P ⟶ B$
24	23	ad2antrr	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in N) \to Y : N \times P ⟶ B$
25		simplrr	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in N) \to k \in P$
26	24 20 25	fovrnd	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in N) \to j Y k \in B$
27	1 9	ringcl	$⊢ (R \in Ring \land i X j \in B \land j Y k \in B) \to (i X j) \cdot_{R} (j Y k) \in B$
28	15 21 26 27	syl3anc	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in N) \to (i X j) \cdot_{R} (j Y k) \in B$
29	28	ralrimiva	$⊢ (φ \land (i \in M \land k \in P)) \to \forall j \in N (i X j) \cdot_{R} (j Y k) \in B$
30	1 13 14 29	gsummptcl	$⊢ (φ \land (i \in M \land k \in P)) \to \underset{j \in N}{\sum_{R}} ((i X j) \cdot_{R} (j Y k)) \in B$
31	30	ralrimivva	$⊢ φ \to \forall i \in M \forall k \in P \underset{j \in N}{\sum_{R}} ((i X j) \cdot_{R} (j Y k)) \in B$
32		eqid	$⊢ (i \in M, k \in P ⟼ \underset{j \in N}{\sum_{R}} ((i X j) \cdot_{R} (j Y k))) = (i \in M, k \in P ⟼ \underset{j \in N}{\sum_{R}} ((i X j) \cdot_{R} (j Y k)))$
33	32	fmpo	$⊢ \forall i \in M \forall k \in P \underset{j \in N}{\sum_{R}} ((i X j) \cdot_{R} (j Y k)) \in B \leftrightarrow (i \in M, k \in P ⟼ \underset{j \in N}{\sum_{R}} ((i X j) \cdot_{R} (j Y k))) : M \times P ⟶ B$
34	1	fvexi	$⊢ B \in V$
35		xpfi	$⊢ (M \in Fin \land P \in Fin) \to M \times P \in Fin$
36	4 6 35	syl2anc	$⊢ φ \to M \times P \in Fin$
37		elmapg	$⊢ (B \in V \land M \times P \in Fin) \to ((i \in M, k \in P ⟼ \underset{j \in N}{\sum_{R}} ((i X j) \cdot_{R} (j Y k))) \in (B^{(M \times P)}) \leftrightarrow (i \in M, k \in P ⟼ \underset{j \in N}{\sum_{R}} ((i X j) \cdot_{R} (j Y k))) : M \times P ⟶ B)$
38	34 36 37	sylancr	$⊢ φ \to ((i \in M, k \in P ⟼ \underset{j \in N}{\sum_{R}} ((i X j) \cdot_{R} (j Y k))) \in (B^{(M \times P)}) \leftrightarrow (i \in M, k \in P ⟼ \underset{j \in N}{\sum_{R}} ((i X j) \cdot_{R} (j Y k))) : M \times P ⟶ B)$
39	33 38	bitr4id	$⊢ φ \to (\forall i \in M \forall k \in P \underset{j \in N}{\sum_{R}} ((i X j) \cdot_{R} (j Y k)) \in B \leftrightarrow (i \in M, k \in P ⟼ \underset{j \in N}{\sum_{R}} ((i X j) \cdot_{R} (j Y k))) \in (B^{(M \times P)}))$
40	31 39	mpbid	$⊢ φ \to (i \in M, k \in P ⟼ \underset{j \in N}{\sum_{R}} ((i X j) \cdot_{R} (j Y k))) \in (B^{(M \times P)})$
41	10 40	eqeltrd	$⊢ φ \to X F Y \in (B^{(M \times P)})$

Metamath Proof Explorer

Theorem mamucl

Proof