mamurid

Description: The identity matrix (as operation in maps-to notation) is a right identity (for any matrix with the same number of columns). (Contributed by Stefan O'Rear, 3-Sep-2015) (Proof shortened by AV, 22-Jul-2019)

	Ref	Expression
Hypotheses	mamumat1cl.b	$⊢ B = {Base}_{R}$
	mamumat1cl.r	$⊢ φ \to R \in Ring$
	mamumat1cl.o	$⊢ \underset{˙}{1} = 1_{R}$
	mamumat1cl.z	$⊢ \underset{˙}{0} = 0_{R}$
	mamumat1cl.i	$⊢ I = (i \in M, j \in M ⟼ if (i = j, \underset{˙}{1}, \underset{˙}{0}))$
	mamumat1cl.m	$⊢ φ \to M \in Fin$
	mamulid.n	$⊢ φ \to N \in Fin$
	mamurid.f	$⊢ F = R maMul ⟨N, M, M⟩$
	mamurid.x	$⊢ φ \to X \in (B^{(N \times M)})$
Assertion	mamurid	$⊢ φ \to X F I = X$

Proof

Step	Hyp	Ref	Expression
1		mamumat1cl.b	$⊢ B = {Base}_{R}$
2		mamumat1cl.r	$⊢ φ \to R \in Ring$
3		mamumat1cl.o	$⊢ \underset{˙}{1} = 1_{R}$
4		mamumat1cl.z	$⊢ \underset{˙}{0} = 0_{R}$
5		mamumat1cl.i	$⊢ I = (i \in M, j \in M ⟼ if (i = j, \underset{˙}{1}, \underset{˙}{0}))$
6		mamumat1cl.m	$⊢ φ \to M \in Fin$
7		mamulid.n	$⊢ φ \to N \in Fin$
8		mamurid.f	$⊢ F = R maMul ⟨N, M, M⟩$
9		mamurid.x	$⊢ φ \to X \in (B^{(N \times M)})$
10		eqid	$⊢ \cdot_{R} = \cdot_{R}$
11	2	adantr	$⊢ (φ \land (l \in N \land m \in M)) \to R \in Ring$
12	7	adantr	$⊢ (φ \land (l \in N \land m \in M)) \to N \in Fin$
13	6	adantr	$⊢ (φ \land (l \in N \land m \in M)) \to M \in Fin$
14	9	adantr	$⊢ (φ \land (l \in N \land m \in M)) \to X \in (B^{(N \times M)})$
15	1 2 3 4 5 6	mamumat1cl	$⊢ φ \to I \in (B^{(M \times M)})$
16	15	adantr	$⊢ (φ \land (l \in N \land m \in M)) \to I \in (B^{(M \times M)})$
17		simprl	$⊢ (φ \land (l \in N \land m \in M)) \to l \in N$
18		simprr	$⊢ (φ \land (l \in N \land m \in M)) \to m \in M$
19	8 1 10 11 12 13 13 14 16 17 18	mamufv	$⊢ (φ \land (l \in N \land m \in M)) \to l (X F I) m = \underset{k \in M}{\sum_{R}} ((l X k) \cdot_{R} (k I m))$
20		ringmnd	$⊢ R \in Ring \to R \in Mnd$
21	11 20	syl	$⊢ (φ \land (l \in N \land m \in M)) \to R \in Mnd$
22	2	ad2antrr	$⊢ ((φ \land (l \in N \land m \in M)) \land k \in M) \to R \in Ring$
23		elmapi	$⊢ X \in (B^{(N \times M)}) \to X : N \times M ⟶ B$
24	9 23	syl	$⊢ φ \to X : N \times M ⟶ B$
25	24	ad2antrr	$⊢ ((φ \land (l \in N \land m \in M)) \land k \in M) \to X : N \times M ⟶ B$
26		simplrl	$⊢ ((φ \land (l \in N \land m \in M)) \land k \in M) \to l \in N$
27		simpr	$⊢ ((φ \land (l \in N \land m \in M)) \land k \in M) \to k \in M$
28	25 26 27	fovcdmd	$⊢ ((φ \land (l \in N \land m \in M)) \land k \in M) \to l X k \in B$
29		elmapi	$⊢ I \in (B^{(M \times M)}) \to I : M \times M ⟶ B$
30	15 29	syl	$⊢ φ \to I : M \times M ⟶ B$
31	30	ad2antrr	$⊢ ((φ \land (l \in N \land m \in M)) \land k \in M) \to I : M \times M ⟶ B$
32		simplrr	$⊢ ((φ \land (l \in N \land m \in M)) \land k \in M) \to m \in M$
33	31 27 32	fovcdmd	$⊢ ((φ \land (l \in N \land m \in M)) \land k \in M) \to k I m \in B$
34	1 10	ringcl	$⊢ (R \in Ring \land l X k \in B \land k I m \in B) \to (l X k) \cdot_{R} (k I m) \in B$
35	22 28 33 34	syl3anc	$⊢ ((φ \land (l \in N \land m \in M)) \land k \in M) \to (l X k) \cdot_{R} (k I m) \in B$
36	35	fmpttd	$⊢ (φ \land (l \in N \land m \in M)) \to (k \in M ⟼ (l X k) \cdot_{R} (k I m)) : M ⟶ B$
37		simp2	$⊢ ((φ \land (l \in N \land m \in M)) \land k \in M \land k \neq m) \to k \in M$
38	32	3adant3	$⊢ ((φ \land (l \in N \land m \in M)) \land k \in M \land k \neq m) \to m \in M$
39	1 2 3 4 5 6	mat1comp	$⊢ (k \in M \land m \in M) \to k I m = if (k = m, \underset{˙}{1}, \underset{˙}{0})$
40	37 38 39	syl2anc	$⊢ ((φ \land (l \in N \land m \in M)) \land k \in M \land k \neq m) \to k I m = if (k = m, \underset{˙}{1}, \underset{˙}{0})$
41		ifnefalse	$⊢ k \neq m \to if (k = m, \underset{˙}{1}, \underset{˙}{0}) = \underset{˙}{0}$
42	41	3ad2ant3	$⊢ ((φ \land (l \in N \land m \in M)) \land k \in M \land k \neq m) \to if (k = m, \underset{˙}{1}, \underset{˙}{0}) = \underset{˙}{0}$
43	40 42	eqtrd	$⊢ ((φ \land (l \in N \land m \in M)) \land k \in M \land k \neq m) \to k I m = \underset{˙}{0}$
44	43	oveq2d	$⊢ ((φ \land (l \in N \land m \in M)) \land k \in M \land k \neq m) \to (l X k) \cdot_{R} (k I m) = (l X k) \cdot_{R} \underset{˙}{0}$
45	1 10 4	ringrz	$⊢ (R \in Ring \land l X k \in B) \to (l X k) \cdot_{R} \underset{˙}{0} = \underset{˙}{0}$
46	22 28 45	syl2anc	$⊢ ((φ \land (l \in N \land m \in M)) \land k \in M) \to (l X k) \cdot_{R} \underset{˙}{0} = \underset{˙}{0}$
47	46	3adant3	$⊢ ((φ \land (l \in N \land m \in M)) \land k \in M \land k \neq m) \to (l X k) \cdot_{R} \underset{˙}{0} = \underset{˙}{0}$
48	44 47	eqtrd	$⊢ ((φ \land (l \in N \land m \in M)) \land k \in M \land k \neq m) \to (l X k) \cdot_{R} (k I m) = \underset{˙}{0}$
49	48 13	suppsssn	$⊢ (φ \land (l \in N \land m \in M)) \to (k \in M ⟼ (l X k) \cdot_{R} (k I m)) supp \underset{˙}{0} \subseteq \{m\}$
50	1 4 21 13 18 36 49	gsumpt	$⊢ (φ \land (l \in N \land m \in M)) \to \underset{k \in M}{\sum_{R}} ((l X k) \cdot_{R} (k I m)) = (k \in M ⟼ (l X k) \cdot_{R} (k I m)) (m)$
51		oveq2	$⊢ k = m \to l X k = l X m$
52		oveq1	$⊢ k = m \to k I m = m I m$
53	51 52	oveq12d	$⊢ k = m \to (l X k) \cdot_{R} (k I m) = (l X m) \cdot_{R} (m I m)$
54		eqid	$⊢ (k \in M ⟼ (l X k) \cdot_{R} (k I m)) = (k \in M ⟼ (l X k) \cdot_{R} (k I m))$
55		ovex	$⊢ (l X m) \cdot_{R} (m I m) \in V$
56	53 54 55	fvmpt	$⊢ m \in M \to (k \in M ⟼ (l X k) \cdot_{R} (k I m)) (m) = (l X m) \cdot_{R} (m I m)$
57	56	ad2antll	$⊢ (φ \land (l \in N \land m \in M)) \to (k \in M ⟼ (l X k) \cdot_{R} (k I m)) (m) = (l X m) \cdot_{R} (m I m)$
58		equequ1	$⊢ i = m \to (i = j \leftrightarrow m = j)$
59	58	ifbid	$⊢ i = m \to if (i = j, \underset{˙}{1}, \underset{˙}{0}) = if (m = j, \underset{˙}{1}, \underset{˙}{0})$
60		equequ2	$⊢ j = m \to (m = j \leftrightarrow m = m)$
61	60	ifbid	$⊢ j = m \to if (m = j, \underset{˙}{1}, \underset{˙}{0}) = if (m = m, \underset{˙}{1}, \underset{˙}{0})$
62		eqid	$⊢ m = m$
63	62	iftruei	$⊢ if (m = m, \underset{˙}{1}, \underset{˙}{0}) = \underset{˙}{1}$
64	61 63	eqtrdi	$⊢ j = m \to if (m = j, \underset{˙}{1}, \underset{˙}{0}) = \underset{˙}{1}$
65	3	fvexi	$⊢ \underset{˙}{1} \in V$
66	59 64 5 65	ovmpo	$⊢ (m \in M \land m \in M) \to m I m = \underset{˙}{1}$
67	66	anidms	$⊢ m \in M \to m I m = \underset{˙}{1}$
68	67	oveq2d	$⊢ m \in M \to (l X m) \cdot_{R} (m I m) = (l X m) \cdot_{R} \underset{˙}{1}$
69	68	ad2antll	$⊢ (φ \land (l \in N \land m \in M)) \to (l X m) \cdot_{R} (m I m) = (l X m) \cdot_{R} \underset{˙}{1}$
70	24	fovcdmda	$⊢ (φ \land (l \in N \land m \in M)) \to l X m \in B$
71	1 10 3	ringridm	$⊢ (R \in Ring \land l X m \in B) \to (l X m) \cdot_{R} \underset{˙}{1} = l X m$
72	11 70 71	syl2anc	$⊢ (φ \land (l \in N \land m \in M)) \to (l X m) \cdot_{R} \underset{˙}{1} = l X m$
73	57 69 72	3eqtrd	$⊢ (φ \land (l \in N \land m \in M)) \to (k \in M ⟼ (l X k) \cdot_{R} (k I m)) (m) = l X m$
74	19 50 73	3eqtrd	$⊢ (φ \land (l \in N \land m \in M)) \to l (X F I) m = l X m$
75	74	ralrimivva	$⊢ φ \to \forall l \in N \forall m \in M l (X F I) m = l X m$
76	1 2 8 7 6 6 9 15	mamucl	$⊢ φ \to X F I \in (B^{(N \times M)})$
77		elmapi	$⊢ X F I \in (B^{(N \times M)}) \to (X F I) : N \times M ⟶ B$
78	76 77	syl	$⊢ φ \to (X F I) : N \times M ⟶ B$
79	78	ffnd	$⊢ φ \to (X F I) Fn (N \times M)$
80	24	ffnd	$⊢ φ \to X Fn (N \times M)$
81		eqfnov2	$⊢ ((X F I) Fn (N \times M) \land X Fn (N \times M)) \to (X F I = X \leftrightarrow \forall l \in N \forall m \in M l (X F I) m = l X m)$
82	79 80 81	syl2anc	$⊢ φ \to (X F I = X \leftrightarrow \forall l \in N \forall m \in M l (X F I) m = l X m)$
83	75 82	mpbird	$⊢ φ \to X F I = X$

Metamath Proof Explorer

Theorem mamurid

Proof