Metamath Proof Explorer

Theorem fldext2chn

Description: In a non-empty chain T of quadratic field extensions, the degree of the final extension is always a power of two. (Contributed by Thierry Arnoux, 19-Oct-2025)

Ref Expression
Hypotheses fldext2chn.e 
|- E = ( W |`s e )
fldext2chn.f 
|- F = ( W |`s f )
fldext2chn.l 
|- .< = { <. f , e >. | ( E /FldExt F /\ ( E [:] F ) = 2 ) }
fldext2chn.t 
|- ( ph -> T e. ( .< Chain ( SubDRing ` W ) ) )
fldext2chn.w 
|- ( ph -> W e. Field )
fldext2chn.1 
|- ( ph -> ( W |`s ( T ` 0 ) ) = Q )
fldext2chn.2 
|- ( ph -> ( W |`s ( lastS ` T ) ) = L )
fldext2chn.3 
|- ( ph -> 0 < ( # ` T ) )
Assertion fldext2chn 
|- ( ph -> ( L /FldExt Q /\ E. n e. NN0 ( L [:] Q ) = ( 2 ^ n ) ) )

Proof

Step Hyp Ref Expression
1 fldext2chn.e 
 |-  E = ( W |`s e )
2 fldext2chn.f 
 |-  F = ( W |`s f )
3 fldext2chn.l 
 |-  .< = { <. f , e >. | ( E /FldExt F /\ ( E [:] F ) = 2 ) }
4 fldext2chn.t 
 |-  ( ph -> T e. ( .< Chain ( SubDRing ` W ) ) )
5 fldext2chn.w 
 |-  ( ph -> W e. Field )
6 fldext2chn.1 
 |-  ( ph -> ( W |`s ( T ` 0 ) ) = Q )
7 fldext2chn.2 
 |-  ( ph -> ( W |`s ( lastS ` T ) ) = L )
8 fldext2chn.3 
 |-  ( ph -> 0 < ( # ` T ) )
9 fveq2 
 |-  ( d = (/) -> ( # ` d ) = ( # ` (/) ) )
10 9 breq2d 
 |-  ( d = (/) -> ( 0 < ( # ` d ) <-> 0 < ( # ` (/) ) ) )
11 fveq2 
 |-  ( d = (/) -> ( lastS ` d ) = ( lastS ` (/) ) )
12 11 oveq2d 
 |-  ( d = (/) -> ( W |`s ( lastS ` d ) ) = ( W |`s ( lastS ` (/) ) ) )
13 fveq1 
 |-  ( d = (/) -> ( d ` 0 ) = ( (/) ` 0 ) )
14 13 oveq2d 
 |-  ( d = (/) -> ( W |`s ( d ` 0 ) ) = ( W |`s ( (/) ` 0 ) ) )
15 12 14 breq12d 
 |-  ( d = (/) -> ( ( W |`s ( lastS ` d ) ) /FldExt ( W |`s ( d ` 0 ) ) <-> ( W |`s ( lastS ` (/) ) ) /FldExt ( W |`s ( (/) ` 0 ) ) ) )
16 12 14 oveq12d 
 |-  ( d = (/) -> ( ( W |`s ( lastS ` d ) ) [:] ( W |`s ( d ` 0 ) ) ) = ( ( W |`s ( lastS ` (/) ) ) [:] ( W |`s ( (/) ` 0 ) ) ) )
17 16 eqeq1d 
 |-  ( d = (/) -> ( ( ( W |`s ( lastS ` d ) ) [:] ( W |`s ( d ` 0 ) ) ) = ( 2 ^ n ) <-> ( ( W |`s ( lastS ` (/) ) ) [:] ( W |`s ( (/) ` 0 ) ) ) = ( 2 ^ n ) ) )
18 17 rexbidv 
 |-  ( d = (/) -> ( E. n e. NN0 ( ( W |`s ( lastS ` d ) ) [:] ( W |`s ( d ` 0 ) ) ) = ( 2 ^ n ) <-> E. n e. NN0 ( ( W |`s ( lastS ` (/) ) ) [:] ( W |`s ( (/) ` 0 ) ) ) = ( 2 ^ n ) ) )
