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 = Base R
mamumat1cl.r φ R Ring
mamumat1cl.o 1 ˙ = 1 R
mamumat1cl.z 0 ˙ = 0 R
mamumat1cl.i I = i M , j M if i = j 1 ˙ 0 ˙
mamumat1cl.m φ M Fin
mamulid.n φ N Fin
mamurid.f F = R maMul N M M
mamurid.x φ X B N × M
Assertion mamurid φ X F I = X

Proof

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