Step | Hyp | Ref
| Expression |
1 | | ax-1 6 |
. . 3
finSupp
linC
|
2 | 1 | 2a1d 26 |
. 2
finSupp linC finSupp
linC
|
3 | | elmapi 7879 |
. . . . . . . . . 10
|
4 | | ffvelrn 6357 |
. . . . . . . . . . . . . 14
|
5 | 4 | expcom 451 |
. . . . . . . . . . . . 13
|
6 | 5 | adantl 482 |
. . . . . . . . . . . 12
|
7 | 6 | adantl 482 |
. . . . . . . . . . 11
|
8 | 7 | com12 32 |
. . . . . . . . . 10
|
9 | 3, 8 | syl 17 |
. . . . . . . . 9
|
10 | 9 | adantr 481 |
. . . . . . . 8
finSupp linC
|
11 | 10 | impcom 446 |
. . . . . . 7
finSupp linC
|
12 | 11 | biantrurd 529 |
. . . . . 6
finSupp linC
|
13 | | df-ne 2795 |
. . . . . . 7
|
14 | 13 | bicomi 214 |
. . . . . 6
|
15 | | eldifsn 4317 |
. . . . . 6
|
16 | 12, 14, 15 | 3bitr4g 303 |
. . . . 5
finSupp linC
|
17 | | lindslinind.r |
. . . . . . . . . . 11
Scalar |
18 | 17 | lmodfgrp 18872 |
. . . . . . . . . 10
|
19 | 18 | adantl 482 |
. . . . . . . . 9
|
20 | 19 | adantr 481 |
. . . . . . . 8
|
21 | 20 | adantr 481 |
. . . . . . 7
finSupp linC
|
22 | | lindslinind.b |
. . . . . . . 8
|
23 | | lindslinind.0 |
. . . . . . . 8
|
24 | | eqid 2622 |
. . . . . . . 8
|
25 | 22, 23, 24 | grpinvnzcl 17487 |
. . . . . . 7
|
26 | 21, 25 | sylan 488 |
. . . . . 6
finSupp linC |
27 | 26 | ex 450 |
. . . . 5
finSupp linC
|
28 | 16, 27 | sylbid 230 |
. . . 4
finSupp linC
|
29 | | oveq1 6657 |
. . . . . . . . . . 11
|
30 | 29 | eqeq1d 2624 |
. . . . . . . . . 10
linC linC |
31 | 30 | notbid 308 |
. . . . . . . . 9
linC
linC |
32 | 31 | orbi2d 738 |
. . . . . . . 8
finSupp
linC
finSupp linC |
33 | 32 | ralbidv 2986 |
. . . . . . 7
finSupp
linC finSupp
linC |
34 | 33 | rspcva 3307 |
. . . . . 6
finSupp
linC finSupp
linC |
35 | | simpl 473 |
. . . . . . . . 9
|
36 | 35 | adantr 481 |
. . . . . . . 8
finSupp linC
|
37 | | simplrl 800 |
. . . . . . . 8
finSupp linC
|
38 | | simplrr 801 |
. . . . . . . 8
finSupp linC
|
39 | | simpl 473 |
. . . . . . . . 9
finSupp linC |
40 | 39 | adantl 482 |
. . . . . . . 8
finSupp linC
|
41 | | lindslinind.z |
. . . . . . . . 9
|
42 | | eqid 2622 |
. . . . . . . . 9
|
43 | | eqid 2622 |
. . . . . . . . 9
|
44 | 17, 22, 23, 41, 42, 43 | lindslinindimp2lem2 42248 |
. . . . . . . 8
|
45 | 36, 37, 38, 40, 44 | syl13anc 1328 |
. . . . . . 7
finSupp linC
|
46 | | id 22 |
. . . . . . . . . . . . . 14
|
47 | 23 | a1i 11 |
. . . . . . . . . . . . . 14
|
48 | 46, 47 | breq12d 4666 |
. . . . . . . . . . . . 13
finSupp
finSupp |
49 | 48 | notbid 308 |
. . . . . . . . . . . 12
finSupp finSupp
|
50 | | oveq1 6657 |
. . . . . . . . . . . . . 14
linC linC |
51 | 50 | eqeq2d 2632 |
. . . . . . . . . . . . 13
linC linC |
52 | 51 | notbid 308 |
. . . . . . . . . . . 12
linC
linC |
53 | 49, 52 | orbi12d 746 |
. . . . . . . . . . 11
finSupp
linC
finSupp
linC |
54 | 53 | rspcva 3307 |
. . . . . . . . . 10
finSupp linC finSupp linC |
55 | 23 | breq2i 4661 |
. . . . . . . . . . . . . . . . . 18
finSupp finSupp |
56 | 55 | biimpi 206 |
. . . . . . . . . . . . . . . . 17
finSupp finSupp
|
57 | 56 | adantr 481 |
. . . . . . . . . . . . . . . 16
finSupp
linC finSupp |
58 | 57 | adantl 482 |
. . . . . . . . . . . . . . 15
finSupp linC finSupp |
59 | 58 | adantl 482 |
. . . . . . . . . . . . . 14
finSupp linC
finSupp |
60 | | fvexd 6203 |
. . . . . . . . . . . . . 14
finSupp linC
|
61 | 59, 60 | fsuppres 8300 |
. . . . . . . . . . . . 13
finSupp linC
finSupp |
62 | 61 | pm2.24d 147 |
. . . . . . . . . . . 12
finSupp linC
finSupp
|
63 | 62 | com12 32 |
. . . . . . . . . . 11
finSupp
finSupp linC
|
64 | | simplr 792 |
. . . . . . . . . . . . . . . 16
|
65 | 64 | adantr 481 |
. . . . . . . . . . . . . . 15
finSupp linC
|
66 | 17 | fveq2i 6194 |
. . . . . . . . . . . . . . . . . 18
Scalar |
67 | 22, 66 | eqtr2i 2645 |
. . . . . . . . . . . . . . . . 17
Scalar |
68 | 67 | oveq1i 6660 |
. . . . . . . . . . . . . . . 16
Scalar |
69 | 45, 68 | syl6eleqr 2712 |
. . . . . . . . . . . . . . 15
finSupp linC
Scalar
|
70 | | ssdifss 3741 |
. . . . . . . . . . . . . . . . . . 19
|
71 | 70 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
72 | 71 | adantl 482 |
. . . . . . . . . . . . . . . . 17
|
73 | | difexg 4808 |
. . . . . . . . . . . . . . . . . . . 20
|
74 | 73 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
75 | 74 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
76 | | elpwg 4166 |
. . . . . . . . . . . . . . . . . 18
|
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
78 | 72, 77 | mpbird 247 |
. . . . . . . . . . . . . . . 16
|
79 | 78 | adantr 481 |
. . . . . . . . . . . . . . 15
finSupp linC
|
80 | | lincval 42198 |
. . . . . . . . . . . . . . 15
Scalar linC g |
81 | 65, 69, 79, 80 | syl3anc 1326 |
. . . . . . . . . . . . . 14
finSupp linC
linC g |
82 | | fvres 6207 |
. . . . . . . . . . . . . . . . . 18
|
83 | 82 | adantl 482 |
. . . . . . . . . . . . . . . . 17
finSupp linC |
84 | 83 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
finSupp linC
|
85 | 84 | mpteq2dva 4744 |
. . . . . . . . . . . . . . 15
finSupp linC
|
86 | 85 | oveq2d 6666 |
. . . . . . . . . . . . . 14
finSupp linC
g
g |
87 | | simplr 792 |
. . . . . . . . . . . . . . 15
finSupp linC
|
88 | | 3anass 1042 |
. . . . . . . . . . . . . . . . . 18
finSupp linC
finSupp linC |
89 | 88 | bicomi 214 |
. . . . . . . . . . . . . . . . 17
finSupp linC
finSupp linC |
90 | 89 | biimpi 206 |
. . . . . . . . . . . . . . . 16
finSupp linC finSupp
linC |
91 | 90 | adantl 482 |
. . . . . . . . . . . . . . 15
finSupp linC
finSupp linC |
92 | 17, 22, 23, 41, 42, 43 | lindslinindimp2lem4 42250 |
. . . . . . . . . . . . . . 15
finSupp linC g |
93 | 36, 87, 91, 92 | syl3anc 1326 |
. . . . . . . . . . . . . 14
finSupp linC
g |
94 | 81, 86, 93 | 3eqtrrd 2661 |
. . . . . . . . . . . . 13
finSupp linC
linC |
95 | 94 | pm2.24d 147 |
. . . . . . . . . . . 12
finSupp linC
linC |
96 | 95 | com12 32 |
. . . . . . . . . . 11
linC
finSupp linC
|
97 | 63, 96 | jaoi 394 |
. . . . . . . . . 10
finSupp linC
finSupp linC
|
98 | 54, 97 | syl 17 |
. . . . . . . . 9
finSupp linC
finSupp linC
|
99 | 98 | ex 450 |
. . . . . . . 8
finSupp linC
finSupp linC
|
100 | 99 | com23 86 |
. . . . . . 7
finSupp linC
finSupp linC |
101 | 45, 100 | mpcom 38 |
. . . . . 6
finSupp linC
finSupp linC |
102 | 34, 101 | syl5 34 |
. . . . 5
finSupp linC
finSupp
linC |
103 | 102 | expd 452 |
. . . 4
finSupp linC
finSupp
linC
|
104 | 28, 103 | syldc 48 |
. . 3
finSupp linC
finSupp
linC
|
105 | 104 | expd 452 |
. 2
finSupp linC finSupp
linC
|
106 | 2, 105 | pm2.61i 176 |
1
finSupp linC finSupp
linC
|