19 15 18 anbi12d 
 |-  ( d = (/) -> ( ( ( W |`s ( lastS ` d ) ) /FldExt ( W |`s ( d ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` d ) ) [:] ( W |`s ( d ` 0 ) ) ) = ( 2 ^ n ) ) <-> ( ( W |`s ( lastS ` (/) ) ) /FldExt ( W |`s ( (/) ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` (/) ) ) [:] ( W |`s ( (/) ` 0 ) ) ) = ( 2 ^ n ) ) ) )
20 10 19 imbi12d 
 |-  ( d = (/) -> ( ( 0 < ( # ` d ) -> ( ( W |`s ( lastS ` d ) ) /FldExt ( W |`s ( d ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` d ) ) [:] ( W |`s ( d ` 0 ) ) ) = ( 2 ^ n ) ) ) <-> ( 0 < ( # ` (/) ) -> ( ( W |`s ( lastS ` (/) ) ) /FldExt ( W |`s ( (/) ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` (/) ) ) [:] ( W |`s ( (/) ` 0 ) ) ) = ( 2 ^ n ) ) ) ) )
21 fveq2 
 |-  ( d = c -> ( # ` d ) = ( # ` c ) )
22 21 breq2d 
 |-  ( d = c -> ( 0 < ( # ` d ) <-> 0 < ( # ` c ) ) )
23 fveq2 
 |-  ( d = c -> ( lastS ` d ) = ( lastS ` c ) )
24 23 oveq2d 
 |-  ( d = c -> ( W |`s ( lastS ` d ) ) = ( W |`s ( lastS ` c ) ) )
25 fveq1 
 |-  ( d = c -> ( d ` 0 ) = ( c ` 0 ) )
26 25 oveq2d 
 |-  ( d = c -> ( W |`s ( d ` 0 ) ) = ( W |`s ( c ` 0 ) ) )
27 24 26 breq12d 
 |-  ( d = c -> ( ( W |`s ( lastS ` d ) ) /FldExt ( W |`s ( d ` 0 ) ) <-> ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) ) )
28 24 26 oveq12d 
 |-  ( d = c -> ( ( W |`s ( lastS ` d ) ) [:] ( W |`s ( d ` 0 ) ) ) = ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) )
29 28 eqeq1d 
 |-  ( d = c -> ( ( ( W |`s ( lastS ` d ) ) [:] ( W |`s ( d ` 0 ) ) ) = ( 2 ^ n ) <-> ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) )
30 29 rexbidv 
 |-  ( d = c -> ( E. n e. NN0 ( ( W |`s ( lastS ` d ) ) [:] ( W |`s ( d ` 0 ) ) ) = ( 2 ^ n ) <-> E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) )
31 27 30 anbi12d 
 |-  ( d = c -> ( ( ( W |`s ( lastS ` d ) ) /FldExt ( W |`s ( d ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` d ) ) [:] ( W |`s ( d ` 0 ) ) ) = ( 2 ^ n ) ) <-> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) )
32 22 31 imbi12d 
 |-  ( d = c -> ( ( 0 < ( # ` d ) -> ( ( W |`s ( lastS ` d ) ) /FldExt ( W |`s ( d ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` d ) ) [:] ( W |`s ( d ` 0 ) ) ) = ( 2 ^ n ) ) ) <-> ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) )
33 fveq2 
 |-  ( d = ( c ++ <" g "> ) -> ( # ` d ) = ( # ` ( c ++ <" g "> ) ) )
34 33 breq2d 
 |-  ( d = ( c ++ <" g "> ) -> ( 0 < ( # ` d ) <-> 0 < ( # ` ( c ++ <" g "> ) ) ) )
35 fveq2 
 |-  ( d = ( c ++ <" g "> ) -> ( lastS ` d ) = ( lastS ` ( c ++ <" g "> ) ) )
36 35 oveq2d 
 |-  ( d = ( c ++ <" g "> ) -> ( W |`s ( lastS ` d ) ) = ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) )
37 fveq1 
 |-  ( d = ( c ++ <" g "> ) -> ( d ` 0 ) = ( ( c ++ <" g "> ) ` 0 ) )
38 37 oveq2d 
 |-  ( d = ( c ++ <" g "> ) -> ( W |`s ( d ` 0 ) ) = ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) )
39 36 38 breq12d 
 |-  ( d = ( c ++ <" g "> ) -> ( ( W |`s ( lastS ` d ) ) /FldExt ( W |`s ( d ` 0 ) ) <-> ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) /FldExt ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) ) )
40 36 38 oveq12d 
 |-  ( d = ( c ++ <" g "> ) -> ( ( W |`s ( lastS ` d ) ) [:] ( W |`s ( d ` 0 ) ) ) = ( ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) [:] ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) ) )
