Metamath Proof Explorer

Theorem constrextdg2lem

Description: Lemma for constrextdg2 (Contributed by Thierry Arnoux, 19-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 )
constrextdg2lem.1 
|- ( ph -> R e. ( .< Chain ( SubDRing ` CCfld ) ) )
constrextdg2lem.2 
|- ( ph -> ( R ` 0 ) = QQ )
constrextdg2lem.3 
|- ( ph -> ( C ` N ) C_ ( lastS ` R ) )
Assertion constrextdg2lem 
|- ( ph -> E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( C ` suc N ) C_ ( lastS ` v ) ) )

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 constrextdg2lem.1 
 |-  ( ph -> R e. ( .< Chain ( SubDRing ` CCfld ) ) )
7 constrextdg2lem.2 
 |-  ( ph -> ( R ` 0 ) = QQ )
8 constrextdg2lem.3 
 |-  ( ph -> ( C ` N ) C_ ( lastS ` R ) )
9 uneq2 
 |-  ( i = (/) -> ( ( C ` N ) u. i ) = ( ( C ` N ) u. (/) ) )
10 9 sseq1d 
 |-  ( i = (/) -> ( ( ( C ` N ) u. i ) C_ ( lastS ` v ) <-> ( ( C ` N ) u. (/) ) C_ ( lastS ` v ) ) )
11 10 anbi2d 
 |-  ( i = (/) -> ( ( ( v ` 0 ) = QQ /\ ( ( C ` N ) u. i ) C_ ( lastS ` v ) ) <-> ( ( v ` 0 ) = QQ /\ ( ( C ` N ) u. (/) ) C_ ( lastS ` v ) ) ) )
12 11 rexbidv 
 |-  ( i = (/) -> ( E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( ( C ` N ) u. i ) C_ ( lastS ` v ) ) <-> E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( ( C ` N ) u. (/) ) C_ ( lastS ` v ) ) ) )
13 uneq2 
 |-  ( i = g -> ( ( C ` N ) u. i ) = ( ( C ` N ) u. g ) )
14 13 sseq1d 
 |-  ( i = g -> ( ( ( C ` N ) u. i ) C_ ( lastS ` v ) <-> ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) )
15 14 anbi2d 
 |-  ( i = g -> ( ( ( v ` 0 ) = QQ /\ ( ( C ` N ) u. i ) C_ ( lastS ` v ) ) <-> ( ( v ` 0 ) = QQ /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) ) )
16 15 rexbidv 
 |-  ( i = g -> ( E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( ( C ` N ) u. i ) C_ ( lastS ` v ) ) <-> E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) ) )
17 fveq1 
 |-  ( v = u -> ( v ` 0 ) = ( u ` 0 ) )
18 17 eqeq1d 
 |-  ( v = u -> ( ( v ` 0 ) = QQ <-> ( u ` 0 ) = QQ ) )
19 fveq2 
 |-  ( v = u -> ( lastS ` v ) = ( lastS ` u ) )
20 19 sseq2d 
 |-  ( v = u -> ( ( ( C ` N ) u. i ) C_ ( lastS ` v ) <-> ( ( C ` N ) u. i ) C_ ( lastS ` u ) ) )
21 18 20 anbi12d 
 |-  ( v = u -> ( ( ( v ` 0 ) = QQ /\ ( ( C ` N ) u. i ) C_ ( lastS ` v ) ) <-> ( ( u ` 0 ) = QQ /\ ( ( C ` N ) u. i ) C_ ( lastS ` u ) ) ) )
22 21 cbvrexvw 
 |-  ( E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( ( C ` N ) u. i ) C_ ( lastS ` v ) ) <-> E. u e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( u ` 0 ) = QQ /\ ( ( C ` N ) u. i ) C_ ( lastS ` u ) ) )
23 uneq2 
 |-  ( i = ( g u. { y } ) -> ( ( C ` N ) u. i ) = ( ( C ` N ) u. ( g u. { y } ) ) )
24 23 sseq1d 
 |-  ( i = ( g u. { y } ) -> ( ( ( C ` N ) u. i ) C_ ( lastS ` u ) <-> ( ( C ` N ) u. ( g u. { y } ) ) C_ ( lastS ` u ) ) )
25 24 anbi2d 
 |-  ( i = ( g u. { y } ) -> ( ( ( u ` 0 ) = QQ /\ ( ( C ` N ) u. i ) C_ ( lastS ` u ) ) <-> ( ( u ` 0 ) = QQ /\ ( ( C ` N ) u. ( g u. { y } ) ) C_ ( lastS ` u ) ) ) )
26 25 rexbidv 
 |-  ( i = ( g u. { y } ) -> ( E. u e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( u ` 0 ) = QQ /\ ( ( C ` N ) u. i ) C_ ( lastS ` u ) ) <-> E. u e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( u ` 0 ) = QQ /\ ( ( C ` N ) u. ( g u. { y } ) ) C_ ( lastS ` u ) ) ) )
27 22 26 bitrid 
 |-  ( i = ( g u. { y } ) -> ( E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( ( C ` N ) u. i ) C_ ( lastS ` v ) ) <-> E. u e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( u ` 0 ) = QQ /\ ( ( C ` N ) u. ( g u. { y } ) ) C_ ( lastS ` u ) ) ) )
