# Metamath Proof Explorer

## Theorem 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}={\mathrm{Base}}_{{R}}$
mamumat1cl.r ${⊢}{\phi }\to {R}\in \mathrm{Ring}$
mamumat1cl.o
mamumat1cl.z
mamumat1cl.i
mamumat1cl.m ${⊢}{\phi }\to {M}\in \mathrm{Fin}$
mamulid.n ${⊢}{\phi }\to {N}\in \mathrm{Fin}$
mamurid.f ${⊢}{F}={R}\mathrm{maMul}⟨{N},{M},{M}⟩$
mamurid.x ${⊢}{\phi }\to {X}\in \left({{B}}^{\left({N}×{M}\right)}\right)$
Assertion mamurid ${⊢}{\phi }\to {X}{F}{I}={X}$

### Proof

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