Metamath Proof Explorer

Theorem 1mavmul

Description: Multiplication of the identity NxN matrix with an N-dimensional vector results in the vector itself. (Contributed by AV, 9-Feb-2019) (Revised by AV, 23-Feb-2019)

Ref Expression
Hypotheses 1mavmul.a 
|- A = ( N Mat R )
1mavmul.b 
|- B = ( Base ` R )
1mavmul.t 
|- .x. = ( R maVecMul <. N , N >. )
1mavmul.r 
|- ( ph -> R e. Ring )
1mavmul.n 
|- ( ph -> N e. Fin )
1mavmul.y 
|- ( ph -> Y e. ( B ^m N ) )
Assertion 1mavmul 
|- ( ph -> ( ( 1r ` A ) .x. Y ) = Y )

Proof

Step Hyp Ref Expression
1 1mavmul.a 
 |-  A = ( N Mat R )
2 1mavmul.b 
 |-  B = ( Base ` R )
3 1mavmul.t 
 |-  .x. = ( R maVecMul <. N , N >. )
4 1mavmul.r 
 |-  ( ph -> R e. Ring )
5 1mavmul.n 
 |-  ( ph -> N e. Fin )
6 1mavmul.y 
 |-  ( ph -> Y e. ( B ^m N ) )
7 eqid 
 |-  ( .r ` R ) = ( .r ` R )
8 eqid 
 |-  ( Base ` A ) = ( Base ` A )
9 1 fveq2i 
 |-  ( 1r ` A ) = ( 1r ` ( N Mat R ) )
10 1 8 9 mat1bas 
 |-  ( ( R e. Ring /\ N e. Fin ) -> ( 1r ` A ) e. ( Base ` A ) )
11 4 5 10 syl2anc 
 |-  ( ph -> ( 1r ` A ) e. ( Base ` A ) )
12 1 3 2 7 4 5 11 6 mavmulval 
 |-  ( ph -> ( ( 1r ` A ) .x. Y ) = ( i e. N |-> ( R gsum ( j e. N |-> ( ( i ( 1r ` A ) j ) ( .r ` R ) ( Y ` j ) ) ) ) ) )
13 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
14 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
15 1 13 14 mat1 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) = ( x e. N , y e. N |-> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) ) )
16 5 4 15 syl2anc 
 |-  ( ph -> ( 1r ` A ) = ( x e. N , y e. N |-> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) ) )
17 16 oveqdr 
 |-  ( ( ph /\ i e. N ) -> ( i ( 1r ` A ) j ) = ( i ( x e. N , y e. N |-> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) ) j ) )
18 17 oveq1d 
 |-  ( ( ph /\ i e. N ) -> ( ( i ( 1r ` A ) j ) ( .r ` R ) ( Y ` j ) ) = ( ( i ( x e. N , y e. N |-> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) ) j ) ( .r ` R ) ( Y ` j ) ) )
19 18 mpteq2dv 
 |-  ( ( ph /\ i e. N ) -> ( j e. N |-> ( ( i ( 1r ` A ) j ) ( .r ` R ) ( Y ` j ) ) ) = ( j e. N |-> ( ( i ( x e. N , y e. N |-> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) ) j ) ( .r ` R ) ( Y ` j ) ) ) )
20 19 oveq2d 
 |-  ( ( ph /\ i e. N ) -> ( R gsum ( j e. N |-> ( ( i ( 1r ` A ) j ) ( .r ` R ) ( Y ` j ) ) ) ) = ( R gsum ( j e. N |-> ( ( i ( x e. N , y e. N |-> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) ) j ) ( .r ` R ) ( Y ` j ) ) ) ) )
21 eqidd 
 |-  ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( x e. N , y e. N |-> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) ) = ( x e. N , y e. N |-> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) ) )
22 eqeq12 
 |-  ( ( x = i /\ y = j ) -> ( x = y <-> i = j ) )