28 uneq2 
 |-  ( i = ( C ` suc N ) -> ( ( C ` N ) u. i ) = ( ( C ` N ) u. ( C ` suc N ) ) )
29 28 sseq1d 
 |-  ( i = ( C ` suc N ) -> ( ( ( C ` N ) u. i ) C_ ( lastS ` v ) <-> ( ( C ` N ) u. ( C ` suc N ) ) C_ ( lastS ` v ) ) )
30 29 anbi2d 
 |-  ( i = ( C ` suc N ) -> ( ( ( v ` 0 ) = QQ /\ ( ( C ` N ) u. i ) C_ ( lastS ` v ) ) <-> ( ( v ` 0 ) = QQ /\ ( ( C ` N ) u. ( C ` suc N ) ) C_ ( lastS ` v ) ) ) )
31 30 rexbidv 
 |-  ( i = ( C ` suc N ) -> ( E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( ( C ` N ) u. i ) C_ ( lastS ` v ) ) <-> E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( ( C ` N ) u. ( C ` suc N ) ) C_ ( lastS ` v ) ) ) )
32 fveq1 
 |-  ( v = R -> ( v ` 0 ) = ( R ` 0 ) )
33 32 eqeq1d 
 |-  ( v = R -> ( ( v ` 0 ) = QQ <-> ( R ` 0 ) = QQ ) )
34 fveq2 
 |-  ( v = R -> ( lastS ` v ) = ( lastS ` R ) )