41 40 eqeq1d 
 |-  ( d = ( c ++ <" g "> ) -> ( ( ( W |`s ( lastS ` d ) ) [:] ( W |`s ( d ` 0 ) ) ) = ( 2 ^ n ) <-> ( ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) [:] ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) ) = ( 2 ^ n ) ) )
42 41 rexbidv 
 |-  ( d = ( c ++ <" g "> ) -> ( E. n e. NN0 ( ( W |`s ( lastS ` d ) ) [:] ( W |`s ( d ` 0 ) ) ) = ( 2 ^ n ) <-> E. n e. NN0 ( ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) [:] ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) ) = ( 2 ^ n ) ) )
43 oveq2 
 |-  ( n = m -> ( 2 ^ n ) = ( 2 ^ m ) )
44 43 eqeq2d 
 |-  ( n = m -> ( ( ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) [:] ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) ) = ( 2 ^ n ) <-> ( ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) [:] ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) ) = ( 2 ^ m ) ) )
45 44 cbvrexvw 
 |-  ( E. n e. NN0 ( ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) [:] ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) ) = ( 2 ^ n ) <-> E. m e. NN0 ( ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) [:] ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) ) = ( 2 ^ m ) )
46 42 45 bitrdi 
 |-  ( d = ( c ++ <" g "> ) -> ( E. n e. NN0 ( ( W |`s ( lastS ` d ) ) [:] ( W |`s ( d ` 0 ) ) ) = ( 2 ^ n ) <-> E. m e. NN0 ( ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) [:] ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) ) = ( 2 ^ m ) ) )
47 39 46 anbi12d 
 |-  ( d = ( c ++ <" g "> ) -> ( ( ( W |`s ( lastS ` d ) ) /FldExt ( W |`s ( d ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` d ) ) [:] ( W |`s ( d ` 0 ) ) ) = ( 2 ^ n ) ) <-> ( ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) /FldExt ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) /\ E. m e. NN0 ( ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) [:] ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) ) = ( 2 ^ m ) ) ) )
48 34 47 imbi12d 
 |-  ( d = ( c ++ <" g "> ) -> ( ( 0 < ( # ` d ) -> ( ( W |`s ( lastS ` d ) ) /FldExt ( W |`s ( d ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` d ) ) [:] ( W |`s ( d ` 0 ) ) ) = ( 2 ^ n ) ) ) <-> ( 0 < ( # ` ( c ++ <" g "> ) ) -> ( ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) /FldExt ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) /\ E. m e. NN0 ( ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) [:] ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) ) = ( 2 ^ m ) ) ) ) )
49 fveq2 
 |-  ( d = T -> ( # ` d ) = ( # ` T ) )
50 49 breq2d 
 |-  ( d = T -> ( 0 < ( # ` d ) <-> 0 < ( # ` T ) ) )
51 fveq2 
 |-  ( d = T -> ( lastS ` d ) = ( lastS ` T ) )
52 51 oveq2d 
 |-  ( d = T -> ( W |`s ( lastS ` d ) ) = ( W |`s ( lastS ` T ) ) )
53 fveq1 
 |-  ( d = T -> ( d ` 0 ) = ( T ` 0 ) )
54 53 oveq2d 
 |-  ( d = T -> ( W |`s ( d ` 0 ) ) = ( W |`s ( T ` 0 ) ) )
55 52 54 breq12d 
 |-  ( d = T -> ( ( W |`s ( lastS ` d ) ) /FldExt ( W |`s ( d ` 0 ) ) <-> ( W |`s ( lastS ` T ) ) /FldExt ( W |`s ( T ` 0 ) ) ) )
56 52 54 oveq12d 
 |-  ( d = T -> ( ( W |`s ( lastS ` d ) ) [:] ( W |`s ( d ` 0 ) ) ) = ( ( W |`s ( lastS ` T ) ) [:] ( W |`s ( T ` 0 ) ) ) )
