Step | Hyp | Ref
| Expression |
1 | | lspsolv.v |
. . 3
|
2 | | lspsolv.s |
. . 3
|
3 | | lspsolv.n |
. . 3
|
4 | | eqid 2622 |
. . 3
Scalar Scalar |
5 | | eqid 2622 |
. . 3
Scalar Scalar |
6 | | eqid 2622 |
. . 3
|
7 | | eqid 2622 |
. . 3
|
8 | | eqid 2622 |
. . 3
Scalar
Scalar |
9 | | lveclmod 19106 |
. . . 4
|
10 | 9 | adantr 481 |
. . 3
|
11 | | simpr1 1067 |
. . 3
|
12 | | simpr2 1068 |
. . 3
|
13 | | simpr3 1069 |
. . . 4
|
14 | 13 | eldifad 3586 |
. . 3
|
15 | 1, 2, 3, 4, 5, 6, 7, 8, 10, 11, 12, 14 | lspsolvlem 19142 |
. 2
Scalar |
16 | 4 | lvecdrng 19105 |
. . . . . . 7
Scalar |
17 | 16 | ad2antrr 762 |
. . . . . 6
Scalar Scalar |
18 | | simprl 794 |
. . . . . 6
Scalar Scalar |
19 | 10 | adantr 481 |
. . . . . . . . . . . 12
Scalar
|
20 | 12 | adantr 481 |
. . . . . . . . . . . 12
Scalar
|
21 | | eqid 2622 |
. . . . . . . . . . . . 13
Scalar Scalar |
22 | | eqid 2622 |
. . . . . . . . . . . . 13
|
23 | 1, 4, 7, 21, 22 | lmod0vs 18896 |
. . . . . . . . . . . 12
Scalar |
24 | 19, 20, 23 | syl2anc 693 |
. . . . . . . . . . 11
Scalar Scalar |
25 | 24 | oveq2d 6666 |
. . . . . . . . . 10
Scalar Scalar |
26 | 11 | adantr 481 |
. . . . . . . . . . . . . . 15
Scalar |
27 | 20 | snssd 4340 |
. . . . . . . . . . . . . . 15
Scalar |
28 | 26, 27 | unssd 3789 |
. . . . . . . . . . . . . 14
Scalar |
29 | 1, 3 | lspssv 18983 |
. . . . . . . . . . . . . 14
|
30 | 19, 28, 29 | syl2anc 693 |
. . . . . . . . . . . . 13
Scalar
|
31 | 30 | ssdifssd 3748 |
. . . . . . . . . . . 12
Scalar
|
32 | 13 | adantr 481 |
. . . . . . . . . . . 12
Scalar
|
33 | 31, 32 | sseldd 3604 |
. . . . . . . . . . 11
Scalar
|
34 | 1, 6, 22 | lmod0vrid 18894 |
. . . . . . . . . . 11
|
35 | 19, 33, 34 | syl2anc 693 |
. . . . . . . . . 10
Scalar |
36 | 25, 35 | eqtrd 2656 |
. . . . . . . . 9
Scalar Scalar |
37 | 36, 32 | eqeltrd 2701 |
. . . . . . . 8
Scalar Scalar
|
38 | 37 | eldifbd 3587 |
. . . . . . 7
Scalar Scalar |
39 | | simprr 796 |
. . . . . . . . 9
Scalar |
40 | | oveq1 6657 |
. . . . . . . . . . 11
Scalar Scalar |
41 | 40 | oveq2d 6666 |
. . . . . . . . . 10
Scalar Scalar |
42 | 41 | eleq1d 2686 |
. . . . . . . . 9
Scalar Scalar |
43 | 39, 42 | syl5ibcom 235 |
. . . . . . . 8
Scalar Scalar Scalar |
44 | 43 | necon3bd 2808 |
. . . . . . 7
Scalar Scalar Scalar |
45 | 38, 44 | mpd 15 |
. . . . . 6
Scalar Scalar |
46 | | eqid 2622 |
. . . . . . 7
Scalar Scalar |
47 | | eqid 2622 |
. . . . . . 7
Scalar Scalar |
48 | | eqid 2622 |
. . . . . . 7
Scalar Scalar |
49 | 5, 21, 46, 47, 48 | drnginvrl 18766 |
. . . . . 6
Scalar
Scalar Scalar ScalarScalar Scalar |
50 | 17, 18, 45, 49 | syl3anc 1326 |
. . . . 5
Scalar ScalarScalar Scalar |
51 | 50 | oveq1d 6665 |
. . . 4
Scalar ScalarScalar Scalar |
52 | 5, 21, 48 | drnginvrcl 18764 |
. . . . . 6
Scalar
Scalar Scalar Scalar Scalar |
53 | 17, 18, 45, 52 | syl3anc 1326 |
. . . . 5
Scalar Scalar Scalar |
54 | 1, 4, 7, 5, 46 | lmodvsass 18888 |
. . . . 5
Scalar Scalar Scalar
ScalarScalar Scalar |
55 | 19, 53, 18, 20, 54 | syl13anc 1328 |
. . . 4
Scalar ScalarScalar Scalar |
56 | 1, 4, 7, 47 | lmodvs1 18891 |
. . . . 5
Scalar |
57 | 19, 20, 56 | syl2anc 693 |
. . . 4
Scalar Scalar |
58 | 51, 55, 57 | 3eqtr3d 2664 |
. . 3
Scalar Scalar |
59 | 33 | snssd 4340 |
. . . . . 6
Scalar |
60 | 26, 59 | unssd 3789 |
. . . . 5
Scalar |
61 | 1, 2, 3 | lspcl 18976 |
. . . . 5
|
62 | 19, 60, 61 | syl2anc 693 |
. . . 4
Scalar
|
63 | 1, 4, 7, 5 | lmodvscl 18880 |
. . . . . . 7
Scalar
|
64 | 19, 18, 20, 63 | syl3anc 1326 |
. . . . . 6
Scalar |
65 | | eqid 2622 |
. . . . . . 7
|
66 | 1, 6, 65 | lmodvpncan 18916 |
. . . . . 6
|
67 | 19, 64, 33, 66 | syl3anc 1326 |
. . . . 5
Scalar |
68 | 1, 6 | lmodcom 18909 |
. . . . . . . 8
|
69 | 19, 64, 33, 68 | syl3anc 1326 |
. . . . . . 7
Scalar |
70 | | ssun1 3776 |
. . . . . . . . . 10
|
71 | 70 | a1i 11 |
. . . . . . . . 9
Scalar |
72 | 1, 3 | lspss 18984 |
. . . . . . . . 9
|
73 | 19, 60, 71, 72 | syl3anc 1326 |
. . . . . . . 8
Scalar
|
74 | 73, 39 | sseldd 3604 |
. . . . . . 7
Scalar
|
75 | 69, 74 | eqeltrd 2701 |
. . . . . 6
Scalar
|
76 | 1, 3 | lspssid 18985 |
. . . . . . . 8
|
77 | 19, 60, 76 | syl2anc 693 |
. . . . . . 7
Scalar |
78 | | snidg 4206 |
. . . . . . . 8
|
79 | | elun2 3781 |
. . . . . . . 8
|
80 | 33, 78, 79 | 3syl 18 |
. . . . . . 7
Scalar
|
81 | 77, 80 | sseldd 3604 |
. . . . . 6
Scalar
|
82 | 65, 2 | lssvsubcl 18944 |
. . . . . 6
|
83 | 19, 62, 75, 81, 82 | syl22anc 1327 |
. . . . 5
Scalar
|
84 | 67, 83 | eqeltrrd 2702 |
. . . 4
Scalar |
85 | 4, 7, 5, 2 | lssvscl 18955 |
. . . 4
Scalar Scalar
Scalar
|
86 | 19, 62, 53, 84, 85 | syl22anc 1327 |
. . 3
Scalar Scalar
|
87 | 58, 86 | eqeltrrd 2702 |
. 2
Scalar
|
88 | 15, 87 | rexlimddv 3035 |
1
|