23 22 ifbid 
 |-  ( ( x = i /\ y = j ) -> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) = if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) )
24 23 adantl 
 |-  ( ( ( ( ph /\ i e. N ) /\ j e. N ) /\ ( x = i /\ y = j ) ) -> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) = if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) )
25 simpr 
 |-  ( ( ph /\ i e. N ) -> i e. N )
26 25 adantr 
 |-  ( ( ( ph /\ i e. N ) /\ j e. N ) -> i e. N )
27 simpr 
 |-  ( ( ( ph /\ i e. N ) /\ j e. N ) -> j e. N )
28 fvexd 
 |-  ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( 1r ` R ) e. _V )
29 fvexd 
 |-  ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( 0g ` R ) e. _V )
30 28 29 ifcld 
 |-  ( ( ( ph /\ i e. N ) /\ j e. N ) -> if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) e. _V )
31 21 24 26 27 30 ovmpod 
 |-  ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( i ( x e. N , y e. N |-> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) ) j ) = if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) )
32 31 oveq1d 
 |-  ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( ( i ( x e. N , y e. N |-> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) ) j ) ( .r ` R ) ( Y ` j ) ) = ( if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ( .r ` R ) ( Y ` j ) ) )
33 iftrue 
 |-  ( i = j -> if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) = ( 1r ` R ) )
34 33 adantr 
 |-  ( ( i = j /\ ( ( ph /\ i e. N ) /\ j e. N ) ) -> if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) = ( 1r ` R ) )
35 34 oveq1d 
 |-  ( ( i = j /\ ( ( ph /\ i e. N ) /\ j e. N ) ) -> ( if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ( .r ` R ) ( Y ` j ) ) = ( ( 1r ` R ) ( .r ` R ) ( Y ` j ) ) )
36 4 adantr 
 |-  ( ( ph /\ i e. N ) -> R e. Ring )
37 36 adantr 
 |-  ( ( ( ph /\ i e. N ) /\ j e. N ) -> R e. Ring )
38 2 fvexi 
 |-  B e. _V
39 38 a1i 
 |-  ( ph -> B e. _V )
40 39 5 elmapd 
 |-  ( ph -> ( Y e. ( B ^m N ) <-> Y : N --> B ) )
41 ffvelcdm 
 |-  ( ( Y : N --> B /\ j e. N ) -> ( Y ` j ) e. B )
42 41 ex 
 |-  ( Y : N --> B -> ( j e. N -> ( Y ` j ) e. B ) )
43 40 42 biimtrdi 
 |-  ( ph -> ( Y e. ( B ^m N ) -> ( j e. N -> ( Y ` j ) e. B ) ) )
44 6 43 mpd 
 |-  ( ph -> ( j e. N -> ( Y ` j ) e. B ) )
45 44 adantr 
 |-  ( ( ph /\ i e. N ) -> ( j e. N -> ( Y ` j ) e. B ) )
46 45 imp 
 |-  ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( Y ` j ) e. B )
47 2 7 13 ringlidm 
 |-  ( ( R e. Ring /\ ( Y ` j ) e. B ) -> ( ( 1r ` R ) ( .r ` R ) ( Y ` j ) ) = ( Y ` j ) )
48 37 46 47 syl2anc 
 |-  ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( ( 1r ` R ) ( .r ` R ) ( Y ` j ) ) = ( Y ` j ) )
