cphreccllem

	Ref	Expression
Hypotheses	cphsubrglem.k	$⊢ K = {Base}_{F}$
	cphsubrglem.1	$⊢ φ \to F = ℂ_{fld} ↾_{𝑠} A$
	cphsubrglem.2	$⊢ φ \to F \in DivRing$
Assertion	cphreccllem	$⊢ (φ \land X \in K \land X \neq 0) \to \frac{1}{X} \in K$

Proof

Step	Hyp	Ref	Expression
1		cphsubrglem.k	$⊢ K = {Base}_{F}$
2		cphsubrglem.1	$⊢ φ \to F = ℂ_{fld} ↾_{𝑠} A$
3		cphsubrglem.2	$⊢ φ \to F \in DivRing$
4	1 2 3	cphsubrglem	$⊢ φ \to (F = ℂ_{fld} ↾_{𝑠} K \land K = A \cap ℂ \land K \in SubRing (ℂ_{fld}))$
5	4	simp3d	$⊢ φ \to K \in SubRing (ℂ_{fld})$
6	5	3ad2ant1	$⊢ (φ \land X \in K \land X \neq 0) \to K \in SubRing (ℂ_{fld})$
7		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
8	7	subrgss	$⊢ K \in SubRing (ℂ_{fld}) \to K \subseteq ℂ$
9	6 8	syl	$⊢ (φ \land X \in K \land X \neq 0) \to K \subseteq ℂ$
10		simp2	$⊢ (φ \land X \in K \land X \neq 0) \to X \in K$
11	9 10	sseldd	$⊢ (φ \land X \in K \land X \neq 0) \to X \in ℂ$
12		simp3	$⊢ (φ \land X \in K \land X \neq 0) \to X \neq 0$
13		cnfldinv	$⊢ (X \in ℂ \land X \neq 0) \to {inv}_{r} (ℂ_{fld}) (X) = \frac{1}{X}$
14	11 12 13	syl2anc	$⊢ (φ \land X \in K \land X \neq 0) \to {inv}_{r} (ℂ_{fld}) (X) = \frac{1}{X}$
15		eqid	$⊢ ℂ_{fld} ↾_{𝑠} K = ℂ_{fld} ↾_{𝑠} K$
16		cnfld0	$⊢ 0 = 0_{ℂ_{fld}}$
17	15 16	subrg0	$⊢ K \in SubRing (ℂ_{fld}) \to 0 = 0_{(ℂ_{fld} ↾_{𝑠} K)}$
18	6 17	syl	$⊢ (φ \land X \in K \land X \neq 0) \to 0 = 0_{(ℂ_{fld} ↾_{𝑠} K)}$
19	4	simp1d	$⊢ φ \to F = ℂ_{fld} ↾_{𝑠} K$
20	19	3ad2ant1	$⊢ (φ \land X \in K \land X \neq 0) \to F = ℂ_{fld} ↾_{𝑠} K$
21	20	fveq2d	$⊢ (φ \land X \in K \land X \neq 0) \to 0_{F} = 0_{(ℂ_{fld} ↾_{𝑠} K)}$
22	18 21	eqtr4d	$⊢ (φ \land X \in K \land X \neq 0) \to 0 = 0_{F}$
23	12 22	neeqtrd	$⊢ (φ \land X \in K \land X \neq 0) \to X \neq 0_{F}$
24		eldifsn	$⊢ X \in (K ∖ \{0_{F}\}) \leftrightarrow (X \in K \land X \neq 0_{F})$
25	10 23 24	sylanbrc	$⊢ (φ \land X \in K \land X \neq 0) \to X \in (K ∖ \{0_{F}\})$
26	3	3ad2ant1	$⊢ (φ \land X \in K \land X \neq 0) \to F \in DivRing$
27		eqid	$⊢ Unit (F) = Unit (F)$
28		eqid	$⊢ 0_{F} = 0_{F}$
29	1 27 28	isdrng	$⊢ F \in DivRing \leftrightarrow (F \in Ring \land Unit (F) = K ∖ \{0_{F}\})$
30	29	simprbi	$⊢ F \in DivRing \to Unit (F) = K ∖ \{0_{F}\}$
31	26 30	syl	$⊢ (φ \land X \in K \land X \neq 0) \to Unit (F) = K ∖ \{0_{F}\}$
32	20	fveq2d	$⊢ (φ \land X \in K \land X \neq 0) \to Unit (F) = Unit (ℂ_{fld} ↾_{𝑠} K)$
33	31 32	eqtr3d	$⊢ (φ \land X \in K \land X \neq 0) \to K ∖ \{0_{F}\} = Unit (ℂ_{fld} ↾_{𝑠} K)$
34	25 33	eleqtrd	$⊢ (φ \land X \in K \land X \neq 0) \to X \in Unit (ℂ_{fld} ↾_{𝑠} K)$
35		eqid	$⊢ Unit (ℂ_{fld}) = Unit (ℂ_{fld})$
36		eqid	$⊢ Unit (ℂ_{fld} ↾_{𝑠} K) = Unit (ℂ_{fld} ↾_{𝑠} K)$
37		eqid	$⊢ {inv}_{r} (ℂ_{fld}) = {inv}_{r} (ℂ_{fld})$
38	15 35 36 37	subrgunit	$⊢ K \in SubRing (ℂ_{fld}) \to (X \in Unit (ℂ_{fld} ↾_{𝑠} K) \leftrightarrow (X \in Unit (ℂ_{fld}) \land X \in K \land {inv}_{r} (ℂ_{fld}) (X) \in K))$
39	6 38	syl	$⊢ (φ \land X \in K \land X \neq 0) \to (X \in Unit (ℂ_{fld} ↾_{𝑠} K) \leftrightarrow (X \in Unit (ℂ_{fld}) \land X \in K \land {inv}_{r} (ℂ_{fld}) (X) \in K))$
40	34 39	mpbid	$⊢ (φ \land X \in K \land X \neq 0) \to (X \in Unit (ℂ_{fld}) \land X \in K \land {inv}_{r} (ℂ_{fld}) (X) \in K)$
41	40	simp3d	$⊢ (φ \land X \in K \land X \neq 0) \to {inv}_{r} (ℂ_{fld}) (X) \in K$
42	14 41	eqeltrrd	$⊢ (φ \land X \in K \land X \neq 0) \to \frac{1}{X} \in K$

Metamath Proof Explorer

Theorem cphreccllem

Proof