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 
|- ( 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 )
mamurid.f 
|- F = ( R maMul <. N , M , M >. )
mamurid.x 
|- ( ph -> X e. ( B ^m ( N X. M ) ) )
Assertion mamurid 
|- ( ph -> ( X F I ) = 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 mamurid.f 
 |-  F = ( R maMul <. N , M , M >. )
9 mamurid.x 
 |-  ( ph -> X e. ( B ^m ( N X. M ) ) )
10 eqid 
 |-  ( .r ` R ) = ( .r ` R )
11 2 adantr 
 |-  ( ( ph /\ ( l e. N /\ m e. M ) ) -> R e. Ring )
12 7 adantr 
 |-  ( ( ph /\ ( l e. N /\ m e. M ) ) -> N e. Fin )
13 6 adantr 
 |-  ( ( ph /\ ( l e. N /\ m e. M ) ) -> M e. Fin )
14 9 adantr 
 |-  ( ( ph /\ ( l e. N /\ m e. M ) ) -> X e. ( B ^m ( N X. M ) ) )
15 1 2 3 4 5 6 mamumat1cl 
 |-  ( ph -> I e. ( B ^m ( M X. M ) ) )
16 15 adantr 
 |-  ( ( ph /\ ( l e. N /\ m e. M ) ) -> I e. ( B ^m ( M X. M ) ) )
17 simprl 
 |-  ( ( ph /\ ( l e. N /\ m e. M ) ) -> l e. N )
18 simprr 
 |-  ( ( ph /\ ( l e. N /\ m e. M ) ) -> m e. M )
19 8 1 10 11 12 13 13 14 16 17 18 mamufv 
 |-  ( ( ph /\ ( l e. N /\ m e. M ) ) -> ( l ( X F I ) m ) = ( R gsum ( k e. M |-> ( ( l X k ) ( .r ` R ) ( k I m ) ) ) ) )
20 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
21 11 20 syl 
 |-  ( ( ph /\ ( l e. N /\ m e. M ) ) -> R e. Mnd )
22 2 ad2antrr 
 |-  ( ( ( ph /\ ( l e. N /\ m e. M ) ) /\ k e. M ) -> R e. Ring )
23 elmapi 
 |-  ( X e. ( B ^m ( N X. M ) ) -> X : ( N X. M ) --> B )
24 9 23 syl 
 |-  ( ph -> X : ( N X. M ) --> B )
25 24 ad2antrr 
 |-  ( ( ( ph /\ ( l e. N /\ m e. M ) ) /\ k e. M ) -> X : ( N X. M ) --> B )
26 simplrl 
 |-  ( ( ( ph /\ ( l e. N /\ m e. M ) ) /\ k e. M ) -> l e. N )
27 simpr 
 |-  ( ( ( ph /\ ( l e. N /\ m e. M ) ) /\ k e. M ) -> k e. M )
28 25 26 27 fovcdmd 
 |-  ( ( ( ph /\ ( l e. N /\ m e. M ) ) /\ k e. M ) -> ( l X k ) e. B )
29 elmapi 
 |-  ( I e. ( B ^m ( M X. M ) ) -> I : ( M X. M ) --> B )
30 15 29 syl 
 |-  ( ph -> I : ( M X. M ) --> B )
31 30 ad2antrr 
 |-  ( ( ( ph /\ ( l e. N /\ m e. M ) ) /\ k e. M ) -> I : ( M X. M ) --> B )
32 simplrr 
 |-  ( ( ( ph /\ ( l e. N /\ m e. M ) ) /\ k e. M ) -> m e. M )
33 31 27 32 fovcdmd 
 |-  ( ( ( ph /\ ( l e. N /\ m e. M ) ) /\ k e. M ) -> ( k I m ) e. B )
34 1 10 ringcl 
 |-  ( ( R e. Ring /\ ( l X k ) e. B /\ ( k I m ) e. B ) -> ( ( l X k ) ( .r ` R ) ( k I m ) ) e. B )
35 22 28 33 34 syl3anc 
 |-  ( ( ( ph /\ ( l e. N /\ m e. M ) ) /\ k e. M ) -> ( ( l X k ) ( .r ` R ) ( k I m ) ) e. B )
36 35 fmpttd 
 |-  ( ( ph /\ ( l e. N /\ m e. M ) ) -> ( k e. M |-> ( ( l X k ) ( .r ` R ) ( k I m ) ) ) : M --> B )
37 simp2 
 |-  ( ( ( ph /\ ( l e. N /\ m e. M ) ) /\ k e. M /\ k =/= m ) -> k e. M )
38 32 3adant3 
 |-  ( ( ( ph /\ ( l e. N /\ m e. M ) ) /\ k e. M /\ k =/= m ) -> m e. M )
39 1 2 3 4 5 6 mat1comp 
 |-  ( ( k e. M /\ m e. M ) -> ( k I m ) = if ( k = m , .1. , .0. ) )
40 37 38 39 syl2anc 
 |-  ( ( ( ph /\ ( l e. N /\ m e. M ) ) /\ k e. M /\ k =/= m ) -> ( k I m ) = if ( k = m , .1. , .0. ) )
41 ifnefalse 
 |-  ( k =/= m -> if ( k = m , .1. , .0. ) = .0. )
42 41 3ad2ant3 
 |-  ( ( ( ph /\ ( l e. N /\ m e. M ) ) /\ k e. M /\ k =/= m ) -> if ( k = m , .1. , .0. ) = .0. )
43 40 42 eqtrd 
 |-  ( ( ( ph /\ ( l e. N /\ m e. M ) ) /\ k e. M /\ k =/= m ) -> ( k I m ) = .0. )
44 43 oveq2d 
 |-  ( ( ( ph /\ ( l e. N /\ m e. M ) ) /\ k e. M /\ k =/= m ) -> ( ( l X k ) ( .r ` R ) ( k I m ) ) = ( ( l X k ) ( .r ` R ) .0. ) )
45 1 10 4 ringrz 
 |-  ( ( R e. Ring /\ ( l X k ) e. B ) -> ( ( l X k ) ( .r ` R ) .0. ) = .0. )
46 22 28 45 syl2anc 
 |-  ( ( ( ph /\ ( l e. N /\ m e. M ) ) /\ k e. M ) -> ( ( l X k ) ( .r ` R ) .0. ) = .0. )
47 46 3adant3 
 |-  ( ( ( ph /\ ( l e. N /\ m e. M ) ) /\ k e. M /\ k =/= m ) -> ( ( l X k ) ( .r ` R ) .0. ) = .0. )
48 44 47 eqtrd 
 |-  ( ( ( ph /\ ( l e. N /\ m e. M ) ) /\ k e. M /\ k =/= m ) -> ( ( l X k ) ( .r ` R ) ( k I m ) ) = .0. )
49 48 13 suppsssn 
 |-  ( ( ph /\ ( l e. N /\ m e. M ) ) -> ( ( k e. M |-> ( ( l X k ) ( .r ` R ) ( k I m ) ) ) supp .0. ) C_ { m } )
50 1 4 21 13 18 36 49 gsumpt 
 |-  ( ( ph /\ ( l e. N /\ m e. M ) ) -> ( R gsum ( k e. M |-> ( ( l X k ) ( .r ` R ) ( k I m ) ) ) ) = ( ( k e. M |-> ( ( l X k ) ( .r ` 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 ` R ) ( k I m ) ) = ( ( l X m ) ( .r ` R ) ( m I m ) ) )
54 eqid 
 |-  ( k e. M |-> ( ( l X k ) ( .r ` R ) ( k I m ) ) ) = ( k e. M |-> ( ( l X k ) ( .r ` R ) ( k I m ) ) )
55 ovex 
 |-  ( ( l X m ) ( .r ` R ) ( m I m ) ) e. _V
56 53 54 55 fvmpt 
 |-  ( m e. M -> ( ( k e. M |-> ( ( l X k ) ( .r ` R ) ( k I m ) ) ) ` m ) = ( ( l X m ) ( .r ` R ) ( m I m ) ) )
57 56 ad2antll 
 |-  ( ( ph /\ ( l e. N /\ m e. M ) ) -> ( ( k e. M |-> ( ( l X k ) ( .r ` R ) ( k I m ) ) ) ` m ) = ( ( l X m ) ( .r ` 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 eqtrdi 
 |-  ( j = m -> if ( m = j , .1. , .0. ) = .1. )
65 3 fvexi 
 |-  .1. e. _V
66 59 64 5 65 ovmpo 
 |-  ( ( m e. M /\ m e. M ) -> ( m I m ) = .1. )
67 66 anidms 
 |-  ( m e. M -> ( m I m ) = .1. )
68 67 oveq2d 
 |-  ( m e. M -> ( ( l X m ) ( .r ` R ) ( m I m ) ) = ( ( l X m ) ( .r ` R ) .1. ) )
69 68 ad2antll 
 |-  ( ( ph /\ ( l e. N /\ m e. M ) ) -> ( ( l X m ) ( .r ` R ) ( m I m ) ) = ( ( l X m ) ( .r ` R ) .1. ) )
70 24 fovcdmda 
 |-  ( ( ph /\ ( l e. N /\ m e. M ) ) -> ( l X m ) e. B )
71 1 10 3 ringridm 
 |-  ( ( R e. Ring /\ ( l X m ) e. B ) -> ( ( l X m ) ( .r ` R ) .1. ) = ( l X m ) )
72 11 70 71 syl2anc 
 |-  ( ( ph /\ ( l e. N /\ m e. M ) ) -> ( ( l X m ) ( .r ` R ) .1. ) = ( l X m ) )
73 57 69 72 3eqtrd 
 |-  ( ( ph /\ ( l e. N /\ m e. M ) ) -> ( ( k e. M |-> ( ( l X k ) ( .r ` R ) ( k I m ) ) ) ` m ) = ( l X m ) )
74 19 50 73 3eqtrd 
 |-  ( ( ph /\ ( l e. N /\ m e. M ) ) -> ( l ( X F I ) m ) = ( l X m ) )
75 74 ralrimivva 
 |-  ( ph -> A. l e. N A. m e. M ( l ( X F I ) m ) = ( l X m ) )
76 1 2 8 7 6 6 9 15 mamucl 
 |-  ( ph -> ( X F I ) e. ( B ^m ( N X. M ) ) )
77 elmapi 
 |-  ( ( X F I ) e. ( B ^m ( N X. M ) ) -> ( X F I ) : ( N X. M ) --> B )
78 76 77 syl 
 |-  ( ph -> ( X F I ) : ( N X. M ) --> B )
79 78 ffnd 
 |-  ( ph -> ( X F I ) Fn ( N X. M ) )
80 24 ffnd 
 |-  ( ph -> X Fn ( N X. M ) )
81 eqfnov2 
 |-  ( ( ( X F I ) Fn ( N X. M ) /\ X Fn ( N X. M ) ) -> ( ( X F I ) = X <-> A. l e. N A. m e. M ( l ( X F I ) m ) = ( l X m ) ) )
82 79 80 81 syl2anc 
 |-  ( ph -> ( ( X F I ) = X <-> A. l e. N A. m e. M ( l ( X F I ) m ) = ( l X m ) ) )
83 75 82 mpbird 
 |-  ( ph -> ( X F I ) = X )