This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 / 𝑋 ) ∈ 𝐾 )