35 34 sseq2d 
 |-  ( v = R -> ( ( ( C ` N ) u. (/) ) C_ ( lastS ` v ) <-> ( ( C ` N ) u. (/) ) C_ ( lastS ` R ) ) )
36 33 35 anbi12d 
 |-  ( v = R -> ( ( ( v ` 0 ) = QQ /\ ( ( C ` N ) u. (/) ) C_ ( lastS ` v ) ) <-> ( ( R ` 0 ) = QQ /\ ( ( C ` N ) u. (/) ) C_ ( lastS ` R ) ) ) )
37 un0 
 |-  ( ( C ` N ) u. (/) ) = ( C ` N )
38 37 8 eqsstrid 
 |-  ( ph -> ( ( C ` N ) u. (/) ) C_ ( lastS ` R ) )
39 7 38 jca 
 |-  ( ph -> ( ( R ` 0 ) = QQ /\ ( ( C ` N ) u. (/) ) C_ ( lastS ` R ) ) )
40 36 6 39 rspcedvdw 
 |-  ( ph -> E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( ( C ` N ) u. (/) ) C_ ( lastS ` v ) ) )
41 fveq1 
 |-  ( u = v -> ( u ` 0 ) = ( v ` 0 ) )
42 41 eqeq1d 
 |-  ( u = v -> ( ( u ` 0 ) = QQ <-> ( v ` 0 ) = QQ ) )
43 fveq2 
 |-  ( u = v -> ( lastS ` u ) = ( lastS ` v ) )
44 43 sseq2d 
 |-  ( u = v -> ( ( ( C ` N ) u. ( g u. { y } ) ) C_ ( lastS ` u ) <-> ( ( C ` N ) u. ( g u. { y } ) ) C_ ( lastS ` v ) ) )
45 42 44 anbi12d 
 |-  ( u = v -> ( ( ( u ` 0 ) = QQ /\ ( ( C ` N ) u. ( g u. { y } ) ) C_ ( lastS ` u ) ) <-> ( ( v ` 0 ) = QQ /\ ( ( C ` N ) u. ( g u. { y } ) ) C_ ( lastS ` v ) ) ) )
46 simpllr 
 |-  ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) -> v e. ( .< Chain ( SubDRing ` CCfld ) ) )
47 46 adantr 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ y e. ( lastS ` v ) ) -> v e. ( .< Chain ( SubDRing ` CCfld ) ) )
48 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ y e. ( lastS ` v ) ) -> ( v ` 0 ) = QQ )
49 simpr 
 |-  ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) -> ( ( C ` N ) u. g ) C_ ( lastS ` v ) )
50 49 unssad 
 |-  ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) -> ( C ` N ) C_ ( lastS ` v ) )
51 50 adantr 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ y e. ( lastS ` v ) ) -> ( C ` N ) C_ ( lastS ` v ) )
52 simplr 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ y e. ( lastS ` v ) ) -> ( ( C ` N ) u. g ) C_ ( lastS ` v ) )
53 52 unssbd 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ y e. ( lastS ` v ) ) -> g C_ ( lastS ` v ) )
54 simpr 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ y e. ( lastS ` v ) ) -> y e. ( lastS ` v ) )
55 54 snssd 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ y e. ( lastS ` v ) ) -> { y } C_ ( lastS ` v ) )
56 53 55 unssd 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ y e. ( lastS ` v ) ) -> ( g u. { y } ) C_ ( lastS ` v ) )
57 51 56 unssd 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ y e. ( lastS ` v ) ) -> ( ( C ` N ) u. ( g u. { y } ) ) C_ ( lastS ` v ) )
58 48 57 jca 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ y e. ( lastS ` v ) ) -> ( ( v ` 0 ) = QQ /\ ( ( C ` N ) u. ( g u. { y } ) ) C_ ( lastS ` v ) ) )
59 45 47 58 rspcedvdw 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ y e. ( lastS ` v ) ) -> E. u e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( u ` 0 ) = QQ /\ ( ( C ` N ) u. ( g u. { y } ) ) C_ ( lastS ` u ) ) )
60 fveq1 
 |-  ( u = ( v ++ <" ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) "> ) -> ( u ` 0 ) = ( ( v ++ <" ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) "> ) ` 0 ) )
61 60 eqeq1d 
 |-  ( u = ( v ++ <" ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) "> ) -> ( ( u ` 0 ) = QQ <-> ( ( v ++ <" ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) "> ) ` 0 ) = QQ ) )
62 fveq2 
 |-  ( u = ( v ++ <" ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) "> ) -> ( lastS ` u ) = ( lastS ` ( v ++ <" ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) "> ) ) )
63 62 sseq2d 
 |-  ( u = ( v ++ <" ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) "> ) -> ( ( ( C ` N ) u. ( g u. { y } ) ) C_ ( lastS ` u ) <-> ( ( C ` N ) u. ( g u. { y } ) ) C_ ( lastS ` ( v ++ <" ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) "> ) ) ) )
64 61 63 anbi12d 
 |-  ( u = ( v ++ <" ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) "> ) -> ( ( ( u ` 0 ) = QQ /\ ( ( C ` N ) u. ( g u. { y } ) ) C_ ( lastS ` u ) ) <-> ( ( ( v ++ <" ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) "> ) ` 0 ) = QQ /\ ( ( C ` N ) u. ( g u. { y } ) ) C_ ( lastS ` ( v ++ <" ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) "> ) ) ) ) )
65 cnfldbas 
 |-  CC = ( Base ` CCfld )
