Metamath Proof Explorer

Theorem constrext2chnlem

Description: Lemma for constrext2chn . (Contributed by Thierry Arnoux, 26-Oct-2025)

Ref Expression
Hypotheses constr0.1 
|- C = rec ( ( s e. _V |-> { x e. CC | ( E. a e. s E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. s E. b e. s E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. s E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) } ) , { 0 , 1 } )
constrextdg2.1 
|- E = ( CCfld |`s e )
constrextdg2.2 
|- F = ( CCfld |`s f )
constrextdg2.l 
|- .< = { <. f , e >. | ( E /FldExt F /\ ( E [:] F ) = 2 ) }
constrextdg2.n 
|- ( ph -> N e. _om )
constrext2chnlem.q 
|- Q = ( CCfld |`s QQ )
constrext2chnlem.l 
|- L = ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) )
constrext2chnlem.a 
|- ( ph -> A e. Constr )
Assertion constrext2chnlem 
|- ( ph -> E. n e. NN0 ( L [:] Q ) = ( 2 ^ n ) )

Proof

Step Hyp Ref Expression
1 constr0.1 
 |-  C = rec ( ( s e. _V |-> { x e. CC | ( E. a e. s E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. s E. b e. s E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. s E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) } ) , { 0 , 1 } )
2 constrextdg2.1 
 |-  E = ( CCfld |`s e )
3 constrextdg2.2 
 |-  F = ( CCfld |`s f )
4 constrextdg2.l 
 |-  .< = { <. f , e >. | ( E /FldExt F /\ ( E [:] F ) = 2 ) }
5 constrextdg2.n 
 |-  ( ph -> N e. _om )
6 constrext2chnlem.q 
 |-  Q = ( CCfld |`s QQ )
7 constrext2chnlem.l 
 |-  L = ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) )
8 constrext2chnlem.a 
 |-  ( ph -> A e. Constr )
9 2prm 
 |-  2 e. Prime
10 9 a1i 
 |-  ( ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ p e. NN0 ) /\ ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) ) -> 2 e. Prime )
11 7 6 oveq12i 
 |-  ( L [:] Q ) = ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) )
12 cnfldbas 
 |-  CC = ( Base ` CCfld )
13 eqid 
 |-  ( CCfld |`s QQ ) = ( CCfld |`s QQ )
14 eqid 
 |-  ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) = ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) )
15 cnfldfld 
 |-  CCfld e. Field
16 15 a1i 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> CCfld e. Field )
17 cndrng 
 |-  CCfld e. DivRing
18 qsubdrg 
 |-  ( QQ e. ( SubRing ` CCfld ) /\ ( CCfld |`s QQ ) e. DivRing )
19 18 simpli 
 |-  QQ e. ( SubRing ` CCfld )
20 18 simpri 
 |-  ( CCfld |`s QQ ) e. DivRing
21 issdrg 
 |-  ( QQ e. ( SubDRing ` CCfld ) <-> ( CCfld e. DivRing /\ QQ e. ( SubRing ` CCfld ) /\ ( CCfld |`s QQ ) e. DivRing ) )
22 17 19 20 21 mpbir3an 
 |-  QQ e. ( SubDRing ` CCfld )
23 22 a1i 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> QQ e. ( SubDRing ` CCfld ) )
24 nnon 
 |-  ( m e. _om -> m e. On )
25 24 adantl 
 |-  ( ( ph /\ m e. _om ) -> m e. On )
26 1 25 constrsscn 
 |-  ( ( ph /\ m e. _om ) -> ( C ` m ) C_ CC )
27 26 sselda 
 |-  ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) -> A e. CC )
28 27 snssd 
 |-  ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) -> { A } C_ CC )
29 28 ad2antrr 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> { A } C_ CC )
30 12 13 14 16 23 29 fldgenfldext 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) /FldExt ( CCfld |`s QQ ) )
31 30 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ p e. NN0 ) /\ ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) ) -> ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) /FldExt ( CCfld |`s QQ ) )
32 extdgcl 
 |-  ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) /FldExt ( CCfld |`s QQ ) -> ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) e. NN0* )
33 31 32 syl 
 |-  ( ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ p e. NN0 ) /\ ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) ) -> ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) e. NN0* )
34 simpr 
 |-  ( ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ p e. NN0 ) /\ ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) ) -> ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) )
35 2z 
 |-  2 e. ZZ
36 35 a1i 
 |-  ( ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ p e. NN0 ) /\ ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) ) -> 2 e. ZZ )
37 simplr 
 |-  ( ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ p e. NN0 ) /\ ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) ) -> p e. NN0 )
38 36 37 zexpcld 
 |-  ( ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ p e. NN0 ) /\ ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) ) -> ( 2 ^ p ) e. ZZ )
39 34 38 eqeltrd 
 |-  ( ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ p e. NN0 ) /\ ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) ) -> ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) e. ZZ )
40 39 zred 
 |-  ( ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ p e. NN0 ) /\ ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) ) -> ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) e. RR )
41 xnn0xr 
 |-  ( ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) e. NN0* -> ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) e. RR* )
42 31 32 41 3syl 
 |-  ( ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ p e. NN0 ) /\ ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) ) -> ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) e. RR* )
43 eqid 
 |-  ( Base ` ( CCfld |`s ( lastS ` v ) ) ) = ( Base ` ( CCfld |`s ( lastS ` v ) ) )
44 simplr 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> v e. ( .< Chain ( SubDRing ` CCfld ) ) )
45 simprl 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> ( v ` 0 ) = QQ )
46 45 oveq2d 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> ( CCfld |`s ( v ` 0 ) ) = ( CCfld |`s QQ ) )
47 eqidd 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> ( CCfld |`s ( lastS ` v ) ) = ( CCfld |`s ( lastS ` v ) ) )
48 simpr 
 |-  ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ v = (/) ) -> v = (/) )
49 48 fveq1d 
 |-  ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ v = (/) ) -> ( v ` 0 ) = ( (/) ` 0 ) )
50 0fv 
 |-  ( (/) ` 0 ) = (/)
51 50 a1i 
 |-  ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ v = (/) ) -> ( (/) ` 0 ) = (/) )
52 49 51 eqtrd 
 |-  ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ v = (/) ) -> ( v ` 0 ) = (/) )
53 45 adantr 
 |-  ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ v = (/) ) -> ( v ` 0 ) = QQ )
54 1nn 
 |-  1 e. NN
55 nnq 
 |-  ( 1 e. NN -> 1 e. QQ )
56 54 55 ax-mp 
 |-  1 e. QQ
57 56 ne0ii 
 |-  QQ =/= (/)
58 57 a1i 
 |-  ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ v = (/) ) -> QQ =/= (/) )
59 53 58 eqnetrd 
 |-  ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ v = (/) ) -> ( v ` 0 ) =/= (/) )
60 59 neneqd 
 |-  ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ v = (/) ) -> -. ( v ` 0 ) = (/) )
61 52 60 pm2.65da 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> -. v = (/) )
62 61 neqned 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> v =/= (/) )
63 44 62 hashne0 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> 0 < ( # ` v ) )
64 2 3 4 44 16 46 47 63 fldext2chn 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> ( ( CCfld |`s ( lastS ` v ) ) /FldExt ( CCfld |`s QQ ) /\ E. p e. NN0 ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) ) )
65 64 simpld 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> ( CCfld |`s ( lastS ` v ) ) /FldExt ( CCfld |`s QQ ) )
66 fldextfld1 
 |-  ( ( CCfld |`s ( lastS ` v ) ) /FldExt ( CCfld |`s QQ ) -> ( CCfld |`s ( lastS ` v ) ) e. Field )
67 65 66 syl 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> ( CCfld |`s ( lastS ` v ) ) e. Field )
68 44 chnwrd 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> v e. Word ( SubDRing ` CCfld ) )
69 lswcl 
 |-  ( ( v e. Word ( SubDRing ` CCfld ) /\ v =/= (/) ) -> ( lastS ` v ) e. ( SubDRing ` CCfld ) )
70 68 62 69 syl2anc 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> ( lastS ` v ) e. ( SubDRing ` CCfld ) )
71 17 a1i 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> CCfld e. DivRing )
72 qsscn 
 |-  QQ C_ CC
73 72 a1i 
 |-  ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) -> QQ C_ CC )
74 73 28 unssd 
 |-  ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) -> ( QQ u. { A } ) C_ CC )
75 74 ad2antrr 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> ( QQ u. { A } ) C_ CC )
76 12 71 75 fldgensdrg 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> ( CCfld fldGen ( QQ u. { A } ) ) e. ( SubDRing ` CCfld ) )
77 13 qrngbas 
 |-  QQ = ( Base ` ( CCfld |`s QQ ) )
78 77 65 fldextsdrg 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> QQ e. ( SubDRing ` ( CCfld |`s ( lastS ` v ) ) ) )
79 43 sdrgss 
 |-  ( QQ e. ( SubDRing ` ( CCfld |`s ( lastS ` v ) ) ) -> QQ C_ ( Base ` ( CCfld |`s ( lastS ` v ) ) ) )
80 78 79 syl 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> QQ C_ ( Base ` ( CCfld |`s ( lastS ` v ) ) ) )
81 12 sdrgss 
 |-  ( ( lastS ` v ) e. ( SubDRing ` CCfld ) -> ( lastS ` v ) C_ CC )
82 70 81 syl 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> ( lastS ` v ) C_ CC )
83 eqid 
 |-  ( CCfld |`s ( lastS ` v ) ) = ( CCfld |`s ( lastS ` v ) )
84 83 12 ressbas2 
 |-  ( ( lastS ` v ) C_ CC -> ( lastS ` v ) = ( Base ` ( CCfld |`s ( lastS ` v ) ) ) )
85 82 84 syl 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> ( lastS ` v ) = ( Base ` ( CCfld |`s ( lastS ` v ) ) ) )
86 80 85 sseqtrrd 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> QQ C_ ( lastS ` v ) )
87 simprr 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> ( C ` m ) C_ ( lastS ` v ) )
88 simpllr 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> A e. ( C ` m ) )
89 87 88 sseldd 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> A e. ( lastS ` v ) )
90 89 snssd 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> { A } C_ ( lastS ` v ) )
91 86 90 unssd 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> ( QQ u. { A } ) C_ ( lastS ` v ) )
92 12 71 70 91 fldgenssp 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> ( CCfld fldGen ( QQ u. { A } ) ) C_ ( lastS ` v ) )
93 id 
 |-  ( ( lastS ` v ) e. ( SubDRing ` CCfld ) -> ( lastS ` v ) e. ( SubDRing ` CCfld ) )
94 83 93 subsdrg 
 |-  ( ( lastS ` v ) e. ( SubDRing ` CCfld ) -> ( ( CCfld fldGen ( QQ u. { A } ) ) e. ( SubDRing ` ( CCfld |`s ( lastS ` v ) ) ) <-> ( ( CCfld fldGen ( QQ u. { A } ) ) e. ( SubDRing ` CCfld ) /\ ( CCfld fldGen ( QQ u. { A } ) ) C_ ( lastS ` v ) ) ) )
95 94 biimpar 
 |-  ( ( ( lastS ` v ) e. ( SubDRing ` CCfld ) /\ ( ( CCfld fldGen ( QQ u. { A } ) ) e. ( SubDRing ` CCfld ) /\ ( CCfld fldGen ( QQ u. { A } ) ) C_ ( lastS ` v ) ) ) -> ( CCfld fldGen ( QQ u. { A } ) ) e. ( SubDRing ` ( CCfld |`s ( lastS ` v ) ) ) )
96 70 76 92 95 syl12anc 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> ( CCfld fldGen ( QQ u. { A } ) ) e. ( SubDRing ` ( CCfld |`s ( lastS ` v ) ) ) )
97 43 67 96 sdrgfldext 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> ( CCfld |`s ( lastS ` v ) ) /FldExt ( ( CCfld |`s ( lastS ` v ) ) |`s ( CCfld fldGen ( QQ u. { A } ) ) ) )
98 70 elexd 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> ( lastS ` v ) e. _V )
99 ressabs 
 |-  ( ( ( lastS ` v ) e. _V /\ ( CCfld fldGen ( QQ u. { A } ) ) C_ ( lastS ` v ) ) -> ( ( CCfld |`s ( lastS ` v ) ) |`s ( CCfld fldGen ( QQ u. { A } ) ) ) = ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) )
100 98 92 99 syl2anc 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> ( ( CCfld |`s ( lastS ` v ) ) |`s ( CCfld fldGen ( QQ u. { A } ) ) ) = ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) )
101 97 100 breqtrd 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> ( CCfld |`s ( lastS ` v ) ) /FldExt ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) )
102 101 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ p e. NN0 ) /\ ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) ) -> ( CCfld |`s ( lastS ` v ) ) /FldExt ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) )
103 extdgcl 
 |-  ( ( CCfld |`s ( lastS ` v ) ) /FldExt ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) -> ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) ) e. NN0* )
104 102 103 syl 
 |-  ( ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ p e. NN0 ) /\ ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) ) -> ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) ) e. NN0* )
105 xnn0xr 
 |-  ( ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) ) e. NN0* -> ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) ) e. RR* )
106 104 105 syl 
 |-  ( ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ p e. NN0 ) /\ ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) ) -> ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) ) e. RR* )
107 extdggt0 
 |-  ( ( CCfld |`s ( lastS ` v ) ) /FldExt ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) -> 0 < ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) ) )
108 102 107 syl 
 |-  ( ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ p e. NN0 ) /\ ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) ) -> 0 < ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) ) )
109 extdgmul 
 |-  ( ( ( CCfld |`s ( lastS ` v ) ) /FldExt ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) /\ ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) /FldExt ( CCfld |`s QQ ) ) -> ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) ) *e ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) ) )
110 101 30 109 syl2anc 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) ) *e ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) ) )
111 110 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ p e. NN0 ) /\ ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) ) -> ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) ) *e ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) ) )
112 xmulcom 
 |-  ( ( ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) ) e. RR* /\ ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) e. RR* ) -> ( ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) ) *e ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) ) = ( ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) *e ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) ) ) )
113 106 42 112 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ p e. NN0 ) /\ ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) ) -> ( ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) ) *e ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) ) = ( ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) *e ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) ) ) )
114 111 113 eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ p e. NN0 ) /\ ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) ) -> ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) *e ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) ) ) )
115 40 42 106 108 114 rexmul2 
 |-  ( ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ p e. NN0 ) /\ ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) ) -> ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) e. RR )
116 extdggt0 
 |-  ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) /FldExt ( CCfld |`s QQ ) -> 0 < ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) )
117 31 116 syl 
 |-  ( ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ p e. NN0 ) /\ ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) ) -> 0 < ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) )
118 33 115 117 xnn0nnd 
 |-  ( ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ p e. NN0 ) /\ ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) ) -> ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) e. NN )
119 11 118 eqeltrid 
 |-  ( ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ p e. NN0 ) /\ ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) ) -> ( L [:] Q ) e. NN )
120 40 106 42 117 111 rexmul2 
 |-  ( ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ p e. NN0 ) /\ ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) ) -> ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) ) e. RR )
121 104 120 xnn0nn0d 
 |-  ( ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ p e. NN0 ) /\ ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) ) -> ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) ) e. NN0 )
122 121 nn0zd 
 |-  ( ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ p e. NN0 ) /\ ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) ) -> ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) ) e. ZZ )
123 118 nnnn0d 
 |-  ( ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ p e. NN0 ) /\ ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) ) -> ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) e. NN0 )
124 123 nn0zd 
 |-  ( ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ p e. NN0 ) /\ ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) ) -> ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) e. ZZ )
125 rexmul 
 |-  ( ( ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) ) e. RR /\ ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) e. RR ) -> ( ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) ) *e ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) ) = ( ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) ) x. ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) ) )
126 120 115 125 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ p e. NN0 ) /\ ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) ) -> ( ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) ) *e ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) ) = ( ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) ) x. ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) ) )
127 111 126 eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ p e. NN0 ) /\ ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) ) -> ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) ) x. ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) ) )
128 127 eqcomd 
 |-  ( ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ p e. NN0 ) /\ ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) ) -> ( ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) ) x. ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) ) = ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) )
129 128 34 eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ p e. NN0 ) /\ ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) ) -> ( ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) ) x. ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) ) = ( 2 ^ p ) )
130 dvds0lem 
 |-  ( ( ( ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) ) e. ZZ /\ ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) e. ZZ /\ ( 2 ^ p ) e. ZZ ) /\ ( ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) ) x. ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) ) = ( 2 ^ p ) ) -> ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) || ( 2 ^ p ) )
131 122 124 38 129 130 syl31anc 
 |-  ( ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ p e. NN0 ) /\ ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) ) -> ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) || ( 2 ^ p ) )
132 11 131 eqbrtrid 
 |-  ( ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ p e. NN0 ) /\ ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) ) -> ( L [:] Q ) || ( 2 ^ p ) )
133 dvdsprmpweq 
 |-  ( ( 2 e. Prime /\ ( L [:] Q ) e. NN /\ p e. NN0 ) -> ( ( L [:] Q ) || ( 2 ^ p ) -> E. n e. NN0 ( L [:] Q ) = ( 2 ^ n ) ) )
134 133 imp 
 |-  ( ( ( 2 e. Prime /\ ( L [:] Q ) e. NN /\ p e. NN0 ) /\ ( L [:] Q ) || ( 2 ^ p ) ) -> E. n e. NN0 ( L [:] Q ) = ( 2 ^ n ) )
135 10 119 37 132 134 syl31anc 
 |-  ( ( ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) /\ p e. NN0 ) /\ ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) ) -> E. n e. NN0 ( L [:] Q ) = ( 2 ^ n ) )
136 64 simprd 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> E. p e. NN0 ( ( CCfld |`s ( lastS ` v ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ p ) )
137 135 136 r19.29a 
 |-  ( ( ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) ) -> E. n e. NN0 ( L [:] Q ) = ( 2 ^ n ) )
138 simplr 
 |-  ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) -> m e. _om )
139 1 2 3 4 138 constrextdg2 
 |-  ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) -> E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) )
140 137 139 r19.29a 
 |-  ( ( ( ph /\ m e. _om ) /\ A e. ( C ` m ) ) -> E. n e. NN0 ( L [:] Q ) = ( 2 ^ n ) )
141 1 isconstr 
 |-  ( A e. Constr <-> E. m e. _om A e. ( C ` m ) )
142 8 141 sylib 
 |-  ( ph -> E. m e. _om A e. ( C ` m ) )
143 140 142 r19.29a 
 |-  ( ph -> E. n e. NN0 ( L [:] Q ) = ( 2 ^ n ) )