49 48 adantl 
 |-  ( ( i = j /\ ( ( ph /\ i e. N ) /\ j e. N ) ) -> ( ( 1r ` R ) ( .r ` R ) ( Y ` j ) ) = ( Y ` j ) )
50 fveq2 
 |-  ( j = i -> ( Y ` j ) = ( Y ` i ) )
51 50 equcoms 
 |-  ( i = j -> ( Y ` j ) = ( Y ` i ) )
52 51 adantr 
 |-  ( ( i = j /\ ( ( ph /\ i e. N ) /\ j e. N ) ) -> ( Y ` j ) = ( Y ` i ) )
53 35 49 52 3eqtrd 
 |-  ( ( i = j /\ ( ( ph /\ i e. N ) /\ j e. N ) ) -> ( if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ( .r ` R ) ( Y ` j ) ) = ( Y ` i ) )
54 iftrue 
 |-  ( j = i -> if ( j = i , ( Y ` i ) , ( 0g ` R ) ) = ( Y ` i ) )
55 54 equcoms 
 |-  ( i = j -> if ( j = i , ( Y ` i ) , ( 0g ` R ) ) = ( Y ` i ) )
56 55 adantr 
 |-  ( ( i = j /\ ( ( ph /\ i e. N ) /\ j e. N ) ) -> if ( j = i , ( Y ` i ) , ( 0g ` R ) ) = ( Y ` i ) )
57 53 56 eqtr4d 
 |-  ( ( i = j /\ ( ( ph /\ i e. N ) /\ j e. N ) ) -> ( if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ( .r ` R ) ( Y ` j ) ) = if ( j = i , ( Y ` i ) , ( 0g ` R ) ) )
58 iffalse 
 |-  ( -. i = j -> if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) = ( 0g ` R ) )
59 58 oveq1d 
 |-  ( -. i = j -> ( if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ( .r ` R ) ( Y ` j ) ) = ( ( 0g ` R ) ( .r ` R ) ( Y ` j ) ) )
60 59 adantr 
 |-  ( ( -. i = j /\ ( ( ph /\ i e. N ) /\ j e. N ) ) -> ( if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ( .r ` R ) ( Y ` j ) ) = ( ( 0g ` R ) ( .r ` R ) ( Y ` j ) ) )
61 2 7 14 ringlz 
 |-  ( ( R e. Ring /\ ( Y ` j ) e. B ) -> ( ( 0g ` R ) ( .r ` R ) ( Y ` j ) ) = ( 0g ` R ) )
62 37 46 61 syl2anc 
 |-  ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( ( 0g ` R ) ( .r ` R ) ( Y ` j ) ) = ( 0g ` R ) )
63 62 adantl 
 |-  ( ( -. i = j /\ ( ( ph /\ i e. N ) /\ j e. N ) ) -> ( ( 0g ` R ) ( .r ` R ) ( Y ` j ) ) = ( 0g ` R ) )
64 eqcom 
 |-  ( i = j <-> j = i )
65 iffalse 
 |-  ( -. j = i -> if ( j = i , ( Y ` i ) , ( 0g ` R ) ) = ( 0g ` R ) )
66 64 65 sylnbi 
 |-  ( -. i = j -> if ( j = i , ( Y ` i ) , ( 0g ` R ) ) = ( 0g ` R ) )
67 66 eqcomd 
 |-  ( -. i = j -> ( 0g ` R ) = if ( j = i , ( Y ` i ) , ( 0g ` R ) ) )
68 67 adantr 
 |-  ( ( -. i = j /\ ( ( ph /\ i e. N ) /\ j e. N ) ) -> ( 0g ` R ) = if ( j = i , ( Y ` i ) , ( 0g ` R ) ) )
69 60 63 68 3eqtrd 
 |-  ( ( -. i = j /\ ( ( ph /\ i e. N ) /\ j e. N ) ) -> ( if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ( .r ` R ) ( Y ` j ) ) = if ( j = i , ( Y ` i ) , ( 0g ` R ) ) )
70 57 69 pm2.61ian 
 |-  ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ( .r ` R ) ( Y ` j ) ) = if ( j = i , ( Y ` i ) , ( 0g ` R ) ) )
71 32 70 eqtrd 
 |-  ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( ( i ( x e. N , y e. N |-> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) ) j ) ( .r ` R ) ( Y ` j ) ) = if ( j = i , ( Y ` i ) , ( 0g ` R ) ) )