57 56 eqeq1d 
 |-  ( d = T -> ( ( ( W |`s ( lastS ` d ) ) [:] ( W |`s ( d ` 0 ) ) ) = ( 2 ^ n ) <-> ( ( W |`s ( lastS ` T ) ) [:] ( W |`s ( T ` 0 ) ) ) = ( 2 ^ n ) ) )
58 57 rexbidv 
 |-  ( d = T -> ( E. n e. NN0 ( ( W |`s ( lastS ` d ) ) [:] ( W |`s ( d ` 0 ) ) ) = ( 2 ^ n ) <-> E. n e. NN0 ( ( W |`s ( lastS ` T ) ) [:] ( W |`s ( T ` 0 ) ) ) = ( 2 ^ n ) ) )
59 55 58 anbi12d 
 |-  ( d = T -> ( ( ( W |`s ( lastS ` d ) ) /FldExt ( W |`s ( d ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` d ) ) [:] ( W |`s ( d ` 0 ) ) ) = ( 2 ^ n ) ) <-> ( ( W |`s ( lastS ` T ) ) /FldExt ( W |`s ( T ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` T ) ) [:] ( W |`s ( T ` 0 ) ) ) = ( 2 ^ n ) ) ) )
60 50 59 imbi12d 
 |-  ( d = T -> ( ( 0 < ( # ` d ) -> ( ( W |`s ( lastS ` d ) ) /FldExt ( W |`s ( d ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` d ) ) [:] ( W |`s ( d ` 0 ) ) ) = ( 2 ^ n ) ) ) <-> ( 0 < ( # ` T ) -> ( ( W |`s ( lastS ` T ) ) /FldExt ( W |`s ( T ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` T ) ) [:] ( W |`s ( T ` 0 ) ) ) = ( 2 ^ n ) ) ) ) )
61 0re 
 |-  0 e. RR
62 61 ltnri 
 |-  -. 0 < 0
63 62 a1i 
 |-  ( ph -> -. 0 < 0 )
64 hash0 
 |-  ( # ` (/) ) = 0
65 64 breq2i 
 |-  ( 0 < ( # ` (/) ) <-> 0 < 0 )
66 63 65 sylnibr 
 |-  ( ph -> -. 0 < ( # ` (/) ) )
67 66 pm2.21d 
 |-  ( ph -> ( 0 < ( # ` (/) ) -> ( ( W |`s ( lastS ` (/) ) ) /FldExt ( W |`s ( (/) ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` (/) ) ) [:] ( W |`s ( (/) ` 0 ) ) ) = ( 2 ^ n ) ) ) )
68 5 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c = (/) ) -> W e. Field )
69 simp-5r 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c = (/) ) -> g e. ( SubDRing ` W ) )
70 fldsdrgfld 
 |-  ( ( W e. Field /\ g e. ( SubDRing ` W ) ) -> ( W |`s g ) e. Field )
71 68 69 70 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c = (/) ) -> ( W |`s g ) e. Field )
72 fldextid 
 |-  ( ( W |`s g ) e. Field -> ( W |`s g ) /FldExt ( W |`s g ) )
73 71 72 syl 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c = (/) ) -> ( W |`s g ) /FldExt ( W |`s g ) )
74 simp-5r 
 |-  ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) -> c e. ( .< Chain ( SubDRing ` W ) ) )
75 74 chnwrd 
 |-  ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) -> c e. Word ( SubDRing ` W ) )
76 75 adantr 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c = (/) ) -> c e. Word ( SubDRing ` W ) )
77 lswccats1 
 |-  ( ( c e. Word ( SubDRing ` W ) /\ g e. ( SubDRing ` W ) ) -> ( lastS ` ( c ++ <" g "> ) ) = g )
78 76 69 77 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c = (/) ) -> ( lastS ` ( c ++ <" g "> ) ) = g )
79 78 oveq2d 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c = (/) ) -> ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) = ( W |`s g ) )
80 simpr 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c = (/) ) -> c = (/) )
81 80 oveq1d 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c = (/) ) -> ( c ++ <" g "> ) = ( (/) ++ <" g "> ) )
82 s0s1 
 |-  <" g "> = ( (/) ++ <" g "> )
83 81 82 eqtr4di 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c = (/) ) -> ( c ++ <" g "> ) = <" g "> )
84 83 fveq1d 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c = (/) ) -> ( ( c ++ <" g "> ) ` 0 ) = ( <" g "> ` 0 ) )
85 s1fv 
 |-  ( g e. ( SubDRing ` W ) -> ( <" g "> ` 0 ) = g )
86 69 85 syl 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c = (/) ) -> ( <" g "> ` 0 ) = g )
87 84 86 eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c = (/) ) -> ( ( c ++ <" g "> ) ` 0 ) = g )
88 87 oveq2d 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c = (/) ) -> ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) = ( W |`s g ) )
89 73 79 88 3brtr4d 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c = (/) ) -> ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) /FldExt ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) )
90 oveq2 
 |-  ( m = 0 -> ( 2 ^ m ) = ( 2 ^ 0 ) )
