Metamath Proof Explorer

Theorem 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 
|- ( ph -> R e. Ring )
mamumat1cl.o 
|- .1. = ( 1r ` R )
mamumat1cl.z 
|- .0. = ( 0g ` R )
mamumat1cl.i 
|- I = ( i e. M , j e. M |-> if ( i = j , .1. , .0. ) )
mamumat1cl.m 
|- ( ph -> M e. Fin )
mamulid.n 
|- ( ph -> N e. Fin )
mamulid.f 
|- F = ( R maMul <. M , M , N >. )
mamulid.x 
|- ( ph -> X e. ( B ^m ( M X. N ) ) )
Assertion mamulid 
|- ( ph -> ( I F X ) = X )

Proof

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