Metamath Proof Explorer

Theorem cphsubrglem

Description: Lemma for cphsubrg . (Contributed by Mario Carneiro, 9-Oct-2015)

Ref Expression
Hypotheses cphsubrglem.k 
|- K = ( Base ` F )
cphsubrglem.1 
|- ( ph -> F = ( CCfld |`s A ) )
cphsubrglem.2 
|- ( ph -> F e. DivRing )
Assertion cphsubrglem 
|- ( ph -> ( F = ( CCfld |`s K ) /\ K = ( A i^i CC ) /\ K e. ( SubRing ` CCfld ) ) )

Proof

Step Hyp Ref Expression
1 cphsubrglem.k 
 |-  K = ( Base ` F )
2 cphsubrglem.1 
 |-  ( ph -> F = ( CCfld |`s A ) )
3 cphsubrglem.2 
 |-  ( ph -> F e. DivRing )
4 2 fveq2d 
 |-  ( ph -> ( Base ` F ) = ( Base ` ( CCfld |`s A ) ) )
5 drngring 
 |-  ( F e. DivRing -> F e. Ring )
6 3 5 syl 
 |-  ( ph -> F e. Ring )
7 2 6 eqeltrrd 
 |-  ( ph -> ( CCfld |`s A ) e. Ring )
8 eqid 
 |-  ( Base ` ( CCfld |`s A ) ) = ( Base ` ( CCfld |`s A ) )
9 eqid 
 |-  ( 0g ` ( CCfld |`s A ) ) = ( 0g ` ( CCfld |`s A ) )
