# Metamath Proof Explorer

## Theorem cphsubrglem

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

Ref Expression
Hypotheses cphsubrglem.k ${⊢}{K}={\mathrm{Base}}_{{F}}$
cphsubrglem.1 ${⊢}{\phi }\to {F}={ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}$
cphsubrglem.2 ${⊢}{\phi }\to {F}\in \mathrm{DivRing}$
Assertion cphsubrglem ${⊢}{\phi }\to \left({F}={ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}\wedge {K}={A}\cap ℂ\wedge {K}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\right)$

### Proof

Step Hyp Ref Expression
1 cphsubrglem.k ${⊢}{K}={\mathrm{Base}}_{{F}}$
2 cphsubrglem.1 ${⊢}{\phi }\to {F}={ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}$
3 cphsubrglem.2 ${⊢}{\phi }\to {F}\in \mathrm{DivRing}$
4 2 fveq2d ${⊢}{\phi }\to {\mathrm{Base}}_{{F}}={\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}$
5 drngring ${⊢}{F}\in \mathrm{DivRing}\to {F}\in \mathrm{Ring}$
6 3 5 syl ${⊢}{\phi }\to {F}\in \mathrm{Ring}$
7 2 6 eqeltrrd ${⊢}{\phi }\to {ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\in \mathrm{Ring}$
8 eqid ${⊢}{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}={\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}$
9 eqid ${⊢}{0}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}={0}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}$
10 8 9 ring0cl ${⊢}{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\in \mathrm{Ring}\to {0}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\in {\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}$
11 reldmress ${⊢}\mathrm{Rel}\mathrm{dom}{↾}_{𝑠}$
12 eqid ${⊢}{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}={ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}$
13 11 12 8 elbasov ${⊢}{0}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\in {\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\to \left({ℂ}_{\mathrm{fld}}\in \mathrm{V}\wedge {A}\in \mathrm{V}\right)$
14 7 10 13 3syl ${⊢}{\phi }\to \left({ℂ}_{\mathrm{fld}}\in \mathrm{V}\wedge {A}\in \mathrm{V}\right)$
15 14 simprd ${⊢}{\phi }\to {A}\in \mathrm{V}$
16 cnfldbas ${⊢}ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$
17 12 16 ressbas ${⊢}{A}\in \mathrm{V}\to {A}\cap ℂ={\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}$
18 15 17 syl ${⊢}{\phi }\to {A}\cap ℂ={\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}$
19 4 18 eqtr4d ${⊢}{\phi }\to {\mathrm{Base}}_{{F}}={A}\cap ℂ$
20 1 19 syl5eq ${⊢}{\phi }\to {K}={A}\cap ℂ$
21 20 oveq2d ${⊢}{\phi }\to {ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}={ℂ}_{\mathrm{fld}}{↾}_{𝑠}\left({A}\cap ℂ\right)$
22 16 ressinbas ${⊢}{A}\in \mathrm{V}\to {ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}={ℂ}_{\mathrm{fld}}{↾}_{𝑠}\left({A}\cap ℂ\right)$
23 15 22 syl ${⊢}{\phi }\to {ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}={ℂ}_{\mathrm{fld}}{↾}_{𝑠}\left({A}\cap ℂ\right)$
24 21 23 eqtr4d ${⊢}{\phi }\to {ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}={ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}$
25 2 24 eqtr4d ${⊢}{\phi }\to {F}={ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}$
26 25 6 eqeltrrd ${⊢}{\phi }\to {ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}\in \mathrm{Ring}$
27 cnring ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$
28 26 27 jctil ${⊢}{\phi }\to \left({ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\wedge {ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}\in \mathrm{Ring}\right)$
29 12 16 ressbasss ${⊢}{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{A}\right)}\subseteq ℂ$
30 4 29 eqsstrdi ${⊢}{\phi }\to {\mathrm{Base}}_{{F}}\subseteq ℂ$
31 1 30 eqsstrid ${⊢}{\phi }\to {K}\subseteq ℂ$
32 eqid ${⊢}{0}_{{F}}={0}_{{F}}$
33 eqid ${⊢}{1}_{{F}}={1}_{{F}}$
34 32 33 drngunz ${⊢}{F}\in \mathrm{DivRing}\to {1}_{{F}}\ne {0}_{{F}}$
35 3 34 syl ${⊢}{\phi }\to {1}_{{F}}\ne {0}_{{F}}$
36 25 fveq2d ${⊢}{\phi }\to {0}_{{F}}={0}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}\right)}$
37 ringgrp ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{Grp}$
38 27 37 mp1i ${⊢}{\phi }\to {ℂ}_{\mathrm{fld}}\in \mathrm{Grp}$
39 ringgrp ${⊢}{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}\in \mathrm{Grp}$
40 26 39 syl ${⊢}{\phi }\to {ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}\in \mathrm{Grp}$
41 16 issubg ${⊢}{K}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)↔\left({ℂ}_{\mathrm{fld}}\in \mathrm{Grp}\wedge {K}\subseteq ℂ\wedge {ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}\in \mathrm{Grp}\right)$
42 38 31 40 41 syl3anbrc ${⊢}{\phi }\to {K}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$
43 eqid ${⊢}{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}={ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}$
44 cnfld0 ${⊢}0={0}_{{ℂ}_{\mathrm{fld}}}$
45 43 44 subg0 ${⊢}{K}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\to 0={0}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}\right)}$
46 42 45 syl ${⊢}{\phi }\to 0={0}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}\right)}$
47 36 46 eqtr4d ${⊢}{\phi }\to {0}_{{F}}=0$
48 35 47 neeqtrd ${⊢}{\phi }\to {1}_{{F}}\ne 0$
49 48 neneqd ${⊢}{\phi }\to ¬{1}_{{F}}=0$
50 1 33 ringidcl ${⊢}{F}\in \mathrm{Ring}\to {1}_{{F}}\in {K}$
51 6 50 syl ${⊢}{\phi }\to {1}_{{F}}\in {K}$
52 31 51 sseldd ${⊢}{\phi }\to {1}_{{F}}\in ℂ$
53 52 sqvald ${⊢}{\phi }\to {{1}_{{F}}}^{2}={1}_{{F}}{1}_{{F}}$
54 25 fveq2d ${⊢}{\phi }\to {1}_{{F}}={1}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}\right)}$
55 54 oveq1d ${⊢}{\phi }\to {1}_{{F}}{1}_{{F}}={1}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}\right)}{1}_{{F}}$
56 25 fveq2d ${⊢}{\phi }\to {\mathrm{Base}}_{{F}}={\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}\right)}$
57 1 56 syl5eq ${⊢}{\phi }\to {K}={\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}\right)}$
58 51 57 eleqtrd ${⊢}{\phi }\to {1}_{{F}}\in {\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}\right)}$
59 eqid ${⊢}{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}\right)}={\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}\right)}$
60 1 fvexi ${⊢}{K}\in \mathrm{V}$
61 cnfldmul ${⊢}×={\cdot }_{{ℂ}_{\mathrm{fld}}}$
62 43 61 ressmulr ${⊢}{K}\in \mathrm{V}\to ×={\cdot }_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}\right)}$
63 60 62 ax-mp ${⊢}×={\cdot }_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}\right)}$
64 eqid ${⊢}{1}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}\right)}={1}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}\right)}$
65 59 63 64 ringlidm ${⊢}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}\in \mathrm{Ring}\wedge {1}_{{F}}\in {\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}\right)}\right)\to {1}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}\right)}{1}_{{F}}={1}_{{F}}$
66 26 58 65 syl2anc ${⊢}{\phi }\to {1}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}\right)}{1}_{{F}}={1}_{{F}}$
67 53 55 66 3eqtrd ${⊢}{\phi }\to {{1}_{{F}}}^{2}={1}_{{F}}$
68 sq01 ${⊢}{1}_{{F}}\in ℂ\to \left({{1}_{{F}}}^{2}={1}_{{F}}↔\left({1}_{{F}}=0\vee {1}_{{F}}=1\right)\right)$
69 52 68 syl ${⊢}{\phi }\to \left({{1}_{{F}}}^{2}={1}_{{F}}↔\left({1}_{{F}}=0\vee {1}_{{F}}=1\right)\right)$
70 67 69 mpbid ${⊢}{\phi }\to \left({1}_{{F}}=0\vee {1}_{{F}}=1\right)$
71 70 ord ${⊢}{\phi }\to \left(¬{1}_{{F}}=0\to {1}_{{F}}=1\right)$
72 49 71 mpd ${⊢}{\phi }\to {1}_{{F}}=1$
73 72 51 eqeltrrd ${⊢}{\phi }\to 1\in {K}$
74 31 73 jca ${⊢}{\phi }\to \left({K}\subseteq ℂ\wedge 1\in {K}\right)$
75 cnfld1 ${⊢}1={1}_{{ℂ}_{\mathrm{fld}}}$
76 16 75 issubrg ${⊢}{K}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)↔\left(\left({ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\wedge {ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}\in \mathrm{Ring}\right)\wedge \left({K}\subseteq ℂ\wedge 1\in {K}\right)\right)$
77 28 74 76 sylanbrc ${⊢}{\phi }\to {K}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$
78 25 20 77 3jca ${⊢}{\phi }\to \left({F}={ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}\wedge {K}={A}\cap ℂ\wedge {K}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\right)$