91 2cn 
 |-  2 e. CC
92 exp0 
 |-  ( 2 e. CC -> ( 2 ^ 0 ) = 1 )
93 91 92 ax-mp 
 |-  ( 2 ^ 0 ) = 1
94 90 93 eqtrdi 
 |-  ( m = 0 -> ( 2 ^ m ) = 1 )
95 94 eqeq2d 
 |-  ( m = 0 -> ( ( ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) [:] ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) ) = ( 2 ^ m ) <-> ( ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) [:] ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) ) = 1 ) )
96 0nn0 
 |-  0 e. NN0
97 96 a1i 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c = (/) ) -> 0 e. NN0 )
98 79 88 oveq12d 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c = (/) ) -> ( ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) [:] ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) ) = ( ( W |`s g ) [:] ( W |`s g ) ) )
99 extdgid 
 |-  ( ( W |`s g ) e. Field -> ( ( W |`s g ) [:] ( W |`s g ) ) = 1 )
100 71 99 syl 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c = (/) ) -> ( ( W |`s g ) [:] ( W |`s g ) ) = 1 )
101 98 100 eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c = (/) ) -> ( ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) [:] ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) ) = 1 )
102 95 97 101 rspcedvdw 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c = (/) ) -> E. m e. NN0 ( ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) [:] ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) ) = ( 2 ^ m ) )
103 89 102 jca 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c = (/) ) -> ( ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) /FldExt ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) /\ E. m e. NN0 ( ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) [:] ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) ) = ( 2 ^ m ) ) )
104 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> ( c = (/) \/ ( lastS ` c ) .< g ) )
105 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> c =/= (/) )
106 105 neneqd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> -. c = (/) )
107 104 106 orcnd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> ( lastS ` c ) .< g )
108 75 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> c e. Word ( SubDRing ` W ) )
109 lswcl 
 |-  ( ( c e. Word ( SubDRing ` W ) /\ c =/= (/) ) -> ( lastS ` c ) e. ( SubDRing ` W ) )
110 108 105 109 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> ( lastS ` c ) e. ( SubDRing ` W ) )
111 simp-7r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> g e. ( SubDRing ` W ) )
112 1 2 breq12i 
 |-  ( E /FldExt F <-> ( W |`s e ) /FldExt ( W |`s f ) )
113 1 2 oveq12i 
 |-  ( E [:] F ) = ( ( W |`s e ) [:] ( W |`s f ) )
114 113 eqeq1i 
 |-  ( ( E [:] F ) = 2 <-> ( ( W |`s e ) [:] ( W |`s f ) ) = 2 )
115 112 114 anbi12i 
 |-  ( ( E /FldExt F /\ ( E [:] F ) = 2 ) <-> ( ( W |`s e ) /FldExt ( W |`s f ) /\ ( ( W |`s e ) [:] ( W |`s f ) ) = 2 ) )
116 oveq2 
 |-  ( e = g -> ( W |`s e ) = ( W |`s g ) )
117 116 adantr 
 |-  ( ( e = g /\ f = ( lastS ` c ) ) -> ( W |`s e ) = ( W |`s g ) )
118 oveq2 
 |-  ( f = ( lastS ` c ) -> ( W |`s f ) = ( W |`s ( lastS ` c ) ) )
119 118 adantl 
 |-  ( ( e = g /\ f = ( lastS ` c ) ) -> ( W |`s f ) = ( W |`s ( lastS ` c ) ) )
120 117 119 breq12d 
 |-  ( ( e = g /\ f = ( lastS ` c ) ) -> ( ( W |`s e ) /FldExt ( W |`s f ) <-> ( W |`s g ) /FldExt ( W |`s ( lastS ` c ) ) ) )
121 117 119 oveq12d 
 |-  ( ( e = g /\ f = ( lastS ` c ) ) -> ( ( W |`s e ) [:] ( W |`s f ) ) = ( ( W |`s g ) [:] ( W |`s ( lastS ` c ) ) ) )
122 121 eqeq1d 
 |-  ( ( e = g /\ f = ( lastS ` c ) ) -> ( ( ( W |`s e ) [:] ( W |`s f ) ) = 2 <-> ( ( W |`s g ) [:] ( W |`s ( lastS ` c ) ) ) = 2 ) )
123 120 122 anbi12d 
 |-  ( ( e = g /\ f = ( lastS ` c ) ) -> ( ( ( W |`s e ) /FldExt ( W |`s f ) /\ ( ( W |`s e ) [:] ( W |`s f ) ) = 2 ) <-> ( ( W |`s g ) /FldExt ( W |`s ( lastS ` c ) ) /\ ( ( W |`s g ) [:] ( W |`s ( lastS ` c ) ) ) = 2 ) ) )
124 115 123 bitrid 
 |-  ( ( e = g /\ f = ( lastS ` c ) ) -> ( ( E /FldExt F /\ ( E [:] F ) = 2 ) <-> ( ( W |`s g ) /FldExt ( W |`s ( lastS ` c ) ) /\ ( ( W |`s g ) [:] ( W |`s ( lastS ` c ) ) ) = 2 ) ) )
125 124 ancoms 
 |-  ( ( f = ( lastS ` c ) /\ e = g ) -> ( ( E /FldExt F /\ ( E [:] F ) = 2 ) <-> ( ( W |`s g ) /FldExt ( W |`s ( lastS ` c ) ) /\ ( ( W |`s g ) [:] ( W |`s ( lastS ` c ) ) ) = 2 ) ) )
126 125 3 brabga 
 |-  ( ( ( lastS ` c ) e. ( SubDRing ` W ) /\ g e. ( SubDRing ` W ) ) -> ( ( lastS ` c ) .< g <-> ( ( W |`s g ) /FldExt ( W |`s ( lastS ` c ) ) /\ ( ( W |`s g ) [:] ( W |`s ( lastS ` c ) ) ) = 2 ) ) )
127 110 111 126 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> ( ( lastS ` c ) .< g <-> ( ( W |`s g ) /FldExt ( W |`s ( lastS ` c ) ) /\ ( ( W |`s g ) [:] ( W |`s ( lastS ` c ) ) ) = 2 ) ) )
128 107 127 mpbid 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> ( ( W |`s g ) /FldExt ( W |`s ( lastS ` c ) ) /\ ( ( W |`s g ) [:] ( W |`s ( lastS ` c ) ) ) = 2 ) )
129 128 simpld 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> ( W |`s g ) /FldExt ( W |`s ( lastS ` c ) ) )
130 hashgt0 
 |-  ( ( c e. ( .< Chain ( SubDRing ` W ) ) /\ c =/= (/) ) -> 0 < ( # ` c ) )
131 74 130 sylan 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) -> 0 < ( # ` c ) )
132 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) -> ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) )
133 131 132 mpd 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) )
134 133 simprd 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) -> E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) )
135 oveq2 
 |-  ( n = o -> ( 2 ^ n ) = ( 2 ^ o ) )
136 135 eqeq2d 
 |-  ( n = o -> ( ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) <-> ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) )
137 136 cbvrexvw 
 |-  ( E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) <-> E. o e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) )
138 134 137 sylib 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) -> E. o e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) )
139 129 138 r19.29a 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) -> ( W |`s g ) /FldExt ( W |`s ( lastS ` c ) ) )
140 133 simpld 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) -> ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) )
141 fldexttr 
 |-  ( ( ( W |`s g ) /FldExt ( W |`s ( lastS ` c ) ) /\ ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) ) -> ( W |`s g ) /FldExt ( W |`s ( c ` 0 ) ) )
142 139 140 141 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) -> ( W |`s g ) /FldExt ( W |`s ( c ` 0 ) ) )
143 108 111 77 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> ( lastS ` ( c ++ <" g "> ) ) = g )
144 143 oveq2d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) = ( W |`s g ) )
145 144 138 r19.29a 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) -> ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) = ( W |`s g ) )
146 111 s1cld 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> <" g "> e. Word ( SubDRing ` W ) )
147 131 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> 0 < ( # ` c ) )
148 ccatfv0 
 |-  ( ( c e. Word ( SubDRing ` W ) /\ <" g "> e. Word ( SubDRing ` W ) /\ 0 < ( # ` c ) ) -> ( ( c ++ <" g "> ) ` 0 ) = ( c ` 0 ) )
149 108 146 147 148 syl3anc 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> ( ( c ++ <" g "> ) ` 0 ) = ( c ` 0 ) )
150 149 oveq2d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) = ( W |`s ( c ` 0 ) ) )
151 150 138 r19.29a 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) -> ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) = ( W |`s ( c ` 0 ) ) )
152 142 145 151 3brtr4d 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) -> ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) /FldExt ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) )
153 oveq2 
 |-  ( m = ( o + 1 ) -> ( 2 ^ m ) = ( 2 ^ ( o + 1 ) ) )
