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

Metamath Proof Explorer

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 eqtrid ⊢ ( 𝜑 → 𝐾 = ( 𝐴 ∩ ℂ ) )
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 eqtrid ⊢ ( 𝜑 → 𝐾 = ( 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 ) ) )