Step | Hyp | Ref
| Expression |
1 | | 3simpa 1058 |
. . . . . . 7
|
2 | 1 | ad2antlr 763 |
. . . . . 6
|
3 | | fvex 6201 |
. . . . . . . 8
|
4 | | fvex 6201 |
. . . . . . . 8
|
5 | 3, 4 | pm3.2i 471 |
. . . . . . 7
|
6 | 5 | a1i 11 |
. . . . . 6
|
7 | | simp3 1063 |
. . . . . . 7
|
8 | 7 | ad2antlr 763 |
. . . . . 6
|
9 | | fprg 6422 |
. . . . . 6
|
10 | 2, 6, 8, 9 | syl3anc 1326 |
. . . . 5
|
11 | | prfi 8235 |
. . . . . 6
|
12 | 11 | a1i 11 |
. . . . 5
|
13 | | snlindsntor.0 |
. . . . . . 7
|
14 | | fvex 6201 |
. . . . . . 7
|
15 | 13, 14 | eqeltri 2697 |
. . . . . 6
|
16 | 15 | a1i 11 |
. . . . 5
|
17 | 10, 12, 16 | fdmfifsupp 8285 |
. . . 4
finSupp |
18 | 7 | anim2i 593 |
. . . . . . 7
|
19 | 18 | adantr 481 |
. . . . . 6
|
20 | | snlindsntor.r |
. . . . . . . . 9
Scalar |
21 | | snlindsntor.s |
. . . . . . . . 9
|
22 | | eqid 2622 |
. . . . . . . . 9
|
23 | 20, 21, 22 | lmod1cl 18890 |
. . . . . . . 8
|
24 | | simp1 1061 |
. . . . . . . 8
|
25 | 23, 24 | anim12ci 591 |
. . . . . . 7
|
26 | 25 | adantr 481 |
. . . . . 6
|
27 | | simp2 1062 |
. . . . . . 7
|
28 | 27 | ad2antlr 763 |
. . . . . 6
|
29 | 20 | lmodfgrp 18872 |
. . . . . . . 8
|
30 | 29 | adantr 481 |
. . . . . . 7
|
31 | | simpl 473 |
. . . . . . 7
|
32 | | eqid 2622 |
. . . . . . . 8
|
33 | 21, 32 | grpinvcl 17467 |
. . . . . . 7
|
34 | 30, 31, 33 | syl2an 494 |
. . . . . 6
|
35 | | snlindsntor.b |
. . . . . . 7
|
36 | | snlindsntor.t |
. . . . . . 7
|
37 | | eqid 2622 |
. . . . . . 7
|
38 | | eqid 2622 |
. . . . . . 7
|
39 | 35, 20, 21, 36, 37, 38 | lincvalpr 42207 |
. . . . . 6
linC
|
40 | 19, 26, 28, 34, 39 | syl112anc 1330 |
. . . . 5
linC |
41 | | simpll 790 |
. . . . . . 7
|
42 | 24 | ad2antlr 763 |
. . . . . . . 8
|
43 | 31 | adantl 482 |
. . . . . . . 8
|
44 | 42, 28, 43 | 3jca 1242 |
. . . . . . 7
|
45 | 41, 44 | jca 554 |
. . . . . 6
|
46 | | simprr 796 |
. . . . . 6
|
47 | | snlindsntor.z |
. . . . . . 7
|
48 | 35, 20, 21, 13, 47, 36, 22, 32 | ldepsprlem 42261 |
. . . . . 6
|
49 | 45, 46, 48 | sylc 65 |
. . . . 5
|
50 | 40, 49 | eqtrd 2656 |
. . . 4
linC |
51 | 20 | lmodring 18871 |
. . . . . . . . . 10
|
52 | | eqcom 2629 |
. . . . . . . . . . . 12
|
53 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
54 | 21, 53, 22 | 01eq0ring 19272 |
. . . . . . . . . . . . . 14
|
55 | | sneq 4187 |
. . . . . . . . . . . . . . . . 17
|
56 | 55 | eqeq2d 2632 |
. . . . . . . . . . . . . . . 16
|
57 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . 19
|
58 | | elsni 4194 |
. . . . . . . . . . . . . . . . . . . 20
|
59 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . 22
|
60 | 59 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . 21
|
61 | 27 | anim1i 592 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
62 | 61 | ancomd 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
63 | 35, 20, 36, 22 | lmodvs1 18891 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
65 | 64 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
66 | | eqneqall 2805 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
67 | 66 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
68 | 67 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
69 | 68 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
70 | 65, 69 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
71 | 70 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . 22
|
72 | 71 | com3r 87 |
. . . . . . . . . . . . . . . . . . . . 21
|
73 | 60, 72 | syl6bi 243 |
. . . . . . . . . . . . . . . . . . . 20
|
74 | 58, 73 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
75 | 57, 74 | syl6bi 243 |
. . . . . . . . . . . . . . . . . 18
|
76 | 75 | impd 447 |
. . . . . . . . . . . . . . . . 17
|
77 | 76 | com23 86 |
. . . . . . . . . . . . . . . 16
|
78 | 56, 77 | syl6bi 243 |
. . . . . . . . . . . . . . 15
|
79 | 78 | adantl 482 |
. . . . . . . . . . . . . 14
|
80 | 54, 79 | mpd 15 |
. . . . . . . . . . . . 13
|
81 | 80 | ex 450 |
. . . . . . . . . . . 12
|
82 | 52, 81 | syl5bi 232 |
. . . . . . . . . . 11
|
83 | 82 | com25 99 |
. . . . . . . . . 10
|
84 | 51, 83 | mpcom 38 |
. . . . . . . . 9
|
85 | 84 | imp31 448 |
. . . . . . . 8
|
86 | | orc 400 |
. . . . . . . 8
|
87 | 85, 86 | pm2.61d1 171 |
. . . . . . 7
|
88 | 13 | eqeq2i 2634 |
. . . . . . . . 9
|
89 | 88 | necon3abii 2840 |
. . . . . . . 8
|
90 | 89 | orbi1i 542 |
. . . . . . 7
|
91 | 87, 90 | sylibr 224 |
. . . . . 6
|
92 | | fvexd 6203 |
. . . . . . . . 9
|
93 | | fvpr1g 6458 |
. . . . . . . . 9
|
94 | 42, 92, 8, 93 | syl3anc 1326 |
. . . . . . . 8
|
95 | 94 | neeq1d 2853 |
. . . . . . 7
|
96 | | fvexd 6203 |
. . . . . . . . 9
|
97 | | fvpr2g 6459 |
. . . . . . . . 9
|
98 | 28, 96, 8, 97 | syl3anc 1326 |
. . . . . . . 8
|
99 | 98 | neeq1d 2853 |
. . . . . . 7
|
100 | 95, 99 | orbi12d 746 |
. . . . . 6
|
101 | 91, 100 | mpbird 247 |
. . . . 5
|
102 | | fveq2 6191 |
. . . . . . . 8
|
103 | 102 | neeq1d 2853 |
. . . . . . 7
|
104 | | fveq2 6191 |
. . . . . . . 8
|
105 | 104 | neeq1d 2853 |
. . . . . . 7
|
106 | 103, 105 | rexprg 4235 |
. . . . . 6
|
107 | 2, 106 | syl 17 |
. . . . 5
|
108 | 101, 107 | mpbird 247 |
. . . 4
|
109 | 23 | adantr 481 |
. . . . . . 7
|
110 | 109 | adantr 481 |
. . . . . 6
|
111 | | fvex 6201 |
. . . . . . . 8
|
112 | 21, 111 | eqeltri 2697 |
. . . . . . 7
|
113 | 8, 112 | jctir 561 |
. . . . . 6
|
114 | 38 | mapprop 42124 |
. . . . . 6
|
115 | 42, 110, 28, 34, 113, 114 | syl221anc 1337 |
. . . . 5
|
116 | | breq1 4656 |
. . . . . . 7
finSupp
finSupp |
117 | | oveq1 6657 |
. . . . . . . 8
linC
linC |
118 | 117 | eqeq1d 2624 |
. . . . . . 7
linC
linC |
119 | | fveq1 6190 |
. . . . . . . . 9
|
120 | 119 | neeq1d 2853 |
. . . . . . . 8
|
121 | 120 | rexbidv 3052 |
. . . . . . 7
|
122 | 116, 118,
121 | 3anbi123d 1399 |
. . . . . 6
finSupp
linC
finSupp
linC |
123 | 122 | adantl 482 |
. . . . 5
finSupp linC
finSupp
linC |
124 | 115, 123 | rspcedv 3313 |
. . . 4
finSupp
linC
finSupp linC |
125 | 17, 50, 108, 124 | mp3and 1427 |
. . 3
finSupp
linC |
126 | | prelpwi 4915 |
. . . . . 6
|
127 | 126 | 3adant3 1081 |
. . . . 5
|
128 | 127 | ad2antlr 763 |
. . . 4
|
129 | 35, 47, 20, 21, 13 | islindeps 42242 |
. . . 4
linDepS
finSupp linC |
130 | 41, 128, 129 | syl2anc 693 |
. . 3
linDepS
finSupp linC |
131 | 125, 130 | mpbird 247 |
. 2
linDepS |
132 | 131 | ex 450 |
1
linDepS |