mamulid

Description: The identity matrix (as operation in maps-to notation) is a left identity (for any matrix with the same number of rows). (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$
	mamulid.f	$⊢ F = R maMul ⟨M, M, N⟩$
	mamulid.x	$⊢ φ \to X \in (B^{(M \times N)})$
Assertion	mamulid	$⊢ φ \to I F X = 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		mamulid.f	$⊢ F = R maMul ⟨M, M, N⟩$
9		mamulid.x	$⊢ φ \to X \in (B^{(M \times N)})$
10		eqid	$⊢ \cdot_{R} = \cdot_{R}$
11	2	adantr	$⊢ (φ \land (l \in M \land k \in N)) \to R \in Ring$
12	6	adantr	$⊢ (φ \land (l \in M \land k \in N)) \to M \in Fin$
13	7	adantr	$⊢ (φ \land (l \in M \land k \in N)) \to N \in Fin$
14	1 2 3 4 5 6	mamumat1cl	$⊢ φ \to I \in (B^{(M \times M)})$
15	14	adantr	$⊢ (φ \land (l \in M \land k \in N)) \to I \in (B^{(M \times M)})$
16	9	adantr	$⊢ (φ \land (l \in M \land k \in N)) \to X \in (B^{(M \times N)})$
17		simprl	$⊢ (φ \land (l \in M \land k \in N)) \to l \in M$
18		simprr	$⊢ (φ \land (l \in M \land k \in N)) \to k \in N$
19	8 1 10 11 12 12 13 15 16 17 18	mamufv	$⊢ (φ \land (l \in M \land k \in N)) \to l (I F X) k = \underset{m \in M}{\sum_{R}} ((l I m) \cdot_{R} (m X k))$
20		ringmnd	$⊢ R \in Ring \to R \in Mnd$
21	11 20	syl	$⊢ (φ \land (l \in M \land k \in N)) \to R \in Mnd$
22	2	ad2antrr	$⊢ ((φ \land (l \in M \land k \in N)) \land m \in M) \to R \in Ring$
23		elmapi	$⊢ I \in (B^{(M \times M)}) \to I : M \times M ⟶ B$
24	14 23	syl	$⊢ φ \to I : M \times M ⟶ B$
25	24	ad2antrr	$⊢ ((φ \land (l \in M \land k \in N)) \land m \in M) \to I : M \times M ⟶ B$
26		simplrl	$⊢ ((φ \land (l \in M \land k \in N)) \land m \in M) \to l \in M$
27		simpr	$⊢ ((φ \land (l \in M \land k \in N)) \land m \in M) \to m \in M$
28	25 26 27	fovcdmd	$⊢ ((φ \land (l \in M \land k \in N)) \land m \in M) \to l I m \in B$
29		elmapi	$⊢ X \in (B^{(M \times N)}) \to X : M \times N ⟶ B$
30	9 29	syl	$⊢ φ \to X : M \times N ⟶ B$
31	30	ad2antrr	$⊢ ((φ \land (l \in M \land k \in N)) \land m \in M) \to X : M \times N ⟶ B$
32		simplrr	$⊢ ((φ \land (l \in M \land k \in N)) \land m \in M) \to k \in N$
33	31 27 32	fovcdmd	$⊢ ((φ \land (l \in M \land k \in N)) \land m \in M) \to m X k \in B$
34	1 10	ringcl	$⊢ (R \in Ring \land l I m \in B \land m X k \in B) \to (l I m) \cdot_{R} (m X k) \in B$
35	22 28 33 34	syl3anc	$⊢ ((φ \land (l \in M \land k \in N)) \land m \in M) \to (l I m) \cdot_{R} (m X k) \in B$
36	35	fmpttd	$⊢ (φ \land (l \in M \land k \in N)) \to (m \in M ⟼ (l I m) \cdot_{R} (m X k)) : M ⟶ B$
37	26	3adant3	$⊢ ((φ \land (l \in M \land k \in N)) \land m \in M \land m \neq l) \to l \in M$
38		simp2	$⊢ ((φ \land (l \in M \land k \in N)) \land m \in M \land m \neq l) \to m \in M$
39	1 2 3 4 5 6	mat1comp	$⊢ (l \in M \land m \in M) \to l I m = if (l = m, \underset{˙}{1}, \underset{˙}{0})$
40		equcom	$⊢ l = m \leftrightarrow m = l$
41	40	a1i	$⊢ (l \in M \land m \in M) \to (l = m \leftrightarrow m = l)$
42	41	ifbid	$⊢ (l \in M \land m \in M) \to if (l = m, \underset{˙}{1}, \underset{˙}{0}) = if (m = l, \underset{˙}{1}, \underset{˙}{0})$
43	39 42	eqtrd	$⊢ (l \in M \land m \in M) \to l I m = if (m = l, \underset{˙}{1}, \underset{˙}{0})$
44	37 38 43	syl2anc	$⊢ ((φ \land (l \in M \land k \in N)) \land m \in M \land m \neq l) \to l I m = if (m = l, \underset{˙}{1}, \underset{˙}{0})$
45		ifnefalse	$⊢ m \neq l \to if (m = l, \underset{˙}{1}, \underset{˙}{0}) = \underset{˙}{0}$
46	45	3ad2ant3	$⊢ ((φ \land (l \in M \land k \in N)) \land m \in M \land m \neq l) \to if (m = l, \underset{˙}{1}, \underset{˙}{0}) = \underset{˙}{0}$
47	44 46	eqtrd	$⊢ ((φ \land (l \in M \land k \in N)) \land m \in M \land m \neq l) \to l I m = \underset{˙}{0}$
48	47	oveq1d	$⊢ ((φ \land (l \in M \land k \in N)) \land m \in M \land m \neq l) \to (l I m) \cdot_{R} (m X k) = \underset{˙}{0} \cdot_{R} (m X k)$
49	1 10 4	ringlz	$⊢ (R \in Ring \land m X k \in B) \to \underset{˙}{0} \cdot_{R} (m X k) = \underset{˙}{0}$
50	22 33 49	syl2anc	$⊢ ((φ \land (l \in M \land k \in N)) \land m \in M) \to \underset{˙}{0} \cdot_{R} (m X k) = \underset{˙}{0}$
51	50	3adant3	$⊢ ((φ \land (l \in M \land k \in N)) \land m \in M \land m \neq l) \to \underset{˙}{0} \cdot_{R} (m X k) = \underset{˙}{0}$
52	48 51	eqtrd	$⊢ ((φ \land (l \in M \land k \in N)) \land m \in M \land m \neq l) \to (l I m) \cdot_{R} (m X k) = \underset{˙}{0}$
53	52 12	suppsssn	$⊢ (φ \land (l \in M \land k \in N)) \to (m \in M ⟼ (l I m) \cdot_{R} (m X k)) supp \underset{˙}{0} \subseteq \{l\}$
54	1 4 21 12 17 36 53	gsumpt	$⊢ (φ \land (l \in M \land k \in N)) \to \underset{m \in M}{\sum_{R}} ((l I m) \cdot_{R} (m X k)) = (m \in M ⟼ (l I m) \cdot_{R} (m X k)) (l)$
55		oveq2	$⊢ m = l \to l I m = l I l$
56		oveq1	$⊢ m = l \to m X k = l X k$
57	55 56	oveq12d	$⊢ m = l \to (l I m) \cdot_{R} (m X k) = (l I l) \cdot_{R} (l X k)$
58		eqid	$⊢ (m \in M ⟼ (l I m) \cdot_{R} (m X k)) = (m \in M ⟼ (l I m) \cdot_{R} (m X k))$
59		ovex	$⊢ (l I l) \cdot_{R} (l X k) \in V$
60	57 58 59	fvmpt	$⊢ l \in M \to (m \in M ⟼ (l I m) \cdot_{R} (m X k)) (l) = (l I l) \cdot_{R} (l X k)$
61	60	ad2antrl	$⊢ (φ \land (l \in M \land k \in N)) \to (m \in M ⟼ (l I m) \cdot_{R} (m X k)) (l) = (l I l) \cdot_{R} (l X k)$
62		equequ1	$⊢ i = l \to (i = j \leftrightarrow l = j)$
63	62	ifbid	$⊢ i = l \to if (i = j, \underset{˙}{1}, \underset{˙}{0}) = if (l = j, \underset{˙}{1}, \underset{˙}{0})$
64		equequ2	$⊢ j = l \to (l = j \leftrightarrow l = l)$
65	64	ifbid	$⊢ j = l \to if (l = j, \underset{˙}{1}, \underset{˙}{0}) = if (l = l, \underset{˙}{1}, \underset{˙}{0})$
66		equid	$⊢ l = l$
67	66	iftruei	$⊢ if (l = l, \underset{˙}{1}, \underset{˙}{0}) = \underset{˙}{1}$
68	65 67	eqtrdi	$⊢ j = l \to if (l = j, \underset{˙}{1}, \underset{˙}{0}) = \underset{˙}{1}$
69	3	fvexi	$⊢ \underset{˙}{1} \in V$
70	63 68 5 69	ovmpo	$⊢ (l \in M \land l \in M) \to l I l = \underset{˙}{1}$
71	70	anidms	$⊢ l \in M \to l I l = \underset{˙}{1}$
72	71	ad2antrl	$⊢ (φ \land (l \in M \land k \in N)) \to l I l = \underset{˙}{1}$
73	72	oveq1d	$⊢ (φ \land (l \in M \land k \in N)) \to (l I l) \cdot_{R} (l X k) = \underset{˙}{1} \cdot_{R} (l X k)$
74	30	fovcdmda	$⊢ (φ \land (l \in M \land k \in N)) \to l X k \in B$
75	1 10 3	ringlidm	$⊢ (R \in Ring \land l X k \in B) \to \underset{˙}{1} \cdot_{R} (l X k) = l X k$
76	11 74 75	syl2anc	$⊢ (φ \land (l \in M \land k \in N)) \to \underset{˙}{1} \cdot_{R} (l X k) = l X k$
77	61 73 76	3eqtrd	$⊢ (φ \land (l \in M \land k \in N)) \to (m \in M ⟼ (l I m) \cdot_{R} (m X k)) (l) = l X k$
78	19 54 77	3eqtrd	$⊢ (φ \land (l \in M \land k \in N)) \to l (I F X) k = l X k$
79	78	ralrimivva	$⊢ φ \to \forall l \in M \forall k \in N l (I F X) k = l X k$
80	1 2 8 6 6 7 14 9	mamucl	$⊢ φ \to I F X \in (B^{(M \times N)})$
81		elmapi	$⊢ I F X \in (B^{(M \times N)}) \to (I F X) : M \times N ⟶ B$
82	80 81	syl	$⊢ φ \to (I F X) : M \times N ⟶ B$
83	82	ffnd	$⊢ φ \to (I F X) Fn (M \times N)$
84	30	ffnd	$⊢ φ \to X Fn (M \times N)$
85		eqfnov2	$⊢ ((I F X) Fn (M \times N) \land X Fn (M \times N)) \to (I F X = X \leftrightarrow \forall l \in M \forall k \in N l (I F X) k = l X k)$
86	83 84 85	syl2anc	$⊢ φ \to (I F X = X \leftrightarrow \forall l \in M \forall k \in N l (I F X) k = l X k)$
87	79 86	mpbird	$⊢ φ \to I F X = X$

Metamath Proof Explorer

Theorem mamulid

Proof