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 ffvelrn
 |-  ( ( 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 syl6bi
 |-  ( 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 ffvelrn
 |-  ( ( 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 syl6bi
 |-  ( 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 syl6bi
 |-  ( 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 )