66 cndrng 
 |-  CCfld e. DivRing
67 66 a1i 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> CCfld e. DivRing )
68 46 chnwrd 
 |-  ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) -> v e. Word ( SubDRing ` CCfld ) )
69 simpr 
 |-  ( ( ( ph /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ v = (/) ) -> v = (/) )
70 69 fveq2d 
 |-  ( ( ( ph /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ v = (/) ) -> ( lastS ` v ) = ( lastS ` (/) ) )
71 lsw0g 
 |-  ( lastS ` (/) ) = (/)
72 70 71 eqtrdi 
 |-  ( ( ( ph /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ v = (/) ) -> ( lastS ` v ) = (/) )
73 simplr 
 |-  ( ( ( ph /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ v = (/) ) -> ( ( C ` N ) u. g ) C_ ( lastS ` v ) )
74 ssun1 
 |-  ( C ` N ) C_ ( ( C ` N ) u. g )
75 nnon 
 |-  ( N e. _om -> N e. On )
76 5 75 syl 
 |-  ( ph -> N e. On )
77 1 76 constr01 
 |-  ( ph -> { 0 , 1 } C_ ( C ` N ) )
78 c0ex 
 |-  0 e. _V
79 78 prnz 
 |-  { 0 , 1 } =/= (/)
80 ssn0 
 |-  ( ( { 0 , 1 } C_ ( C ` N ) /\ { 0 , 1 } =/= (/) ) -> ( C ` N ) =/= (/) )
81 77 79 80 sylancl 
 |-  ( ph -> ( C ` N ) =/= (/) )
82 ssn0 
 |-  ( ( ( C ` N ) C_ ( ( C ` N ) u. g ) /\ ( C ` N ) =/= (/) ) -> ( ( C ` N ) u. g ) =/= (/) )
83 74 81 82 sylancr 
 |-  ( ph -> ( ( C ` N ) u. g ) =/= (/) )
84 83 ad2antrr 
 |-  ( ( ( ph /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ v = (/) ) -> ( ( C ` N ) u. g ) =/= (/) )
85 ssn0 
 |-  ( ( ( ( C ` N ) u. g ) C_ ( lastS ` v ) /\ ( ( C ` N ) u. g ) =/= (/) ) -> ( lastS ` v ) =/= (/) )
86 73 84 85 syl2anc 
 |-  ( ( ( ph /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ v = (/) ) -> ( lastS ` v ) =/= (/) )
87 86 neneqd 
 |-  ( ( ( ph /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ v = (/) ) -> -. ( lastS ` v ) = (/) )
88 72 87 pm2.65da 
 |-  ( ( ph /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) -> -. v = (/) )
89 88 neqned 
 |-  ( ( ph /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) -> v =/= (/) )
90 89 ad4antr 
 |-  ( ( ( ( ( ( ph /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ g C_ ( C ` suc N ) ) -> v =/= (/) )
91 90 an62ds 
 |-  ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) -> v =/= (/) )
