Theorem cphsubrglem

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

	Ref	Expression
Hypotheses	cphsubrglem.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
	cphsubrglem.1	⊢ ( 𝜑 → 𝐹 = ( ℂfld ↾s 𝐴 ) )
	cphsubrglem.2	⊢ ( 𝜑 → 𝐹 ∈ DivRing )
Assertion	cphsubrglem	⊢ ( 𝜑 → ( 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 = ( 𝐴 ∩ ℂ ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) )

Proof

Step	Hyp	Ref	Expression
1		cphsubrglem.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
2		cphsubrglem.1	⊢ ( 𝜑 → 𝐹 = ( ℂfld ↾s 𝐴 ) )
3		cphsubrglem.2	⊢ ( 𝜑 → 𝐹 ∈ DivRing )
4	2	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝐹 ) = ( Base ‘ ( ℂfld ↾s 𝐴 ) ) )
5		drngring	⊢ ( 𝐹 ∈ DivRing → 𝐹 ∈ Ring )
6	3 5	syl	⊢ ( 𝜑 → 𝐹 ∈ Ring )
7	2 6	eqeltrrd	⊢ ( 𝜑 → ( ℂfld ↾s 𝐴 ) ∈ Ring )
8		eqid	⊢ ( Base ‘ ( ℂfld ↾s 𝐴 ) ) = ( Base ‘ ( ℂfld ↾s 𝐴 ) )
9		eqid	⊢ ( 0g ‘ ( ℂfld ↾s 𝐴 ) ) = ( 0g ‘ ( ℂfld ↾s 𝐴 ) )
10	8 9	ring0cl	⊢ ( ( ℂfld ↾s 𝐴 ) ∈ Ring → ( 0g ‘ ( ℂfld ↾s 𝐴 ) ) ∈ ( Base ‘ ( ℂfld ↾s 𝐴 ) ) )
11		reldmress	⊢ Rel dom ↾s
12		eqid	⊢ ( ℂfld ↾s 𝐴 ) = ( ℂfld ↾s 𝐴 )
13	11 12 8	elbasov	⊢ ( ( 0g ‘ ( ℂfld ↾s 𝐴 ) ) ∈ ( Base ‘ ( ℂfld ↾s 𝐴 ) ) → ( ℂfld ∈ V ∧ 𝐴 ∈ V ) )
14	7 10 13	3syl	⊢ ( 𝜑 → ( ℂfld ∈ V ∧ 𝐴 ∈ V ) )
15	14	simprd	⊢ ( 𝜑 → 𝐴 ∈ V )
16		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
17	12 16	ressbas	⊢ ( 𝐴 ∈ V → ( 𝐴 ∩ ℂ ) = ( Base ‘ ( ℂfld ↾s 𝐴 ) ) )
18	15 17	syl	⊢ ( 𝜑 → ( 𝐴 ∩ ℂ ) = ( Base ‘ ( ℂfld ↾s 𝐴 ) ) )
19	4 18	eqtr4d	⊢ ( 𝜑 → ( Base ‘ 𝐹 ) = ( 𝐴 ∩ ℂ ) )
20	1 19	syl5eq	⊢ ( 𝜑 → 𝐾 = ( 𝐴 ∩ ℂ ) )
21	20	oveq2d	⊢ ( 𝜑 → ( ℂfld ↾s 𝐾 ) = ( ℂfld ↾s ( 𝐴 ∩ ℂ ) ) )
22	16	ressinbas	⊢ ( 𝐴 ∈ V → ( ℂfld ↾s 𝐴 ) = ( ℂfld ↾s ( 𝐴 ∩ ℂ ) ) )
23	15 22	syl	⊢ ( 𝜑 → ( ℂfld ↾s 𝐴 ) = ( ℂfld ↾s ( 𝐴 ∩ ℂ ) ) )
24	21 23	eqtr4d	⊢ ( 𝜑 → ( ℂfld ↾s 𝐾 ) = ( ℂfld ↾s 𝐴 ) )
25	2 24	eqtr4d	⊢ ( 𝜑 → 𝐹 = ( ℂfld ↾s 𝐾 ) )
26	25 6	eqeltrrd	⊢ ( 𝜑 → ( ℂfld ↾s 𝐾 ) ∈ Ring )
27		cnring	⊢ ℂfld ∈ Ring
28	26 27	jctil	⊢ ( 𝜑 → ( ℂfld ∈ Ring ∧ ( ℂfld ↾s 𝐾 ) ∈ Ring ) )
29	12 16	ressbasss	⊢ ( Base ‘ ( ℂfld ↾s 𝐴 ) ) ⊆ ℂ
30	4 29	eqsstrdi	⊢ ( 𝜑 → ( Base ‘ 𝐹 ) ⊆ ℂ )
31	1 30	eqsstrid	⊢ ( 𝜑 → 𝐾 ⊆ ℂ )
32		eqid	⊢ ( 0g ‘ 𝐹 ) = ( 0g ‘ 𝐹 )
33		eqid	⊢ ( 1r ‘ 𝐹 ) = ( 1r ‘ 𝐹 )
34	32 33	drngunz	⊢ ( 𝐹 ∈ DivRing → ( 1r ‘ 𝐹 ) ≠ ( 0g ‘ 𝐹 ) )
35	3 34	syl	⊢ ( 𝜑 → ( 1r ‘ 𝐹 ) ≠ ( 0g ‘ 𝐹 ) )
36	25	fveq2d	⊢ ( 𝜑 → ( 0g ‘ 𝐹 ) = ( 0g ‘ ( ℂfld ↾s 𝐾 ) ) )
37		ringgrp	⊢ ( ℂfld ∈ Ring → ℂfld ∈ Grp )
38	27 37	mp1i	⊢ ( 𝜑 → ℂfld ∈ Grp )
39		ringgrp	⊢ ( ( ℂfld ↾s 𝐾 ) ∈ Ring → ( ℂfld ↾s 𝐾 ) ∈ Grp )
40	26 39	syl	⊢ ( 𝜑 → ( ℂfld ↾s 𝐾 ) ∈ Grp )
41	16	issubg	⊢ ( 𝐾 ∈ ( SubGrp ‘ ℂfld ) ↔ ( ℂfld ∈ Grp ∧ 𝐾 ⊆ ℂ ∧ ( ℂfld ↾s 𝐾 ) ∈ Grp ) )
42	38 31 40 41	syl3anbrc	⊢ ( 𝜑 → 𝐾 ∈ ( SubGrp ‘ ℂfld ) )
43		eqid	⊢ ( ℂfld ↾s 𝐾 ) = ( ℂfld ↾s 𝐾 )
44		cnfld0	⊢ 0 = ( 0g ‘ ℂfld )
45	43 44	subg0	⊢ ( 𝐾 ∈ ( SubGrp ‘ ℂfld ) → 0 = ( 0g ‘ ( ℂfld ↾s 𝐾 ) ) )
46	42 45	syl	⊢ ( 𝜑 → 0 = ( 0g ‘ ( ℂfld ↾s 𝐾 ) ) )
47	36 46	eqtr4d	⊢ ( 𝜑 → ( 0g ‘ 𝐹 ) = 0 )
48	35 47	neeqtrd	⊢ ( 𝜑 → ( 1r ‘ 𝐹 ) ≠ 0 )
49	48	neneqd	⊢ ( 𝜑 → ¬ ( 1r ‘ 𝐹 ) = 0 )
50	1 33	ringidcl	⊢ ( 𝐹 ∈ Ring → ( 1r ‘ 𝐹 ) ∈ 𝐾 )
51	6 50	syl	⊢ ( 𝜑 → ( 1r ‘ 𝐹 ) ∈ 𝐾 )
52	31 51	sseldd	⊢ ( 𝜑 → ( 1r ‘ 𝐹 ) ∈ ℂ )
53	52	sqvald	⊢ ( 𝜑 → ( ( 1r ‘ 𝐹 ) ↑ 2 ) = ( ( 1r ‘ 𝐹 ) · ( 1r ‘ 𝐹 ) ) )
54	25	fveq2d	⊢ ( 𝜑 → ( 1r ‘ 𝐹 ) = ( 1r ‘ ( ℂfld ↾s 𝐾 ) ) )
55	54	oveq1d	⊢ ( 𝜑 → ( ( 1r ‘ 𝐹 ) · ( 1r ‘ 𝐹 ) ) = ( ( 1r ‘ ( ℂfld ↾s 𝐾 ) ) · ( 1r ‘ 𝐹 ) ) )
56	25	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝐹 ) = ( Base ‘ ( ℂfld ↾s 𝐾 ) ) )
57	1 56	syl5eq	⊢ ( 𝜑 → 𝐾 = ( Base ‘ ( ℂfld ↾s 𝐾 ) ) )
58	51 57	eleqtrd	⊢ ( 𝜑 → ( 1r ‘ 𝐹 ) ∈ ( Base ‘ ( ℂfld ↾s 𝐾 ) ) )
59		eqid	⊢ ( Base ‘ ( ℂfld ↾s 𝐾 ) ) = ( Base ‘ ( ℂfld ↾s 𝐾 ) )
60	1	fvexi	⊢ 𝐾 ∈ V
61		cnfldmul	⊢ · = ( .r ‘ ℂfld )
62	43 61	ressmulr	⊢ ( 𝐾 ∈ V → · = ( .r ‘ ( ℂfld ↾s 𝐾 ) ) )
63	60 62	ax-mp	⊢ · = ( .r ‘ ( ℂfld ↾s 𝐾 ) )
64		eqid	⊢ ( 1r ‘ ( ℂfld ↾s 𝐾 ) ) = ( 1r ‘ ( ℂfld ↾s 𝐾 ) )
65	59 63 64	ringlidm	⊢ ( ( ( ℂfld ↾s 𝐾 ) ∈ Ring ∧ ( 1r ‘ 𝐹 ) ∈ ( Base ‘ ( ℂfld ↾s 𝐾 ) ) ) → ( ( 1r ‘ ( ℂfld ↾s 𝐾 ) ) · ( 1r ‘ 𝐹 ) ) = ( 1r ‘ 𝐹 ) )
66	26 58 65	syl2anc	⊢ ( 𝜑 → ( ( 1r ‘ ( ℂfld ↾s 𝐾 ) ) · ( 1r ‘ 𝐹 ) ) = ( 1r ‘ 𝐹 ) )
67	53 55 66	3eqtrd	⊢ ( 𝜑 → ( ( 1r ‘ 𝐹 ) ↑ 2 ) = ( 1r ‘ 𝐹 ) )
68		sq01	⊢ ( ( 1r ‘ 𝐹 ) ∈ ℂ → ( ( ( 1r ‘ 𝐹 ) ↑ 2 ) = ( 1r ‘ 𝐹 ) ↔ ( ( 1r ‘ 𝐹 ) = 0 ∨ ( 1r ‘ 𝐹 ) = 1 ) ) )
69	52 68	syl	⊢ ( 𝜑 → ( ( ( 1r ‘ 𝐹 ) ↑ 2 ) = ( 1r ‘ 𝐹 ) ↔ ( ( 1r ‘ 𝐹 ) = 0 ∨ ( 1r ‘ 𝐹 ) = 1 ) ) )
70	67 69	mpbid	⊢ ( 𝜑 → ( ( 1r ‘ 𝐹 ) = 0 ∨ ( 1r ‘ 𝐹 ) = 1 ) )
71	70	ord	⊢ ( 𝜑 → ( ¬ ( 1r ‘ 𝐹 ) = 0 → ( 1r ‘ 𝐹 ) = 1 ) )
72	49 71	mpd	⊢ ( 𝜑 → ( 1r ‘ 𝐹 ) = 1 )
73	72 51	eqeltrrd	⊢ ( 𝜑 → 1 ∈ 𝐾 )
74	31 73	jca	⊢ ( 𝜑 → ( 𝐾 ⊆ ℂ ∧ 1 ∈ 𝐾 ) )
75		cnfld1	⊢ 1 = ( 1r ‘ ℂfld )
76	16 75	issubrg	⊢ ( 𝐾 ∈ ( SubRing ‘ ℂfld ) ↔ ( ( ℂfld ∈ Ring ∧ ( ℂfld ↾s 𝐾 ) ∈ Ring ) ∧ ( 𝐾 ⊆ ℂ ∧ 1 ∈ 𝐾 ) ) )
77	28 74 76	sylanbrc	⊢ ( 𝜑 → 𝐾 ∈ ( SubRing ‘ ℂfld ) )
78	25 20 77	3jca	⊢ ( 𝜑 → ( 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 = ( 𝐴 ∩ ℂ ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) )