Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ttgcontlem1 Structured version   Unicode version

Theorem ttgcontlem1 24020
 Description: Lemma for % ttgcont (Contributed by Thierry Arnoux, 24-May-2019.)
Hypotheses
Ref Expression
ttgval.n toTG
ttgitvval.i Itv
ttgitvval.b
ttgitvval.m
ttgitvval.s
ttgelitv.x
ttgelitv.y
ttgbtwnid.r Scalar
ttgbtwnid.2
ttgitvval.p
ttgcontlem1.h CVec
ttgcontlem1.a
ttgcontlem1.n
ttgcontlem1.o
ttgcontlem1.p
ttgcontlem1.q
ttgcontlem1.r
ttgcontlem1.s
ttgcontlem1.l
ttgcontlem1.k
ttgcontlem1.m
ttgcontlem1.y
ttgcontlem1.x
ttgcontlem1.b
Assertion
Ref Expression
ttgcontlem1

Proof of Theorem ttgcontlem1
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 unitssre 11679 . . . . . . . 8
2 ttgcontlem1.l . . . . . . . 8
31, 2sseldi 3507 . . . . . . 7
4 ttgcontlem1.k . . . . . . . 8
51, 4sseldi 3507 . . . . . . 7
63, 5remulcld 9636 . . . . . 6
7 0re 9608 . . . . . . . . 9
8 iccssre 11618 . . . . . . . . 9
97, 3, 8sylancr 663 . . . . . . . 8
10 ttgcontlem1.m . . . . . . . 8
119, 10sseldd 3510 . . . . . . 7
1211, 5remulcld 9636 . . . . . 6
136, 12resubcld 9999 . . . . 5
14 1red 9623 . . . . . . 7
1511, 14remulcld 9636 . . . . . 6
1615, 12resubcld 9999 . . . . 5
1711recnd 9634 . . . . . . 7
18 1cnd 9624 . . . . . . 7
195recnd 9634 . . . . . . 7
2017, 18, 19subdid 10024 . . . . . 6
2118, 19subcld 9942 . . . . . . 7
22 ttgcontlem1.o . . . . . . 7
23 ttgcontlem1.q . . . . . . . . 9
2423necomd 2738 . . . . . . . 8
2518, 19, 24subne0d 9951 . . . . . . 7
2617, 21, 22, 25mulne0d 10213 . . . . . 6
2720, 26eqnetrrd 2761 . . . . 5
2813, 16, 27redivcld 10384 . . . 4
29 0xr 9652 . . . . . . . . . . 11
3029a1i 11 . . . . . . . . . 10
313rexrd 9655 . . . . . . . . . 10
32 iccgelb 11593 . . . . . . . . . 10
3330, 31, 10, 32syl3anc 1228 . . . . . . . . 9
3411, 33, 22ne0gt0d 9733 . . . . . . . 8
3511, 34elrpd 11266 . . . . . . 7
3614rexrd 9655 . . . . . . . . . 10
37 iccleub 11592 . . . . . . . . . 10
3830, 36, 4, 37syl3anc 1228 . . . . . . . . 9
395, 14ltlend 9741 . . . . . . . . 9
4038, 24, 39mpbir2and 920 . . . . . . . 8
41 difrp 11265 . . . . . . . . 9
425, 14, 41syl2anc 661 . . . . . . . 8
4340, 42mpbid 210 . . . . . . 7
4435, 43rpmulcld 11284 . . . . . 6
4520, 44eqeltrrd 2556 . . . . 5
463, 11resubcld 9999 . . . . . . 7
47 iccleub 11592 . . . . . . . . 9
4830, 31, 10, 47syl3anc 1228 . . . . . . . 8
493, 11subge0d 10154 . . . . . . . 8
5048, 49mpbird 232 . . . . . . 7
51 iccgelb 11593 . . . . . . . 8
5230, 36, 4, 51syl3anc 1228 . . . . . . 7
5346, 5, 50, 52mulge0d 10141 . . . . . 6
543recnd 9634 . . . . . . 7
5554, 17, 19subdird 10025 . . . . . 6
5653, 55breqtrd 4477 . . . . 5
5713, 45, 56divge0d 11304 . . . 4
58 ttgcontlem1.s . . . . . . . . 9
59 ttgcontlem1.p . . . . . . . . . . . 12
605, 52, 59ne0gt0d 9733 . . . . . . . . . . 11
615, 60elrpd 11266 . . . . . . . . . 10
623, 11, 61lemuldivd 11313 . . . . . . . . 9
6358, 62mpbird 232 . . . . . . . 8
6417mulid1d 9625 . . . . . . . 8
6563, 64breqtrrd 4479 . . . . . . 7
666, 15, 12, 65lesub1dd 10180 . . . . . 6
6717, 18mulcld 9628 . . . . . . . 8
6817, 19mulcld 9628 . . . . . . . 8
6967, 68subcld 9942 . . . . . . 7
7069mulid1d 9625 . . . . . 6
7166, 70breqtrrd 4479 . . . . 5
7213, 14, 45ledivmuld 11317 . . . . 5
7371, 72mpbird 232 . . . 4
74 1re 9607 . . . . 5
757, 74elicc2i 11602 . . . 4
7628, 57, 73, 75syl3anbrc 1180 . . 3
77 ttgcontlem1.h . . . . . 6 CVec
7877cvsclm 21473 . . . . 5 CMod
79 ttgbtwnid.2 . . . . . . . 8
8079, 2sseldd 3510 . . . . . . 7
81 0elunit 11650 . . . . . . . . . 10
82 iccss2 11607 . . . . . . . . . 10
8381, 2, 82sylancr 663 . . . . . . . . 9
8483, 79sstrd 3519 . . . . . . . 8
8584, 10sseldd 3510 . . . . . . 7
86 eqid 2467 . . . . . . . 8 Scalar Scalar
87 ttgbtwnid.r . . . . . . . 8 Scalar
8886, 87clmsubcl 21451 . . . . . . 7 CMod
8978, 80, 85, 88syl3anc 1228 . . . . . 6
9086, 87cvsdivcl 21476 . . . . . 6 CVec
9177, 89, 85, 22, 90syl13anc 1230 . . . . 5
9279, 4sseldd 3510 . . . . . 6
93 1elunit 11651 . . . . . . . . 9
9493a1i 11 . . . . . . . 8
9579, 94sseldd 3510 . . . . . . 7
9686, 87clmsubcl 21451 . . . . . . 7 CMod
9778, 95, 92, 96syl3anc 1228 . . . . . 6
9886, 87cvsdivcl 21476 . . . . . 6 CVec
9977, 92, 97, 25, 98syl13anc 1230 . . . . 5
100 clmgrp 21434 . . . . . . 7 CMod
10178, 100syl 16 . . . . . 6
102 ttgelitv.y . . . . . 6
103 ttgelitv.x . . . . . 6
104 ttgitvval.b . . . . . . 7
105 ttgitvval.m . . . . . . 7
106104, 105grpsubcl 15989 . . . . . 6
107101, 102, 103, 106syl3anc 1228 . . . . 5
108 ttgitvval.s . . . . . 6
109104, 86, 108, 87clmvsass 21453 . . . . 5 CMod
11078, 91, 99, 107, 109syl13anc 1230 . . . 4
11146recnd 9634 . . . . . . 7
112111, 17, 19, 21, 22, 25divmuldivd 10373 . . . . . 6
11355, 20oveq12d 6313 . . . . . 6
114112, 113eqtrd 2508 . . . . 5
115114oveq1d 6310 . . . 4
116 ttgcontlem1.a . . . . . . . 8
117104, 105grpsubcl 15989 . . . . . . . 8
118101, 103, 116, 117syl3anc 1228 . . . . . . 7
119 ttgcontlem1.y . . . . . . . . . 10
120119oveq2d 6311 . . . . . . . . 9
12119, 21mulcomd 9629 . . . . . . . . . . 11
122121oveq1d 6310 . . . . . . . . . 10
123104, 105grpsubcl 15989 . . . . . . . . . . . 12
124101, 102, 116, 123syl3anc 1228 . . . . . . . . . . 11
125104, 86, 108, 87clmvsass 21453 . . . . . . . . . . 11 CMod
12678, 92, 97, 124, 125syl13anc 1230 . . . . . . . . . 10
127104, 86, 108, 87clmvsass 21453 . . . . . . . . . . 11 CMod
12878, 97, 92, 124, 127syl13anc 1230 . . . . . . . . . 10
129122, 126, 1283eqtr3d 2516 . . . . . . . . 9
130 eqid 2467 . . . . . . . . . . . . 13 Scalar Scalar
131 clmlmod 21433 . . . . . . . . . . . . . 14 CMod
13278, 131syl 16 . . . . . . . . . . . . 13
133104, 108, 86, 87, 105, 130, 132, 95, 92, 124lmodsubdir 17437 . . . . . . . . . . . 12 Scalar
13486, 87clmsub 21446 . . . . . . . . . . . . . 14 CMod Scalar
13578, 95, 92, 134syl3anc 1228 . . . . . . . . . . . . 13 Scalar
136135oveq1d 6310 . . . . . . . . . . . 12 Scalar
137104, 108clmvs1 21455 . . . . . . . . . . . . . . 15 CMod
13878, 124, 137syl2anc 661 . . . . . . . . . . . . . 14
139138eqcomd 2475 . . . . . . . . . . . . 13
140139, 119oveq12d 6313 . . . . . . . . . . . 12
141133, 136, 1403eqtr4d 2518 . . . . . . . . . . 11
142104, 105grpnnncan2 16006 . . . . . . . . . . . 12
143101, 102, 103, 116, 142syl13anc 1230 . . . . . . . . . . 11
144141, 143eqtrd 2508 . . . . . . . . . 10
145144oveq2d 6311 . . . . . . . . 9
146120, 129, 1453eqtr2rd 2515 . . . . . . . 8
147104, 108, 86, 87, 77, 92, 97, 107, 118, 59, 146cvsmuleqdivd 21477 . . . . . . 7
148104, 108, 86, 87, 77, 97, 92, 107, 118, 25, 59, 147cvsdiveqd 21478 . . . . . 6
149148, 118eqeltrd 2555 . . . . 5
150 ttgcontlem1.b . . . . . . 7
151 ttgcontlem1.n . . . . . . . . . 10
152104, 105grpsubcl 15989 . . . . . . . . . 10
153101, 151, 116, 152syl3anc 1228 . . . . . . . . 9
154104, 86, 108, 87lmodvscl 17398 . . . . . . . . 9
155132, 80, 153, 154syl3anc 1228 . . . . . . . 8
156 ttgitvval.p . . . . . . . . 9
157104, 156grpcl 15934 . . . . . . . 8
158101, 116, 155, 157syl3anc 1228 . . . . . . 7
159150, 158eqeltrd 2555 . . . . . 6
160104, 105grpsubcl 15989 . . . . . 6
161101, 159, 103, 160syl3anc 1228 . . . . 5
162 ttgcontlem1.r . . . . . 6
16354, 17, 162subne0d 9951 . . . . 5
164 ttgcontlem1.x . . . . . . . . . 10
165164oveq2d 6311 . . . . . . . . 9
16617, 111mulcomd 9629 . . . . . . . . . . 11
167166oveq1d 6310 . . . . . . . . . 10
168104, 86, 108, 87clmvsass 21453 . . . . . . . . . . 11 CMod
16978, 85, 89, 153, 168syl13anc 1230 . . . . . . . . . 10
170104, 86, 108, 87clmvsass 21453 . . . . . . . . . . 11 CMod
17178, 89, 85, 153, 170syl13anc 1230 . . . . . . . . . 10
172167, 169, 1713eqtr3d 2516 . . . . . . . . 9
173104, 108, 86, 87, 105, 130, 132, 80, 85, 153lmodsubdir 17437 . . . . . . . . . . . 12 Scalar
17486, 87clmsub 21446 . . . . . . . . . . . . . 14 CMod Scalar
17578, 80, 85, 174syl3anc 1228 . . . . . . . . . . . . 13 Scalar
176175oveq1d 6310 . . . . . . . . . . . 12 Scalar
177150oveq1d 6310 . . . . . . . . . . . . . 14
178 lmodabl 17426 . . . . . . . . . . . . . . . 16
179132, 178syl 16 . . . . . . . . . . . . . . 15
180104, 156, 105ablpncan2 16697 . . . . . . . . . . . . . . 15
181179, 116, 155, 180syl3anc 1228 . . . . . . . . . . . . . 14
182177, 181eqtrd 2508 . . . . . . . . . . . . 13
183182, 164oveq12d 6313 . . . . . . . . . . . 12
184173, 176, 1833eqtr4d 2518 . . . . . . . . . . 11
185104, 105grpnnncan2 16006 . . . . . . . . . . . 12
186101, 159, 103, 116, 185syl13anc 1230 . . . . . . . . . . 11
187184, 186eqtrd 2508 . . . . . . . . . 10
188187oveq2d 6311 . . . . . . . . 9
189165, 172, 1883eqtr2rd 2515 . . . . . . . 8
190104, 108, 86, 87, 77, 85, 89, 161, 118, 22, 189cvsmuleqdivd 21477 . . . . . . 7
191104, 108, 86, 87, 77, 89, 85, 161, 118, 163, 22, 190cvsdiveqd 21478 . . . . . 6
192148, 191eqtr4d 2511 . . . . 5
193104, 108, 86, 87, 77, 85, 89, 149, 161, 22, 163, 192cvsdiveqd 21478 . . . 4
194110, 115, 1933eqtr3rd 2517 . . 3
195 oveq1 6302 . . . . 5
196195eqeq2d 2481 . . . 4
197196rspcev 3219 . . 3
19876, 194, 197syl2anc 661 . 2
199 ttgval.n . . 3 toTG
200 ttgitvval.i . . 3 Itv
201199, 200, 104, 105, 108, 103, 102, 77, 159ttgelitv 24018 . 2
202198, 201mpbird 232 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wceq 1379   wcel 1767   wne 2662  wrex 2818   wss 3481   class class class wbr 4453  cfv 5594  (class class class)co 6295  cr 9503  cc0 9504  c1 9505   cmul 9509  cxr 9639   clt 9640   cle 9641   cmin 9817   cdiv 10218  crp 11232  cicc 11544  cbs 14506   cplusg 14571  Scalarcsca 14574  cvsca 14575  cgrp 15924  csg 15926  cabl 16670  clmod 17381  CModcclm 21428  CVecccvs 21470  Itvcitv 23696  toTGcttg 24008 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4564  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587  ax-cnex 9560  ax-resscn 9561  ax-1cn 9562  ax-icn 9563  ax-addcl 9564  ax-addrcl 9565  ax-mulcl 9566  ax-mulrcl 9567  ax-mulcom 9568  ax-addass 9569  ax-mulass 9570  ax-distr 9571  ax-i2m1 9572  ax-1ne0 9573  ax-1rid 9574  ax-rnegex 9575  ax-rrecex 9576  ax-cnre 9577  ax-pre-lttri 9578  ax-pre-lttrn 9579  ax-pre-ltadd 9580  ax-pre-mulgt0 9581  ax-addf 9583  ax-mulf 9584 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-fal 1385  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2822  df-rex 2823  df-reu 2824  df-rmo 2825  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-tp 4038  df-op 4040  df-uni 4252  df-int 4289  df-iun 4333  df-br 4454  df-opab 4512  df-mpt 4513  df-tr 4547  df-eprel 4797  df-id 4801  df-po 4806  df-so 4807  df-fr 4844  df-we 4846  df-ord 4887  df-on 4888  df-lim 4889  df-suc 4890  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-riota 6256  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-om 6696  df-1st 6795  df-2nd 6796  df-tpos 6967  df-recs 7054  df-rdg 7088  df-1o 7142  df-oadd 7146  df-er 7323  df-en 7529  df-dom 7530  df-sdom 7531  df-fin 7532  df-pnf 9642  df-mnf 9643  df-xr 9644  df-ltxr 9645  df-le 9646  df-sub 9819  df-neg 9820  df-div 10219  df-nn 10549  df-2 10606  df-3 10607  df-4 10608  df-5 10609  df-6 10610  df-7 10611  df-8 10612  df-9 10613  df-10 10614  df-n0 10808  df-z 10877  df-dec 10989  df-uz 11095  df-rp 11233  df-icc 11548  df-fz 11685  df-struct 14508  df-ndx 14509  df-slot 14510  df-base 14511  df-sets 14512  df-ress 14513  df-plusg 14584  df-mulr 14585  df-starv 14586  df-tset 14590  df-ple 14591  df-ds 14593  df-unif 14594  df-0g 14713  df-mgm 15745  df-sgrp 15784  df-mnd 15794  df-grp 15928  df-minusg 15929  df-sbg 15930  df-subg 16069  df-cmn 16671  df-abl 16672  df-mgp 17012  df-ur 17024  df-ring 17070  df-cring 17071  df-oppr 17142  df-dvdsr 17160  df-unit 17161  df-invr 17191  df-dvr 17202  df-drng 17267  df-subrg 17296  df-lmod 17383  df-lvec 17618  df-cnfld 18289  df-clm 21429  df-cvs 21471  df-itv 23698  df-lng 23699  df-ttg 24009 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator