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}}{\upharpoonright }_{𝑠}A$$
	cphsubrglem.2	$$⊢\phi \to F\in \mathrm{DivRing}$$
Assertion	cphsubrglem	$$⊢\phi \to \left(F={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}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}}{\upharpoonright }_{𝑠}A$$
3		cphsubrglem.2	$$⊢\phi \to F\in \mathrm{DivRing}$$
4	2	fveq2d	$$⊢\phi \to {\mathrm{Base}}_F={\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}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}}{\upharpoonright }_{𝑠}A\in \mathrm{Ring}$$
8		eqid	$$⊢{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}A\right)}={\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}A\right)}$$
9		eqid	$$⊢0_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}A\right)}=0_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}A\right)}$$
10	8 9	ring0cl	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}A\in \mathrm{Ring}\to 0_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}A\right)}\in {\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}A\right)}$$
11		reldmress	$$⊢\mathrm{Rel}\mathrm{dom}{\upharpoonright }_{𝑠}$$
12		eqid	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}A={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}A$$
13	11 12 8	elbasov	$$⊢0_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}A\right)}\in {\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}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}}{\upharpoonright }_{𝑠}A\right)}$$
18	15 17	syl	$$⊢\phi \to A\cap ℂ={\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}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}}{\upharpoonright }_{𝑠}K={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\left(A\cap ℂ\right)$$
22	16	ressinbas	$$⊢A\in \mathrm{V}\to {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}A={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\left(A\cap ℂ\right)$$
23	15 22	syl	$$⊢\phi \to {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}A={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\left(A\cap ℂ\right)$$
24	21 23	eqtr4d	$$⊢\phi \to {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}A$$
25	2 24	eqtr4d	$$⊢\phi \to F={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K$$
26	25 6	eqeltrrd	$$⊢\phi \to {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}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}}{\upharpoonright }_{𝑠}K\in \mathrm{Ring}\right)$$
29	12 16	ressbasss	$$⊢{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}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}}{\upharpoonright }_{𝑠}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}}{\upharpoonright }_{𝑠}K\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\in \mathrm{Grp}$$
40	26 39	syl	$$⊢\phi \to {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\in \mathrm{Grp}$$
41	16	issubg	$$⊢K\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\leftrightarrow \left({ℂ}_{\mathrm{fld}}\in \mathrm{Grp}\wedge K\subseteq ℂ\wedge {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}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}}{\upharpoonright }_{𝑠}K={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}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}}{\upharpoonright }_{𝑠}K\right)}$$
46	42 45	syl	$$⊢\phi \to 0=0_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}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 \neg 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}}{\upharpoonright }_{𝑠}K\right)}$$
55	54	oveq1d	$$⊢\phi \to 1_F{1}_F=1_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\right)}{1}_F$$
56	25	fveq2d	$$⊢\phi \to {\mathrm{Base}}_F={\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\right)}$$
57	1 56	syl5eq	$$⊢\phi \to K={\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\right)}$$
58	51 57	eleqtrd	$$⊢\phi \to 1_F\in {\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\right)}$$
59		eqid	$$⊢{\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\right)}={\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\right)}$$
60	1	fvexi	$$⊢K\in \mathrm{V}$$
61		cnfldmul	$$⊢\times ={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
62	43 61	ressmulr	$$⊢K\in \mathrm{V}\to \times ={\cdot }_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\right)}$$
63	60 62	ax-mp	$$⊢\times ={\cdot }_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\right)}$$
64		eqid	$$⊢1_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\right)}=1_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\right)}$$
65	59 63 64	ringlidm	$$⊢\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\in \mathrm{Ring}\wedge 1_F\in {\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\right)}\right)\to 1_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\right)}{1}_F=1_F$$
66	26 58 65	syl2anc	$$⊢\phi \to 1_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}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\leftrightarrow \left(1_F=0\vee 1_F=1\right)\right)$$
69	52 68	syl	$$⊢\phi \to \left({1_F}^2=1_F\leftrightarrow \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(\neg 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)\leftrightarrow \left(\left({ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\wedge {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}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}}{\upharpoonright }_{𝑠}K\wedge K=A\cap ℂ\wedge K\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\right)$$