154 153 eqeq2d 
 |-  ( m = ( o + 1 ) -> ( ( ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) [:] ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) ) = ( 2 ^ m ) <-> ( ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) [:] ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) ) = ( 2 ^ ( o + 1 ) ) ) )
155 simplr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> o e. NN0 )
156 1nn0 
 |-  1 e. NN0
157 156 a1i 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> 1 e. NN0 )
158 155 157 nn0addcld 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> ( o + 1 ) e. NN0 )
159 144 150 oveq12d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> ( ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) [:] ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) ) = ( ( W |`s g ) [:] ( W |`s ( c ` 0 ) ) ) )
160 140 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) )
161 extdgmul 
 |-  ( ( ( W |`s g ) /FldExt ( W |`s ( lastS ` c ) ) /\ ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) ) -> ( ( W |`s g ) [:] ( W |`s ( c ` 0 ) ) ) = ( ( ( W |`s g ) [:] ( W |`s ( lastS ` c ) ) ) *e ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) ) )
162 129 160 161 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> ( ( W |`s g ) [:] ( W |`s ( c ` 0 ) ) ) = ( ( ( W |`s g ) [:] ( W |`s ( lastS ` c ) ) ) *e ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) ) )
163 91 a1i 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> 2 e. CC )
164 163 155 expcld 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> ( 2 ^ o ) e. CC )
165 163 164 mulcomd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> ( 2 x. ( 2 ^ o ) ) = ( ( 2 ^ o ) x. 2 ) )
166 128 simprd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> ( ( W |`s g ) [:] ( W |`s ( lastS ` c ) ) ) = 2 )
167 simpr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) )
168 166 167 oveq12d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> ( ( ( W |`s g ) [:] ( W |`s ( lastS ` c ) ) ) *e ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) ) = ( 2 *e ( 2 ^ o ) ) )
169 2re 
 |-  2 e. RR
170 169 a1i 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> 2 e. RR )
171 170 155 reexpcld 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> ( 2 ^ o ) e. RR )
172 rexmul 
 |-  ( ( 2 e. RR /\ ( 2 ^ o ) e. RR ) -> ( 2 *e ( 2 ^ o ) ) = ( 2 x. ( 2 ^ o ) ) )
