Metamath Proof Explorer

Theorem fldext2chn

Description: In a non-empty tower T of quadratic field extensions, the degree of the extension of the first member by the last is a power of two. (Contributed by Thierry Arnoux, 19-Jun-2025)

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

Proof

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