92 lswcl 
 |-  ( ( v e. Word ( SubDRing ` CCfld ) /\ v =/= (/) ) -> ( lastS ` v ) e. ( SubDRing ` CCfld ) )
93 68 91 92 syl2anc 
 |-  ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) -> ( lastS ` v ) e. ( SubDRing ` CCfld ) )
94 93 adantr 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> ( lastS ` v ) e. ( SubDRing ` CCfld ) )
95 65 sdrgss 
 |-  ( ( lastS ` v ) e. ( SubDRing ` CCfld ) -> ( lastS ` v ) C_ CC )
96 94 95 syl 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> ( lastS ` v ) C_ CC )
97 onsuc 
 |-  ( N e. On -> suc N e. On )
98 76 97 syl 
 |-  ( ph -> suc N e. On )
99 1 98 constrsscn 
 |-  ( ph -> ( C ` suc N ) C_ CC )
100 99 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> ( C ` suc N ) C_ CC )
101 simp-4r 
 |-  ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) -> y e. ( ( C ` suc N ) \ g ) )
102 101 eldifad 
 |-  ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) -> y e. ( C ` suc N ) )
103 102 adantr 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> y e. ( C ` suc N ) )
104 100 103 sseldd 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> y e. CC )
105 104 snssd 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> { y } C_ CC )
106 96 105 unssd 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> ( ( lastS ` v ) u. { y } ) C_ CC )
107 65 67 106 fldgensdrg 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) e. ( SubDRing ` CCfld ) )
108 46 adantr 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> v e. ( .< Chain ( SubDRing ` CCfld ) ) )
109 94 elexd 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> ( lastS ` v ) e. _V )
110 107 elexd 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) e. _V )
111 eqid 
 |-  ( CCfld |`s ( lastS ` v ) ) = ( CCfld |`s ( lastS ` v ) )
112 eqid 
 |-  ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) = ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) )
113 cnfldfld 
 |-  CCfld e. Field
114 113 a1i 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> CCfld e. Field )
115 65 111 112 114 94 105 fldgenfldext 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) /FldExt ( CCfld |`s ( lastS ` v ) ) )
116 simpr 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 )
117 2 3 breq12i 
 |-  ( E /FldExt F <-> ( CCfld |`s e ) /FldExt ( CCfld |`s f ) )
118 oveq2 
 |-  ( e = ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) -> ( CCfld |`s e ) = ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) )
119 118 adantl 
 |-  ( ( f = ( lastS ` v ) /\ e = ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) -> ( CCfld |`s e ) = ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) )
120 oveq2 
 |-  ( f = ( lastS ` v ) -> ( CCfld |`s f ) = ( CCfld |`s ( lastS ` v ) ) )
121 120 adantr 
 |-  ( ( f = ( lastS ` v ) /\ e = ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) -> ( CCfld |`s f ) = ( CCfld |`s ( lastS ` v ) ) )
122 119 121 breq12d 
 |-  ( ( f = ( lastS ` v ) /\ e = ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) -> ( ( CCfld |`s e ) /FldExt ( CCfld |`s f ) <-> ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) /FldExt ( CCfld |`s ( lastS ` v ) ) ) )
123 117 122 bitrid 
 |-  ( ( f = ( lastS ` v ) /\ e = ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) -> ( E /FldExt F <-> ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) /FldExt ( CCfld |`s ( lastS ` v ) ) ) )
124 2 3 oveq12i 
 |-  ( E [:] F ) = ( ( CCfld |`s e ) [:] ( CCfld |`s f ) )
125 119 121 oveq12d 
 |-  ( ( f = ( lastS ` v ) /\ e = ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) -> ( ( CCfld |`s e ) [:] ( CCfld |`s f ) ) = ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) )
126 124 125 eqtrid 
 |-  ( ( f = ( lastS ` v ) /\ e = ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) -> ( E [:] F ) = ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) )
127 126 eqeq1d 
 |-  ( ( f = ( lastS ` v ) /\ e = ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) -> ( ( E [:] F ) = 2 <-> ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) )
128 123 127 anbi12d 
 |-  ( ( f = ( lastS ` v ) /\ e = ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) -> ( ( E /FldExt F /\ ( E [:] F ) = 2 ) <-> ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) /FldExt ( CCfld |`s ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) ) )