10 8 9 ring0cl 
 |-  ( ( CCfld |`s A ) e. Ring -> ( 0g ` ( CCfld |`s A ) ) e. ( Base ` ( CCfld |`s A ) ) )
11 reldmress 
 |-  Rel dom |`s
12 eqid 
 |-  ( CCfld |`s A ) = ( CCfld |`s A )
13 11 12 8 elbasov 
 |-  ( ( 0g ` ( CCfld |`s A ) ) e. ( Base ` ( CCfld |`s A ) ) -> ( CCfld e. _V /\ A e. _V ) )
14 7 10 13 3syl 
 |-  ( ph -> ( CCfld e. _V /\ A e. _V ) )
15 14 simprd 
 |-  ( ph -> A e. _V )
16 cnfldbas 
 |-  CC = ( Base ` CCfld )
17 12 16 ressbas 
 |-  ( A e. _V -> ( A i^i CC ) = ( Base ` ( CCfld |`s A ) ) )
18 15 17 syl 
 |-  ( ph -> ( A i^i CC ) = ( Base ` ( CCfld |`s A ) ) )
19 4 18 eqtr4d 
 |-  ( ph -> ( Base ` F ) = ( A i^i CC ) )
20 1 19 syl5eq 
 |-  ( ph -> K = ( A i^i CC ) )
21 20 oveq2d 
 |-  ( ph -> ( CCfld |`s K ) = ( CCfld |`s ( A i^i CC ) ) )
22 16 ressinbas 
 |-  ( A e. _V -> ( CCfld |`s A ) = ( CCfld |`s ( A i^i CC ) ) )
23 15 22 syl 
 |-  ( ph -> ( CCfld |`s A ) = ( CCfld |`s ( A i^i CC ) ) )
24 21 23 eqtr4d 
 |-  ( ph -> ( CCfld |`s K ) = ( CCfld |`s A ) )
25 2 24 eqtr4d 
 |-  ( ph -> F = ( CCfld |`s K ) )
26 25 6 eqeltrrd 
 |-  ( ph -> ( CCfld |`s K ) e. Ring )
27 cnring 
 |-  CCfld e. Ring
28 26 27 jctil 
 |-  ( ph -> ( CCfld e. Ring /\ ( CCfld |`s K ) e. Ring ) )
29 12 16 ressbasss 
 |-  ( Base ` ( CCfld |`s A ) ) C_ CC
30 4 29 eqsstrdi 
 |-  ( ph -> ( Base ` F ) C_ CC )
31 1 30 eqsstrid 
 |-  ( ph -> K C_ CC )
32 eqid 
 |-  ( 0g ` F ) = ( 0g ` F )
33 eqid 
 |-  ( 1r ` F ) = ( 1r ` F )
34 32 33 drngunz 
 |-  ( F e. DivRing -> ( 1r ` F ) =/= ( 0g ` F ) )
35 3 34 syl 
 |-  ( ph -> ( 1r ` F ) =/= ( 0g ` F ) )
36 25 fveq2d 
 |-  ( ph -> ( 0g ` F ) = ( 0g ` ( CCfld |`s K ) ) )
37 ringgrp 
 |-  ( CCfld e. Ring -> CCfld e. Grp )
38 27 37 mp1i 
 |-  ( ph -> CCfld e. Grp )
39 ringgrp 
 |-  ( ( CCfld |`s K ) e. Ring -> ( CCfld |`s K ) e. Grp )
40 26 39 syl 
 |-  ( ph -> ( CCfld |`s K ) e. Grp )
41 16 issubg 
 |-  ( K e. ( SubGrp ` CCfld ) <-> ( CCfld e. Grp /\ K C_ CC /\ ( CCfld |`s K ) e. Grp ) )
42 38 31 40 41 syl3anbrc 
 |-  ( ph -> K e. ( SubGrp ` CCfld ) )
43 eqid 
 |-  ( CCfld |`s K ) = ( CCfld |`s K )
44 cnfld0 
 |-  0 = ( 0g ` CCfld )
45 43 44 subg0 
 |-  ( K e. ( SubGrp ` CCfld ) -> 0 = ( 0g ` ( CCfld |`s K ) ) )
46 42 45 syl 
 |-  ( ph -> 0 = ( 0g ` ( CCfld |`s K ) ) )
47 36 46 eqtr4d 
 |-  ( ph -> ( 0g ` F ) = 0 )
48 35 47 neeqtrd 
 |-  ( ph -> ( 1r ` F ) =/= 0 )
49 48 neneqd 
 |-  ( ph -> -. ( 1r ` F ) = 0 )
50 1 33 ringidcl 
 |-  ( F e. Ring -> ( 1r ` F ) e. K )
51 6 50 syl 
 |-  ( ph -> ( 1r ` F ) e. K )
52 31 51 sseldd 
 |-  ( ph -> ( 1r ` F ) e. CC )
53 52 sqvald 
 |-  ( ph -> ( ( 1r ` F ) ^ 2 ) = ( ( 1r ` F ) x. ( 1r ` F ) ) )
54 25 fveq2d 
 |-  ( ph -> ( 1r ` F ) = ( 1r ` ( CCfld |`s K ) ) )
55 54 oveq1d 
 |-  ( ph -> ( ( 1r ` F ) x. ( 1r ` F ) ) = ( ( 1r ` ( CCfld |`s K ) ) x. ( 1r ` F ) ) )
56 25 fveq2d 
 |-  ( ph -> ( Base ` F ) = ( Base ` ( CCfld |`s K ) ) )
57 1 56 syl5eq 
 |-  ( ph -> K = ( Base ` ( CCfld |`s K ) ) )
58 51 57 eleqtrd 
 |-  ( ph -> ( 1r ` F ) e. ( Base ` ( CCfld |`s K ) ) )
59 eqid 
 |-  ( Base ` ( CCfld |`s K ) ) = ( Base ` ( CCfld |`s K ) )
60 1 fvexi 
 |-  K e. _V
61 cnfldmul 
 |-  x. = ( .r ` CCfld )
62 43 61 ressmulr 
 |-  ( K e. _V -> x. = ( .r ` ( CCfld |`s K ) ) )
63 60 62 ax-mp 
 |-  x. = ( .r ` ( CCfld |`s K ) )
64 eqid 
 |-  ( 1r ` ( CCfld |`s K ) ) = ( 1r ` ( CCfld |`s K ) )
65 59 63 64 ringlidm 
 |-  ( ( ( CCfld |`s K ) e. Ring /\ ( 1r ` F ) e. ( Base ` ( CCfld |`s K ) ) ) -> ( ( 1r ` ( CCfld |`s K ) ) x. ( 1r ` F ) ) = ( 1r ` F ) )
66 26 58 65 syl2anc 
 |-  ( ph -> ( ( 1r ` ( CCfld |`s K ) ) x. ( 1r ` F ) ) = ( 1r ` F ) )
67 53 55 66 3eqtrd 
 |-  ( ph -> ( ( 1r ` F ) ^ 2 ) = ( 1r ` F ) )
68 sq01 
 |-  ( ( 1r ` F ) e. CC -> ( ( ( 1r ` F ) ^ 2 ) = ( 1r ` F ) <-> ( ( 1r ` F ) = 0 \/ ( 1r ` F ) = 1 ) ) )
69 52 68 syl 
 |-  ( ph -> ( ( ( 1r ` F ) ^ 2 ) = ( 1r ` F ) <-> ( ( 1r ` F ) = 0 \/ ( 1r ` F ) = 1 ) ) )
70 67 69 mpbid 
 |-  ( ph -> ( ( 1r ` F ) = 0 \/ ( 1r ` F ) = 1 ) )
71 70 ord 
 |-  ( ph -> ( -. ( 1r ` F ) = 0 -> ( 1r ` F ) = 1 ) )
72 49 71 mpd 
 |-  ( ph -> ( 1r ` F ) = 1 )
73 72 51 eqeltrrd 
 |-  ( ph -> 1 e. K )
74 31 73 jca 
 |-  ( ph -> ( K C_ CC /\ 1 e. K ) )
75 cnfld1 
 |-  1 = ( 1r ` CCfld )
76 16 75 issubrg 
 |-  ( K e. ( SubRing ` CCfld ) <-> ( ( CCfld e. Ring /\ ( CCfld |`s K ) e. Ring ) /\ ( K C_ CC /\ 1 e. K ) ) )
77 28 74 76 sylanbrc 
 |-  ( ph -> K e. ( SubRing ` CCfld ) )
78 25 20 77 3jca 
 |-  ( ph -> ( F = ( CCfld |`s K ) /\ K = ( A i^i CC ) /\ K e. ( SubRing ` CCfld ) ) )