Proof of Theorem nmoleub2lem3
Step | Hyp | Ref
| Expression |
1 | | simprl 794 |
. . . 4
|
2 | | qre 11793 |
. . . . . 6
|
3 | 2 | ad2antlr 763 |
. . . . 5
|
4 | | nmoleub2lem3.1 |
. . . . . . . 8
|
5 | | nmoleub2.r |
. . . . . . . . 9
|
6 | 5 | rpred 11872 |
. . . . . . . 8
|
7 | 4, 6 | remulcld 10070 |
. . . . . . 7
|
8 | | nmoleub2.t |
. . . . . . . . . . 11
NrmMod CMod |
9 | 8 | elin1d 3802 |
. . . . . . . . . 10
NrmMod |
10 | | nlmngp 22481 |
. . . . . . . . . 10
NrmMod NrmGrp |
11 | 9, 10 | syl 17 |
. . . . . . . . 9
NrmGrp |
12 | | nmoleub2.f |
. . . . . . . . . . 11
LMHom |
13 | | nmoleub2.v |
. . . . . . . . . . . 12
|
14 | | eqid 2622 |
. . . . . . . . . . . 12
|
15 | 13, 14 | lmhmf 19034 |
. . . . . . . . . . 11
LMHom
|
16 | 12, 15 | syl 17 |
. . . . . . . . . 10
|
17 | | nmoleub2lem3.3 |
. . . . . . . . . 10
|
18 | 16, 17 | ffvelrnd 6360 |
. . . . . . . . 9
|
19 | | nmoleub2.m |
. . . . . . . . . 10
|
20 | 14, 19 | nmcl 22420 |
. . . . . . . . 9
NrmGrp
|
21 | 11, 18, 20 | syl2anc 693 |
. . . . . . . 8
|
22 | | 0red 10041 |
. . . . . . . . 9
|
23 | | nmoleub2.s |
. . . . . . . . . . . . 13
NrmMod CMod |
24 | 23 | elin1d 3802 |
. . . . . . . . . . . 12
NrmMod |
25 | | nlmngp 22481 |
. . . . . . . . . . . 12
NrmMod NrmGrp |
26 | 24, 25 | syl 17 |
. . . . . . . . . . 11
NrmGrp |
27 | | nmoleub2.l |
. . . . . . . . . . . 12
|
28 | 13, 27 | nmcl 22420 |
. . . . . . . . . . 11
NrmGrp
|
29 | 26, 17, 28 | syl2anc 693 |
. . . . . . . . . 10
|
30 | 4, 29 | remulcld 10070 |
. . . . . . . . 9
|
31 | | nmoleub2lem3.2 |
. . . . . . . . . 10
|
32 | 13, 27 | nmge0 22421 |
. . . . . . . . . . 11
NrmGrp
|
33 | 26, 17, 32 | syl2anc 693 |
. . . . . . . . . 10
|
34 | 4, 29, 31, 33 | mulge0d 10604 |
. . . . . . . . 9
|
35 | | nmoleub2lem3.6 |
. . . . . . . . . 10
|
36 | 30, 21 | ltnled 10184 |
. . . . . . . . . 10
|
37 | 35, 36 | mpbird 247 |
. . . . . . . . 9
|
38 | 22, 30, 21, 34, 37 | lelttrd 10195 |
. . . . . . . 8
|
39 | 21, 38 | elrpd 11869 |
. . . . . . 7
|
40 | 7, 39 | rerpdivcld 11903 |
. . . . . 6
|
41 | 40 | ad2antrr 762 |
. . . . 5
|
42 | 12 | ad2antrr 762 |
. . . . . . . . . . . 12
LMHom |
43 | | nmoleub2a.5 |
. . . . . . . . . . . . . 14
|
44 | 43 | sselda 3603 |
. . . . . . . . . . . . 13
|
45 | 44 | adantr 481 |
. . . . . . . . . . . 12
|
46 | 17 | ad2antrr 762 |
. . . . . . . . . . . 12
|
47 | | nmoleub2.g |
. . . . . . . . . . . . 13
Scalar |
48 | | nmoleub2.w |
. . . . . . . . . . . . 13
|
49 | | nmoleub2lem3.p |
. . . . . . . . . . . . 13
|
50 | | eqid 2622 |
. . . . . . . . . . . . 13
|
51 | 47, 48, 13, 49, 50 | lmhmlin 19035 |
. . . . . . . . . . . 12
LMHom
|
52 | 42, 45, 46, 51 | syl3anc 1326 |
. . . . . . . . . . 11
|
53 | 52 | fveq2d 6195 |
. . . . . . . . . 10
|
54 | 9 | ad2antrr 762 |
. . . . . . . . . . 11
NrmMod |
55 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
Scalar Scalar |
56 | 47, 55 | lmhmsca 19030 |
. . . . . . . . . . . . . . 15
LMHom
Scalar |
57 | 42, 56 | syl 17 |
. . . . . . . . . . . . . 14
Scalar |
58 | 57 | fveq2d 6195 |
. . . . . . . . . . . . 13
Scalar |
59 | 58, 48 | syl6eqr 2674 |
. . . . . . . . . . . 12
Scalar |
60 | 45, 59 | eleqtrrd 2704 |
. . . . . . . . . . 11
Scalar |
61 | 18 | ad2antrr 762 |
. . . . . . . . . . 11
|
62 | | eqid 2622 |
. . . . . . . . . . . 12
Scalar Scalar |
63 | | eqid 2622 |
. . . . . . . . . . . 12
Scalar Scalar |
64 | 14, 19, 50, 55, 62, 63 | nmvs 22480 |
. . . . . . . . . . 11
NrmMod
Scalar Scalar |
65 | 54, 60, 61, 64 | syl3anc 1326 |
. . . . . . . . . 10
Scalar |
66 | 57 | fveq2d 6195 |
. . . . . . . . . . . . 13
Scalar |
67 | 66 | fveq1d 6193 |
. . . . . . . . . . . 12
Scalar |
68 | 23 | elin2d 3803 |
. . . . . . . . . . . . . . 15
CMod |
69 | 68 | ad2antrr 762 |
. . . . . . . . . . . . . 14
CMod |
70 | 47, 48 | clmabs 22883 |
. . . . . . . . . . . . . 14
CMod |
71 | 69, 45, 70 | syl2anc 693 |
. . . . . . . . . . . . 13
|
72 | | 0red 10041 |
. . . . . . . . . . . . . . 15
|
73 | 5 | rpge0d 11876 |
. . . . . . . . . . . . . . . . . . 19
|
74 | 4, 6, 31, 73 | mulge0d 10604 |
. . . . . . . . . . . . . . . . . 18
|
75 | | divge0 10892 |
. . . . . . . . . . . . . . . . . 18
|
76 | 7, 74, 21, 38, 75 | syl22anc 1327 |
. . . . . . . . . . . . . . . . 17
|
77 | 76 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
|
78 | 72, 41, 3, 77, 1 | lelttrd 10195 |
. . . . . . . . . . . . . . 15
|
79 | 72, 3, 78 | ltled 10185 |
. . . . . . . . . . . . . 14
|
80 | 3, 79 | absidd 14161 |
. . . . . . . . . . . . 13
|
81 | 71, 80 | eqtr3d 2658 |
. . . . . . . . . . . 12
|
82 | 67, 81 | eqtrd 2656 |
. . . . . . . . . . 11
Scalar |
83 | 82 | oveq1d 6665 |
. . . . . . . . . 10
Scalar |
84 | 53, 65, 83 | 3eqtrd 2660 |
. . . . . . . . 9
|
85 | 84 | oveq1d 6665 |
. . . . . . . 8
|
86 | 13, 47, 49, 48 | clmvscl 22888 |
. . . . . . . . . 10
CMod
|
87 | 69, 45, 46, 86 | syl3anc 1326 |
. . . . . . . . 9
|
88 | 24 | ad2antrr 762 |
. . . . . . . . . . . 12
NrmMod |
89 | | eqid 2622 |
. . . . . . . . . . . . 13
|
90 | 13, 27, 49, 47, 48, 89 | nmvs 22480 |
. . . . . . . . . . . 12
NrmMod
|
91 | 88, 45, 46, 90 | syl3anc 1326 |
. . . . . . . . . . 11
|
92 | 81 | oveq1d 6665 |
. . . . . . . . . . 11
|
93 | 91, 92 | eqtrd 2656 |
. . . . . . . . . 10
|
94 | | simprr 796 |
. . . . . . . . . . 11
|
95 | 6 | ad2antrr 762 |
. . . . . . . . . . . 12
|
96 | | nmoleub2lem3.4 |
. . . . . . . . . . . . . . 15
|
97 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
|
98 | 13, 27, 97 | nmrpcl 22424 |
. . . . . . . . . . . . . . 15
NrmGrp
|
99 | 26, 17, 96, 98 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
100 | 99 | rpregt0d 11878 |
. . . . . . . . . . . . 13
|
101 | 100 | ad2antrr 762 |
. . . . . . . . . . . 12
|
102 | | ltmuldiv 10896 |
. . . . . . . . . . . 12
|
103 | 3, 95, 101, 102 | syl3anc 1326 |
. . . . . . . . . . 11
|
104 | 94, 103 | mpbird 247 |
. . . . . . . . . 10
|
105 | 93, 104 | eqbrtrd 4675 |
. . . . . . . . 9
|
106 | | nmoleub2lem3.5 |
. . . . . . . . . 10
|
107 | 106 | ad2antrr 762 |
. . . . . . . . 9
|
108 | 87, 105, 107 | mp2d 49 |
. . . . . . . 8
|
109 | 85, 108 | eqbrtrrd 4677 |
. . . . . . 7
|
110 | 21 | ad2antrr 762 |
. . . . . . . . 9
|
111 | 3, 110 | remulcld 10070 |
. . . . . . . 8
|
112 | 4 | ad2antrr 762 |
. . . . . . . 8
|
113 | 5 | ad2antrr 762 |
. . . . . . . 8
|
114 | 111, 112,
113 | ledivmul2d 11926 |
. . . . . . 7
|
115 | 109, 114 | mpbid 222 |
. . . . . 6
|
116 | 112, 95 | remulcld 10070 |
. . . . . . 7
|
117 | 21, 38 | jca 554 |
. . . . . . . 8
|
118 | 117 | ad2antrr 762 |
. . . . . . 7
|
119 | | lemuldiv 10903 |
. . . . . . 7
|
120 | 3, 116, 118, 119 | syl3anc 1326 |
. . . . . 6
|
121 | 115, 120 | mpbid 222 |
. . . . 5
|
122 | 3, 41, 121 | lensymd 10188 |
. . . 4
|
123 | 1, 122 | pm2.21dd 186 |
. . 3
|
124 | 6, 99 | rerpdivcld 11903 |
. . . 4
|
125 | 4 | recnd 10068 |
. . . . . . 7
|
126 | 6 | recnd 10068 |
. . . . . . 7
|
127 | 29 | recnd 10068 |
. . . . . . 7
|
128 | | mulass 10024 |
. . . . . . . 8
|
129 | | mul12 10202 |
. . . . . . . 8
|
130 | 128, 129 | eqtrd 2656 |
. . . . . . 7
|
131 | 125, 126,
127, 130 | syl3anc 1326 |
. . . . . 6
|
132 | 30, 21, 5, 37 | ltmul2dd 11928 |
. . . . . 6
|
133 | 131, 132 | eqbrtrd 4675 |
. . . . 5
|
134 | | lt2mul2div 10901 |
. . . . . 6
|
135 | 7, 100, 6, 117, 134 | syl22anc 1327 |
. . . . 5
|
136 | 133, 135 | mpbid 222 |
. . . 4
|
137 | | qbtwnre 12030 |
. . . 4
|
138 | 40, 124, 136, 137 | syl3anc 1326 |
. . 3
|
139 | 123, 138 | r19.29a 3078 |
. 2
|
140 | 139, 35 | pm2.65i 185 |
1
|