129 128 4 brabga 
 |-  ( ( ( lastS ` v ) e. _V /\ ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) e. _V ) -> ( ( lastS ` v ) .< ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) <-> ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) /FldExt ( CCfld |`s ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) ) )
130 129 biimpar 
 |-  ( ( ( ( lastS ` v ) e. _V /\ ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) e. _V ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) /FldExt ( CCfld |`s ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) ) -> ( lastS ` v ) .< ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) )
131 109 110 115 116 130 syl22anc 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> ( lastS ` v ) .< ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) )
132 131 olcd 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> ( v = (/) \/ ( lastS ` v ) .< ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) )
133 107 108 132 chnccats1 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> ( v ++ <" ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) "> ) e. ( .< Chain ( SubDRing ` CCfld ) ) )
134 68 adantr 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> v e. Word ( SubDRing ` CCfld ) )
135 107 s1cld 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> <" ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) "> e. Word ( SubDRing ` CCfld ) )
136 hashgt0 
 |-  ( ( v e. ( .< Chain ( SubDRing ` CCfld ) ) /\ v =/= (/) ) -> 0 < ( # ` v ) )
137 46 91 136 syl2anc 
 |-  ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) -> 0 < ( # ` v ) )
138 137 adantr 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> 0 < ( # ` v ) )
139 ccatfv0 
 |-  ( ( v e. Word ( SubDRing ` CCfld ) /\ <" ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) "> e. Word ( SubDRing ` CCfld ) /\ 0 < ( # ` v ) ) -> ( ( v ++ <" ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) "> ) ` 0 ) = ( v ` 0 ) )
140 134 135 138 139 syl3anc 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> ( ( v ++ <" ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) "> ) ` 0 ) = ( v ` 0 ) )
141 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> ( v ` 0 ) = QQ )
142 140 141 eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> ( ( v ++ <" ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) "> ) ` 0 ) = QQ )
143 50 adantr 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> ( C ` N ) C_ ( lastS ` v ) )
144 ssun3 
 |-  ( ( C ` N ) C_ ( lastS ` v ) -> ( C ` N ) C_ ( ( lastS ` v ) u. { y } ) )
145 143 144 syl 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> ( C ` N ) C_ ( ( lastS ` v ) u. { y } ) )
146 simplr 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> ( ( C ` N ) u. g ) C_ ( lastS ` v ) )
147 146 unssbd 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> g C_ ( lastS ` v ) )
148 ssun3 
 |-  ( g C_ ( lastS ` v ) -> g C_ ( ( lastS ` v ) u. { y } ) )
149 147 148 syl 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> g C_ ( ( lastS ` v ) u. { y } ) )
150 ssun2 
 |-  { y } C_ ( ( lastS ` v ) u. { y } )
151 150 a1i 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> { y } C_ ( ( lastS ` v ) u. { y } ) )
152 149 151 unssd 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> ( g u. { y } ) C_ ( ( lastS ` v ) u. { y } ) )
153 145 152 unssd 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> ( ( C ` N ) u. ( g u. { y } ) ) C_ ( ( lastS ` v ) u. { y } ) )
154 65 67 106 fldgenssid 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> ( ( lastS ` v ) u. { y } ) C_ ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) )
155 153 154 sstrd 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> ( ( C ` N ) u. ( g u. { y } ) ) C_ ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) )
156 lswccats1 
 |-  ( ( v e. Word ( SubDRing ` CCfld ) /\ ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) e. ( SubDRing ` CCfld ) ) -> ( lastS ` ( v ++ <" ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) "> ) ) = ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) )
