Theorem cphreccllem

Description: Lemma for cphreccl . (Contributed by Mario Carneiro, 8-Oct-2015)

	Ref	Expression
Hypotheses	cphsubrglem.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
	cphsubrglem.1	⊢ ( 𝜑 → 𝐹 = ( ℂfld ↾s 𝐴 ) )
	cphsubrglem.2	⊢ ( 𝜑 → 𝐹 ∈ DivRing )
Assertion	cphreccllem	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0 ) → ( 1 / 𝑋 ) ∈ 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		cphsubrglem.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
2		cphsubrglem.1	⊢ ( 𝜑 → 𝐹 = ( ℂfld ↾s 𝐴 ) )
3		cphsubrglem.2	⊢ ( 𝜑 → 𝐹 ∈ DivRing )
4	1 2 3	cphsubrglem	⊢ ( 𝜑 → ( 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 = ( 𝐴 ∩ ℂ ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) )
5	4	simp3d	⊢ ( 𝜑 → 𝐾 ∈ ( SubRing ‘ ℂfld ) )
6	5	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0 ) → 𝐾 ∈ ( SubRing ‘ ℂfld ) )
7		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
8	7	subrgss	⊢ ( 𝐾 ∈ ( SubRing ‘ ℂfld ) → 𝐾 ⊆ ℂ )
9	6 8	syl	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0 ) → 𝐾 ⊆ ℂ )
10		simp2	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ 𝐾 )
11	9 10	sseldd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ ℂ )
12		simp3	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0 ) → 𝑋 ≠ 0 )
13		cnfldinv	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑋 ≠ 0 ) → ( ( invr ‘ ℂfld ) ‘ 𝑋 ) = ( 1 / 𝑋 ) )
14	11 12 13	syl2anc	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0 ) → ( ( invr ‘ ℂfld ) ‘ 𝑋 ) = ( 1 / 𝑋 ) )
15		eqid	⊢ ( ℂfld ↾s 𝐾 ) = ( ℂfld ↾s 𝐾 )
16		cnfld0	⊢ 0 = ( 0g ‘ ℂfld )
17	15 16	subrg0	⊢ ( 𝐾 ∈ ( SubRing ‘ ℂfld ) → 0 = ( 0g ‘ ( ℂfld ↾s 𝐾 ) ) )
18	6 17	syl	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0 ) → 0 = ( 0g ‘ ( ℂfld ↾s 𝐾 ) ) )
19	4	simp1d	⊢ ( 𝜑 → 𝐹 = ( ℂfld ↾s 𝐾 ) )
20	19	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0 ) → 𝐹 = ( ℂfld ↾s 𝐾 ) )
21	20	fveq2d	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0 ) → ( 0g ‘ 𝐹 ) = ( 0g ‘ ( ℂfld ↾s 𝐾 ) ) )
22	18 21	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0 ) → 0 = ( 0g ‘ 𝐹 ) )
23	12 22	neeqtrd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0 ) → 𝑋 ≠ ( 0g ‘ 𝐹 ) )
24		eldifsn	⊢ ( 𝑋 ∈ ( 𝐾 ∖ { ( 0g ‘ 𝐹 ) } ) ↔ ( 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ ( 0g ‘ 𝐹 ) ) )
25	10 23 24	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ ( 𝐾 ∖ { ( 0g ‘ 𝐹 ) } ) )
26	3	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0 ) → 𝐹 ∈ DivRing )
27		eqid	⊢ ( Unit ‘ 𝐹 ) = ( Unit ‘ 𝐹 )
28		eqid	⊢ ( 0g ‘ 𝐹 ) = ( 0g ‘ 𝐹 )
29	1 27 28	isdrng	⊢ ( 𝐹 ∈ DivRing ↔ ( 𝐹 ∈ Ring ∧ ( Unit ‘ 𝐹 ) = ( 𝐾 ∖ { ( 0g ‘ 𝐹 ) } ) ) )
30	29	simprbi	⊢ ( 𝐹 ∈ DivRing → ( Unit ‘ 𝐹 ) = ( 𝐾 ∖ { ( 0g ‘ 𝐹 ) } ) )
31	26 30	syl	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0 ) → ( Unit ‘ 𝐹 ) = ( 𝐾 ∖ { ( 0g ‘ 𝐹 ) } ) )
32	20	fveq2d	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0 ) → ( Unit ‘ 𝐹 ) = ( Unit ‘ ( ℂfld ↾s 𝐾 ) ) )
33	31 32	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0 ) → ( 𝐾 ∖ { ( 0g ‘ 𝐹 ) } ) = ( Unit ‘ ( ℂfld ↾s 𝐾 ) ) )
34	25 33	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ ( Unit ‘ ( ℂfld ↾s 𝐾 ) ) )
35		eqid	⊢ ( Unit ‘ ℂfld ) = ( Unit ‘ ℂfld )
36		eqid	⊢ ( Unit ‘ ( ℂfld ↾s 𝐾 ) ) = ( Unit ‘ ( ℂfld ↾s 𝐾 ) )
37		eqid	⊢ ( invr ‘ ℂfld ) = ( invr ‘ ℂfld )
38	15 35 36 37	subrgunit	⊢ ( 𝐾 ∈ ( SubRing ‘ ℂfld ) → ( 𝑋 ∈ ( Unit ‘ ( ℂfld ↾s 𝐾 ) ) ↔ ( 𝑋 ∈ ( Unit ‘ ℂfld ) ∧ 𝑋 ∈ 𝐾 ∧ ( ( invr ‘ ℂfld ) ‘ 𝑋 ) ∈ 𝐾 ) ) )
39	6 38	syl	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0 ) → ( 𝑋 ∈ ( Unit ‘ ( ℂfld ↾s 𝐾 ) ) ↔ ( 𝑋 ∈ ( Unit ‘ ℂfld ) ∧ 𝑋 ∈ 𝐾 ∧ ( ( invr ‘ ℂfld ) ‘ 𝑋 ) ∈ 𝐾 ) ) )
40	34 39	mpbid	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0 ) → ( 𝑋 ∈ ( Unit ‘ ℂfld ) ∧ 𝑋 ∈ 𝐾 ∧ ( ( invr ‘ ℂfld ) ‘ 𝑋 ) ∈ 𝐾 ) )
41	40	simp3d	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0 ) → ( ( invr ‘ ℂfld ) ‘ 𝑋 ) ∈ 𝐾 )
42	14 41	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0 ) → ( 1 / 𝑋 ) ∈ 𝐾 )