72 71 mpteq2dva 
 |-  ( ( ph /\ i e. N ) -> ( j e. N |-> ( ( i ( x e. N , y e. N |-> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) ) j ) ( .r ` R ) ( Y ` j ) ) ) = ( j e. N |-> if ( j = i , ( Y ` i ) , ( 0g ` R ) ) ) )
73 72 oveq2d 
 |-  ( ( ph /\ i e. N ) -> ( R gsum ( j e. N |-> ( ( i ( x e. N , y e. N |-> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) ) j ) ( .r ` R ) ( Y ` j ) ) ) ) = ( R gsum ( j e. N |-> if ( j = i , ( Y ` i ) , ( 0g ` R ) ) ) ) )
74 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
75 4 74 syl 
 |-  ( ph -> R e. Mnd )
76 75 adantr 
 |-  ( ( ph /\ i e. N ) -> R e. Mnd )
77 5 adantr 
 |-  ( ( ph /\ i e. N ) -> N e. Fin )
78 eqid 
 |-  ( j e. N |-> if ( j = i , ( Y ` i ) , ( 0g ` R ) ) ) = ( j e. N |-> if ( j = i , ( Y ` i ) , ( 0g ` R ) ) )
79 ffvelcdm 
 |-  ( ( Y : N --> B /\ i e. N ) -> ( Y ` i ) e. B )
80 79 2 eleqtrdi 
 |-  ( ( Y : N --> B /\ i e. N ) -> ( Y ` i ) e. ( Base ` R ) )
81 80 ex 
 |-  ( Y : N --> B -> ( i e. N -> ( Y ` i ) e. ( Base ` R ) ) )
82 40 81 biimtrdi 
 |-  ( ph -> ( Y e. ( B ^m N ) -> ( i e. N -> ( Y ` i ) e. ( Base ` R ) ) ) )
83 6 82 mpd 
 |-  ( ph -> ( i e. N -> ( Y ` i ) e. ( Base ` R ) ) )
84 83 imp 
 |-  ( ( ph /\ i e. N ) -> ( Y ` i ) e. ( Base ` R ) )
85 14 76 77 25 78 84 gsummptif1n0 
 |-  ( ( ph /\ i e. N ) -> ( R gsum ( j e. N |-> if ( j = i , ( Y ` i ) , ( 0g ` R ) ) ) ) = ( Y ` i ) )
86 20 73 85 3eqtrd 
 |-  ( ( ph /\ i e. N ) -> ( R gsum ( j e. N |-> ( ( i ( 1r ` A ) j ) ( .r ` R ) ( Y ` j ) ) ) ) = ( Y ` i ) )
87 86 mpteq2dva 
 |-  ( ph -> ( i e. N |-> ( R gsum ( j e. N |-> ( ( i ( 1r ` A ) j ) ( .r ` R ) ( Y ` j ) ) ) ) ) = ( i e. N |-> ( Y ` i ) ) )
88 ffn 
 |-  ( Y : N --> B -> Y Fn N )
89 40 88 biimtrdi 
 |-  ( ph -> ( Y e. ( B ^m N ) -> Y Fn N ) )
90 6 89 mpd 
 |-  ( ph -> Y Fn N )
91 eqcom 
 |-  ( ( i e. N |-> ( Y ` i ) ) = Y <-> Y = ( i e. N |-> ( Y ` i ) ) )
92 dffn5 
 |-  ( Y Fn N <-> Y = ( i e. N |-> ( Y ` i ) ) )
93 91 92 bitr4i 
 |-  ( ( i e. N |-> ( Y ` i ) ) = Y <-> Y Fn N )
94 90 93 sylibr 
 |-  ( ph -> ( i e. N |-> ( Y ` i ) ) = Y )
95 12 87 94 3eqtrd 
 |-  ( ph -> ( ( 1r ` A ) .x. Y ) = Y )