173 170 171 172 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> ( 2 *e ( 2 ^ o ) ) = ( 2 x. ( 2 ^ o ) ) )
174 168 173 eqtrd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> ( ( ( W |`s g ) [:] ( W |`s ( lastS ` c ) ) ) *e ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) ) = ( 2 x. ( 2 ^ o ) ) )
175 163 155 expp1d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> ( 2 ^ ( o + 1 ) ) = ( ( 2 ^ o ) x. 2 ) )
176 165 174 175 3eqtr4d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> ( ( ( W |`s g ) [:] ( W |`s ( lastS ` c ) ) ) *e ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) ) = ( 2 ^ ( o + 1 ) ) )
177 159 162 176 3eqtrd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> ( ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) [:] ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) ) = ( 2 ^ ( o + 1 ) ) )
178 154 158 177 rspcedvdw 
 |-  ( ( ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) /\ o e. NN0 ) /\ ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ o ) ) -> E. m e. NN0 ( ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) [:] ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) ) = ( 2 ^ m ) )
179 178 138 r19.29a 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) -> E. m e. NN0 ( ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) [:] ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) ) = ( 2 ^ m ) )
180 152 179 jca 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) /\ c =/= (/) ) -> ( ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) /FldExt ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) /\ E. m e. NN0 ( ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) [:] ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) ) = ( 2 ^ m ) ) )
181 103 180 pm2.61dane 
 |-  ( ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) /\ 0 < ( # ` ( c ++ <" g "> ) ) ) -> ( ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) /FldExt ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) /\ E. m e. NN0 ( ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) [:] ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) ) = ( 2 ^ m ) ) )
182 181 ex 
 |-  ( ( ( ( ( ph /\ c e. ( .< Chain ( SubDRing ` W ) ) ) /\ g e. ( SubDRing ` W ) ) /\ ( c = (/) \/ ( lastS ` c ) .< g ) ) /\ ( 0 < ( # ` c ) -> ( ( W |`s ( lastS ` c ) ) /FldExt ( W |`s ( c ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` c ) ) [:] ( W |`s ( c ` 0 ) ) ) = ( 2 ^ n ) ) ) ) -> ( 0 < ( # ` ( c ++ <" g "> ) ) -> ( ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) /FldExt ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) /\ E. m e. NN0 ( ( W |`s ( lastS ` ( c ++ <" g "> ) ) ) [:] ( W |`s ( ( c ++ <" g "> ) ` 0 ) ) ) = ( 2 ^ m ) ) ) )
183 20 32 48 60 4 67 182 chnind 
 |-  ( ph -> ( 0 < ( # ` T ) -> ( ( W |`s ( lastS ` T ) ) /FldExt ( W |`s ( T ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` T ) ) [:] ( W |`s ( T ` 0 ) ) ) = ( 2 ^ n ) ) ) )
184 8 183 mpd 
 |-  ( ph -> ( ( W |`s ( lastS ` T ) ) /FldExt ( W |`s ( T ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` T ) ) [:] ( W |`s ( T ` 0 ) ) ) = ( 2 ^ n ) ) )
185 7 6 breq12d 
 |-  ( ph -> ( ( W |`s ( lastS ` T ) ) /FldExt ( W |`s ( T ` 0 ) ) <-> L /FldExt Q ) )
186 7 6 oveq12d 
 |-  ( ph -> ( ( W |`s ( lastS ` T ) ) [:] ( W |`s ( T ` 0 ) ) ) = ( L [:] Q ) )
187 186 eqeq1d 
 |-  ( ph -> ( ( ( W |`s ( lastS ` T ) ) [:] ( W |`s ( T ` 0 ) ) ) = ( 2 ^ n ) <-> ( L [:] Q ) = ( 2 ^ n ) ) )
188 187 rexbidv 
 |-  ( ph -> ( E. n e. NN0 ( ( W |`s ( lastS ` T ) ) [:] ( W |`s ( T ` 0 ) ) ) = ( 2 ^ n ) <-> E. n e. NN0 ( L [:] Q ) = ( 2 ^ n ) ) )
189 185 188 anbi12d 
 |-  ( ph -> ( ( ( W |`s ( lastS ` T ) ) /FldExt ( W |`s ( T ` 0 ) ) /\ E. n e. NN0 ( ( W |`s ( lastS ` T ) ) [:] ( W |`s ( T ` 0 ) ) ) = ( 2 ^ n ) ) <-> ( L /FldExt Q /\ E. n e. NN0 ( L [:] Q ) = ( 2 ^ n ) ) ) )
190 184 189 mpbid 
 |-  ( ph -> ( L /FldExt Q /\ E. n e. NN0 ( L [:] Q ) = ( 2 ^ n ) ) )