157 134 107 156 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> ( lastS ` ( v ++ <" ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) "> ) ) = ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) )
158 155 157 sseqtrrd 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> ( ( C ` N ) u. ( g u. { y } ) ) C_ ( lastS ` ( v ++ <" ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) "> ) ) )
159 142 158 jca 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> ( ( ( v ++ <" ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) "> ) ` 0 ) = QQ /\ ( ( C ` N ) u. ( g u. { y } ) ) C_ ( lastS ` ( v ++ <" ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) "> ) ) ) )
160 64 133 159 rspcedvdw 
 |-  ( ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) /\ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) -> E. u e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( u ` 0 ) = QQ /\ ( ( C ` N ) u. ( g u. { y } ) ) C_ ( lastS ` u ) ) )
161 76 ad5antr 
 |-  ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) -> N e. On )
162 1 111 112 93 161 50 102 constrelextdg2 
 |-  ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) -> ( y e. ( lastS ` v ) \/ ( ( CCfld |`s ( CCfld fldGen ( ( lastS ` v ) u. { y } ) ) ) [:] ( CCfld |`s ( lastS ` v ) ) ) = 2 ) )
163 59 160 162 mpjaodan 
 |-  ( ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( v ` 0 ) = QQ ) /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) -> E. u e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( u ` 0 ) = QQ /\ ( ( C ` N ) u. ( g u. { y } ) ) C_ ( lastS ` u ) ) )
164 163 anasss 
 |-  ( ( ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( v ` 0 ) = QQ /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) ) -> E. u e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( u ` 0 ) = QQ /\ ( ( C ` N ) u. ( g u. { y } ) ) C_ ( lastS ` u ) ) )
165 164 rexlimdva2 
 |-  ( ( ( ph /\ g C_ ( C ` suc N ) ) /\ y e. ( ( C ` suc N ) \ g ) ) -> ( E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) -> E. u e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( u ` 0 ) = QQ /\ ( ( C ` N ) u. ( g u. { y } ) ) C_ ( lastS ` u ) ) ) )
166 165 anasss 
 |-  ( ( ph /\ ( g C_ ( C ` suc N ) /\ y e. ( ( C ` suc N ) \ g ) ) ) -> ( E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( ( C ` N ) u. g ) C_ ( lastS ` v ) ) -> E. u e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( u ` 0 ) = QQ /\ ( ( C ` N ) u. ( g u. { y } ) ) C_ ( lastS ` u ) ) ) )
167 peano2 
 |-  ( N e. _om -> suc N e. _om )
168 5 167 syl 
 |-  ( ph -> suc N e. _om )
169 1 168 constrfin 
 |-  ( ph -> ( C ` suc N ) e. Fin )
170 12 16 27 31 40 166 169 findcard2d 
 |-  ( ph -> E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( ( C ` N ) u. ( C ` suc N ) ) C_ ( lastS ` v ) ) )
171 simpr 
 |-  ( ( ( ph /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( C ` N ) u. ( C ` suc N ) ) C_ ( lastS ` v ) ) -> ( ( C ` N ) u. ( C ` suc N ) ) C_ ( lastS ` v ) )
172 171 unssbd 
 |-  ( ( ( ph /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( C ` N ) u. ( C ` suc N ) ) C_ ( lastS ` v ) ) -> ( C ` suc N ) C_ ( lastS ` v ) )
173 172 ex 
 |-  ( ( ph /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) -> ( ( ( C ` N ) u. ( C ` suc N ) ) C_ ( lastS ` v ) -> ( C ` suc N ) C_ ( lastS ` v ) ) )
174 173 anim2d 
 |-  ( ( ph /\ v e. ( .< Chain ( SubDRing ` CCfld ) ) ) -> ( ( ( v ` 0 ) = QQ /\ ( ( C ` N ) u. ( C ` suc N ) ) C_ ( lastS ` v ) ) -> ( ( v ` 0 ) = QQ /\ ( C ` suc N ) C_ ( lastS ` v ) ) ) )
175 174 reximdva 
 |-  ( ph -> ( E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( ( C ` N ) u. ( C ` suc N ) ) C_ ( lastS ` v ) ) -> E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( C ` suc N ) C_ ( lastS ` v ) ) ) )
176 170 175 mpd 
 |-  ( ph -> E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( C ` suc N ) C_ ( lastS ` v ) ) )