Step | Hyp | Ref
| Expression |
1 | | simpl1 1064 |
. . . . 5
|
2 | | lveclmod 19106 |
. . . . . 6
|
3 | | eqlkr.d |
. . . . . . 7
Scalar |
4 | 3 | lmodring 18871 |
. . . . . 6
|
5 | 2, 4 | syl 17 |
. . . . 5
|
6 | 1, 5 | syl 17 |
. . . 4
|
7 | | eqlkr.k |
. . . . 5
|
8 | | eqid 2622 |
. . . . 5
|
9 | 7, 8 | ringidcl 18568 |
. . . 4
|
10 | 6, 9 | syl 17 |
. . 3
|
11 | | simp11 1091 |
. . . . . . . 8
|
12 | 11, 5 | syl 17 |
. . . . . . 7
|
13 | | simp12l 1174 |
. . . . . . . 8
|
14 | | simp3 1063 |
. . . . . . . 8
|
15 | | eqlkr.v |
. . . . . . . . 9
|
16 | | eqlkr.f |
. . . . . . . . 9
LFnl |
17 | 3, 7, 15, 16 | lflcl 34351 |
. . . . . . . 8
|
18 | 11, 13, 14, 17 | syl3anc 1326 |
. . . . . . 7
|
19 | | eqlkr.t |
. . . . . . . 8
|
20 | 7, 19, 8 | ringridm 18572 |
. . . . . . 7
|
21 | 12, 18, 20 | syl2anc 693 |
. . . . . 6
|
22 | | simp2 1062 |
. . . . . . . 8
|
23 | | simp13 1093 |
. . . . . . . . . 10
|
24 | 11, 2 | syl 17 |
. . . . . . . . . . . 12
|
25 | | eqid 2622 |
. . . . . . . . . . . . 13
|
26 | | eqlkr.l |
. . . . . . . . . . . . 13
LKer |
27 | 3, 25, 15, 16, 26 | lkr0f 34381 |
. . . . . . . . . . . 12
|
28 | 24, 13, 27 | syl2anc 693 |
. . . . . . . . . . 11
|
29 | 22, 28 | mpbird 247 |
. . . . . . . . . 10
|
30 | 23, 29 | eqtr3d 2658 |
. . . . . . . . 9
|
31 | | simp12r 1175 |
. . . . . . . . . 10
|
32 | 3, 25, 15, 16, 26 | lkr0f 34381 |
. . . . . . . . . 10
|
33 | 24, 31, 32 | syl2anc 693 |
. . . . . . . . 9
|
34 | 30, 33 | mpbid 222 |
. . . . . . . 8
|
35 | 22, 34 | eqtr4d 2659 |
. . . . . . 7
|
36 | 35 | fveq1d 6193 |
. . . . . 6
|
37 | 21, 36 | eqtr2d 2657 |
. . . . 5
|
38 | 37 | 3expia 1267 |
. . . 4
|
39 | 38 | ralrimiv 2965 |
. . 3
|
40 | | oveq2 6658 |
. . . . . 6
|
41 | 40 | eqeq2d 2632 |
. . . . 5
|
42 | 41 | ralbidv 2986 |
. . . 4
|
43 | 42 | rspcev 3309 |
. . 3
|
44 | 10, 39, 43 | syl2anc 693 |
. 2
|
45 | | simpl1 1064 |
. . . 4
|
46 | | simpl2l 1114 |
. . . 4
|
47 | | simpr 477 |
. . . 4
|
48 | 3, 25, 8, 15, 16 | lfl1 34357 |
. . . 4
|
49 | 45, 46, 47, 48 | syl3anc 1326 |
. . 3
|
50 | | simpl1 1064 |
. . . . . . . 8
|
51 | | simpl2r 1115 |
. . . . . . . 8
|
52 | | simpr2 1068 |
. . . . . . . 8
|
53 | 3, 7, 15, 16 | lflcl 34351 |
. . . . . . . 8
|
54 | 50, 51, 52, 53 | syl3anc 1326 |
. . . . . . 7
|
55 | | simp11 1091 |
. . . . . . . . . . . . . 14
|
56 | 55, 2 | syl 17 |
. . . . . . . . . . . . 13
|
57 | | simp12r 1175 |
. . . . . . . . . . . . 13
|
58 | | simp12l 1174 |
. . . . . . . . . . . . . 14
|
59 | | simp3 1063 |
. . . . . . . . . . . . . 14
|
60 | 3, 7, 15, 16 | lflcl 34351 |
. . . . . . . . . . . . . 14
|
61 | 56, 58, 59, 60 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
62 | | simp22 1095 |
. . . . . . . . . . . . 13
|
63 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
64 | 3, 7, 19, 15, 63, 16 | lflmul 34355 |
. . . . . . . . . . . . 13
|
65 | 56, 57, 61, 62, 64 | syl112anc 1330 |
. . . . . . . . . . . 12
|
66 | 65 | oveq2d 6666 |
. . . . . . . . . . 11
|
67 | 15, 3, 63, 7 | lmodvscl 18880 |
. . . . . . . . . . . . . 14
|
68 | 56, 61, 62, 67 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
69 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
70 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
71 | 3, 69, 15, 70, 16 | lflsub 34354 |
. . . . . . . . . . . . 13
|
72 | 56, 57, 59, 68, 71 | syl112anc 1330 |
. . . . . . . . . . . 12
|
73 | 15, 70 | lmodvsubcl 18908 |
. . . . . . . . . . . . . . . . 17
|
74 | 56, 59, 68, 73 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
75 | 3, 69, 15, 70, 16 | lflsub 34354 |
. . . . . . . . . . . . . . . . . 18
|
76 | 56, 58, 59, 68, 75 | syl112anc 1330 |
. . . . . . . . . . . . . . . . 17
|
77 | 55, 58, 59, 17 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . 20
|
78 | 3, 7, 19, 15, 63, 16 | lflmul 34355 |
. . . . . . . . . . . . . . . . . . . 20
|
79 | 56, 58, 77, 62, 78 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . . 19
|
80 | | simp23 1096 |
. . . . . . . . . . . . . . . . . . . 20
|
81 | 80 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
|
82 | 55, 5 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
83 | 82, 77, 20 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
|
84 | 79, 81, 83 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . . 18
|
85 | 84 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
|
86 | 3 | lmodfgrp 18872 |
. . . . . . . . . . . . . . . . . . . 20
|
87 | 2, 86 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
88 | 55, 87 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
89 | 7, 25, 69 | grpsubid 17499 |
. . . . . . . . . . . . . . . . . 18
|
90 | 88, 77, 89 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
91 | 76, 85, 90 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . 16
|
92 | 15, 3, 25, 16, 26 | ellkr 34376 |
. . . . . . . . . . . . . . . . 17
|
93 | 55, 58, 92 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
94 | 74, 91, 93 | mpbir2and 957 |
. . . . . . . . . . . . . . 15
|
95 | | simp13 1093 |
. . . . . . . . . . . . . . 15
|
96 | 94, 95 | eleqtrd 2703 |
. . . . . . . . . . . . . 14
|
97 | 15, 3, 25, 16, 26 | ellkr 34376 |
. . . . . . . . . . . . . . 15
|
98 | 55, 57, 97 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
99 | 96, 98 | mpbid 222 |
. . . . . . . . . . . . 13
|
100 | 99 | simprd 479 |
. . . . . . . . . . . 12
|
101 | 72, 100 | eqtr3d 2658 |
. . . . . . . . . . 11
|
102 | 66, 101 | eqtr3d 2658 |
. . . . . . . . . 10
|
103 | 3, 7, 15, 16 | lflcl 34351 |
. . . . . . . . . . . 12
|
104 | 55, 57, 59, 103 | syl3anc 1326 |
. . . . . . . . . . 11
|
105 | 54 | 3adant3 1081 |
. . . . . . . . . . . 12
|
106 | 3, 7, 19 | lmodmcl 18875 |
. . . . . . . . . . . 12
|
107 | 56, 77, 105, 106 | syl3anc 1326 |
. . . . . . . . . . 11
|
108 | 7, 25, 69 | grpsubeq0 17501 |
. . . . . . . . . . 11
|
109 | 88, 104, 107, 108 | syl3anc 1326 |
. . . . . . . . . 10
|
110 | 102, 109 | mpbid 222 |
. . . . . . . . 9
|
111 | 110 | 3expia 1267 |
. . . . . . . 8
|
112 | 111 | ralrimiv 2965 |
. . . . . . 7
|
113 | | oveq2 6658 |
. . . . . . . . . 10
|
114 | 113 | eqeq2d 2632 |
. . . . . . . . 9
|
115 | 114 | ralbidv 2986 |
. . . . . . . 8
|
116 | 115 | rspcev 3309 |
. . . . . . 7
|
117 | 54, 112, 116 | syl2anc 693 |
. . . . . 6
|
118 | 117 | 3exp2 1285 |
. . . . 5
|
119 | 118 | imp 445 |
. . . 4
|
120 | 119 | rexlimdv 3030 |
. . 3
|
121 | 49, 120 | mpd 15 |
. 2
|
122 | 44, 121 | pm2.61dane 2881 |
1
|