Step | Hyp | Ref
| Expression |
1 | | elpwi 4168 |
. . . 4
|
2 | 1 | ad2antrl 764 |
. . 3
finSupp linC
|
3 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
4 | 3 | anim2i 593 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
5 | 4 | ancomd 467 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
6 | 5 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
finSupp linC
|
7 | | eldifi 3732 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
8 | 7 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
9 | 8 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
10 | 9 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
finSupp linC
|
11 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
12 | 11 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
finSupp linC
|
13 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . . . 23
finSupp linC
|
14 | 10, 12, 13 | 3jca 1242 |
. . . . . . . . . . . . . . . . . . . . . 22
finSupp linC
|
15 | | simprrl 804 |
. . . . . . . . . . . . . . . . . . . . . 22
finSupp linC
finSupp |
16 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
17 | | lindslinind.r |
. . . . . . . . . . . . . . . . . . . . . . 23
Scalar |
18 | | lindslinind.b |
. . . . . . . . . . . . . . . . . . . . . . 23
|
19 | | lindslinind.0 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
20 | | lindslinind.z |
. . . . . . . . . . . . . . . . . . . . . . 23
|
21 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
22 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
23 | 16, 17, 18, 19, 20, 21, 22 | lincext2 42244 |
. . . . . . . . . . . . . . . . . . . . . 22
finSupp finSupp |
24 | 6, 14, 15, 23 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . 21
finSupp linC
finSupp
|
25 | 4 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
26 | 25 | ancomd 467 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
27 | 26 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
finSupp linC
|
28 | 16, 17, 18, 19, 20, 21, 22 | lincext1 42243 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
29 | 27, 14, 28 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
finSupp linC
|
30 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
finSupp finSupp |
31 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
linC linC |
32 | 31 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
linC linC |
33 | 30, 32 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
finSupp linC finSupp
linC |
34 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
35 | 34 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
36 | 35 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
37 | 33, 36 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . . . . . 24
finSupp
linC
finSupp linC
|
38 | 37 | rspcv 3305 |
. . . . . . . . . . . . . . . . . . . . . . 23
finSupp
linC
finSupp linC
|
39 | 29, 38 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
finSupp linC
finSupp
linC
finSupp linC
|
40 | 39 | exp4a 633 |
. . . . . . . . . . . . . . . . . . . . 21
finSupp linC
finSupp
linC
finSupp linC
|
41 | 24, 40 | mpid 44 |
. . . . . . . . . . . . . . . . . . . 20
finSupp linC
finSupp
linC
linC |
42 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . . 22
finSupp linC
finSupp linC |
43 | 16, 17, 18, 19, 20, 21, 22 | lincext3 42245 |
. . . . . . . . . . . . . . . . . . . . . 22
finSupp linC linC |
44 | 6, 14, 42, 43 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . 21
finSupp linC
linC |
45 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
46 | 45 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
47 | 46 | rspcv 3305 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
48 | 12, 47 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
finSupp linC
|
49 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
50 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
51 | 50 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
52 | | fvexd 6203 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
53 | 49, 51, 11, 52 | fvmptd 6288 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
54 | 53 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
finSupp linC
|
55 | 54 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . . . 23
finSupp linC
|
56 | 17 | lmodfgrp 18872 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
57 | 18, 19, 21 | grpinvnzcl 17487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
58 | | eldif 3584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
59 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
60 | 59 | elsn 4192 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
61 | | pm2.21 120 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
linC |
62 | 61 | com25 99 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
linC |
63 | 60, 62 | sylnbi 320 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
linC |
64 | 63 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
linC |
65 | 58, 64 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
linC |
66 | 57, 65 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
linC |
67 | 66 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
linC |
68 | 56, 67 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
linC |
69 | 68 | com24 95 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
linC |
70 | 69 | impcom 446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
linC |
71 | 70 | impcom 446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
linC |
72 | 71 | com13 88 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
linC |
73 | 72 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
linC |
74 | 73 | impcom 446 |
. . . . . . . . . . . . . . . . . . . . . . . 24
linC |
75 | 74 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
finSupp linC
linC |
76 | 55, 75 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . . . 22
finSupp linC
linC |
77 | 48, 76 | syld 47 |
. . . . . . . . . . . . . . . . . . . . 21
finSupp linC
linC |
78 | 44, 77 | embantd 59 |
. . . . . . . . . . . . . . . . . . . 20
finSupp linC
linC
linC |
79 | 41, 78 | syldc 48 |
. . . . . . . . . . . . . . . . . . 19
finSupp
linC
finSupp linC
linC |
80 | 79 | expd 452 |
. . . . . . . . . . . . . . . . . 18
finSupp
linC
finSupp linC
linC |
81 | 80 | exp4c 636 |
. . . . . . . . . . . . . . . . 17
finSupp
linC
finSupp linC
linC |
82 | 81 | impcom 446 |
. . . . . . . . . . . . . . . 16
finSupp linC
finSupp linC
linC |
83 | 82 | impcom 446 |
. . . . . . . . . . . . . . 15
finSupp linC
finSupp linC
linC |
84 | 83 | imp 445 |
. . . . . . . . . . . . . 14
finSupp linC
finSupp linC
linC |
85 | 84 | expdimp 453 |
. . . . . . . . . . . . 13
finSupp linC
finSupp linC
linC |
86 | 85 | expd 452 |
. . . . . . . . . . . 12
finSupp linC
finSupp
linC
linC |
87 | 86 | impcom 446 |
. . . . . . . . . . 11
finSupp
finSupp linC
linC linC |
88 | 87 | pm2.01d 181 |
. . . . . . . . . 10
finSupp
finSupp linC
linC |
89 | 88 | olcd 408 |
. . . . . . . . 9
finSupp
finSupp linC
finSupp
linC |
90 | | simpl 473 |
. . . . . . . . . 10
finSupp
finSupp linC
finSupp |
91 | 90 | orcd 407 |
. . . . . . . . 9
finSupp
finSupp linC
finSupp
linC |
92 | 89, 91 | pm2.61ian 831 |
. . . . . . . 8
finSupp linC
finSupp linC |
93 | 92 | ralrimiva 2966 |
. . . . . . 7
finSupp linC
finSupp
linC |
94 | | ralnex 2992 |
. . . . . . . 8
finSupp linC
finSupp linC |
95 | | ianor 509 |
. . . . . . . . 9
finSupp linC finSupp
linC |
96 | 95 | ralbii 2980 |
. . . . . . . 8
finSupp linC finSupp
linC |
97 | 94, 96 | bitr3i 266 |
. . . . . . 7
finSupp linC
finSupp
linC |
98 | 93, 97 | sylibr 224 |
. . . . . 6
finSupp linC
finSupp linC |
99 | 98 | intnand 962 |
. . . . 5
finSupp linC
finSupp linC |
100 | 3 | ad2antrr 762 |
. . . . . . 7
finSupp linC
|
101 | 1 | ssdifssd 3748 |
. . . . . . . . . 10
|
102 | 101 | ad2antrl 764 |
. . . . . . . . 9
finSupp linC
|
103 | | difexg 4808 |
. . . . . . . . . . 11
|
104 | 103 | ad2antrr 762 |
. . . . . . . . . 10
finSupp linC
|
105 | | elpwg 4166 |
. . . . . . . . . 10
|
106 | 104, 105 | syl 17 |
. . . . . . . . 9
finSupp linC
|
107 | 102, 106 | mpbird 247 |
. . . . . . . 8
finSupp linC
|
108 | 107 | adantr 481 |
. . . . . . 7
finSupp linC
|
109 | 16 | lspeqlco 42228 |
. . . . . . . . 9
LinCo |
110 | 109 | eleq2d 2687 |
. . . . . . . 8
LinCo
|
111 | 110 | bicomd 213 |
. . . . . . 7
LinCo |
112 | 100, 108,
111 | syl2anc 693 |
. . . . . 6
finSupp linC
LinCo |
113 | 3 | adantr 481 |
. . . . . . . . 9
finSupp linC
|
114 | | difexg 4808 |
. . . . . . . . . . . 12
|
115 | 114, 105 | syl 17 |
. . . . . . . . . . 11
|
116 | 101, 115 | mpbird 247 |
. . . . . . . . . 10
|
117 | 116 | ad2antrl 764 |
. . . . . . . . 9
finSupp linC
|
118 | 113, 117 | jca 554 |
. . . . . . . 8
finSupp linC
|
119 | 118 | adantr 481 |
. . . . . . 7
finSupp linC
|
120 | 16, 17, 18 | lcoval 42201 |
. . . . . . . 8
LinCo
finSupp
linC |
121 | 19 | eqcomi 2631 |
. . . . . . . . . . . 12
|
122 | 121 | breq2i 4661 |
. . . . . . . . . . 11
finSupp
finSupp |
123 | 122 | anbi1i 731 |
. . . . . . . . . 10
finSupp linC
finSupp linC |
124 | 123 | rexbii 3041 |
. . . . . . . . 9
finSupp linC finSupp linC |
125 | 124 | anbi2i 730 |
. . . . . . . 8
finSupp linC
finSupp linC |
126 | 120, 125 | syl6bb 276 |
. . . . . . 7
LinCo
finSupp linC |
127 | 119, 126 | syl 17 |
. . . . . 6
finSupp linC
LinCo finSupp linC |
128 | 112, 127 | bitrd 268 |
. . . . 5
finSupp linC
finSupp linC |
129 | 99, 128 | mtbird 315 |
. . . 4
finSupp linC
|
130 | 129 | ralrimivva 2971 |
. . 3
finSupp linC
|
131 | 2, 130 | jca 554 |
. 2
finSupp linC
|
132 | 131 | ex 450 |
1
finSupp linC
|