Proof of Theorem cphsubrglem
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cphsubrglem.1 | . . 3
⊢ (𝜑 → 𝐹 = (ℂfld
↾s 𝐴)) | 
| 2 |  | cphsubrglem.k | . . . . . 6
⊢ 𝐾 = (Base‘𝐹) | 
| 3 | 1 | fveq2d 6909 | . . . . . . 7
⊢ (𝜑 → (Base‘𝐹) =
(Base‘(ℂfld ↾s 𝐴))) | 
| 4 |  | cphsubrglem.2 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 ∈ DivRing) | 
| 5 |  | drngring 20737 | . . . . . . . . . . . 12
⊢ (𝐹 ∈ DivRing → 𝐹 ∈ Ring) | 
| 6 | 4, 5 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ Ring) | 
| 7 | 1, 6 | eqeltrrd 2841 | . . . . . . . . . 10
⊢ (𝜑 → (ℂfld
↾s 𝐴)
∈ Ring) | 
| 8 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(Base‘(ℂfld ↾s 𝐴)) = (Base‘(ℂfld
↾s 𝐴)) | 
| 9 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(0g‘(ℂfld ↾s 𝐴)) =
(0g‘(ℂfld ↾s 𝐴)) | 
| 10 | 8, 9 | ring0cl 20265 | . . . . . . . . . 10
⊢
((ℂfld ↾s 𝐴) ∈ Ring →
(0g‘(ℂfld ↾s 𝐴)) ∈
(Base‘(ℂfld ↾s 𝐴))) | 
| 11 |  | reldmress 17277 | . . . . . . . . . . 11
⊢ Rel dom
↾s | 
| 12 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(ℂfld ↾s 𝐴) = (ℂfld
↾s 𝐴) | 
| 13 | 11, 12, 8 | elbasov 17255 | . . . . . . . . . 10
⊢
((0g‘(ℂfld ↾s 𝐴)) ∈
(Base‘(ℂfld ↾s 𝐴)) → (ℂfld ∈ V
∧ 𝐴 ∈
V)) | 
| 14 | 7, 10, 13 | 3syl 18 | . . . . . . . . 9
⊢ (𝜑 → (ℂfld
∈ V ∧ 𝐴 ∈
V)) | 
| 15 | 14 | simprd 495 | . . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ V) | 
| 16 |  | cnfldbas 21369 | . . . . . . . . 9
⊢ ℂ =
(Base‘ℂfld) | 
| 17 | 12, 16 | ressbas 17281 | . . . . . . . 8
⊢ (𝐴 ∈ V → (𝐴 ∩ ℂ) =
(Base‘(ℂfld ↾s 𝐴))) | 
| 18 | 15, 17 | syl 17 | . . . . . . 7
⊢ (𝜑 → (𝐴 ∩ ℂ) =
(Base‘(ℂfld ↾s 𝐴))) | 
| 19 | 3, 18 | eqtr4d 2779 | . . . . . 6
⊢ (𝜑 → (Base‘𝐹) = (𝐴 ∩ ℂ)) | 
| 20 | 2, 19 | eqtrid 2788 | . . . . 5
⊢ (𝜑 → 𝐾 = (𝐴 ∩ ℂ)) | 
| 21 | 20 | oveq2d 7448 | . . . 4
⊢ (𝜑 → (ℂfld
↾s 𝐾) =
(ℂfld ↾s (𝐴 ∩ ℂ))) | 
| 22 | 16 | ressinbas 17292 | . . . . 5
⊢ (𝐴 ∈ V →
(ℂfld ↾s 𝐴) = (ℂfld
↾s (𝐴
∩ ℂ))) | 
| 23 | 15, 22 | syl 17 | . . . 4
⊢ (𝜑 → (ℂfld
↾s 𝐴) =
(ℂfld ↾s (𝐴 ∩ ℂ))) | 
| 24 | 21, 23 | eqtr4d 2779 | . . 3
⊢ (𝜑 → (ℂfld
↾s 𝐾) =
(ℂfld ↾s 𝐴)) | 
| 25 | 1, 24 | eqtr4d 2779 | . 2
⊢ (𝜑 → 𝐹 = (ℂfld
↾s 𝐾)) | 
| 26 | 25, 6 | eqeltrrd 2841 | . . . 4
⊢ (𝜑 → (ℂfld
↾s 𝐾)
∈ Ring) | 
| 27 |  | cnring 21404 | . . . 4
⊢
ℂfld ∈ Ring | 
| 28 | 26, 27 | jctil 519 | . . 3
⊢ (𝜑 → (ℂfld
∈ Ring ∧ (ℂfld ↾s 𝐾) ∈ Ring)) | 
| 29 | 12, 16 | ressbasss 17285 | . . . . . 6
⊢
(Base‘(ℂfld ↾s 𝐴)) ⊆ ℂ | 
| 30 | 3, 29 | eqsstrdi 4027 | . . . . 5
⊢ (𝜑 → (Base‘𝐹) ⊆
ℂ) | 
| 31 | 2, 30 | eqsstrid 4021 | . . . 4
⊢ (𝜑 → 𝐾 ⊆ ℂ) | 
| 32 |  | eqid 2736 | . . . . . . . . . 10
⊢
(0g‘𝐹) = (0g‘𝐹) | 
| 33 |  | eqid 2736 | . . . . . . . . . 10
⊢
(1r‘𝐹) = (1r‘𝐹) | 
| 34 | 32, 33 | drngunz 20748 | . . . . . . . . 9
⊢ (𝐹 ∈ DivRing →
(1r‘𝐹)
≠ (0g‘𝐹)) | 
| 35 | 4, 34 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (1r‘𝐹) ≠
(0g‘𝐹)) | 
| 36 | 25 | fveq2d 6909 | . . . . . . . . 9
⊢ (𝜑 → (0g‘𝐹) =
(0g‘(ℂfld ↾s 𝐾))) | 
| 37 |  | ringgrp 20236 | . . . . . . . . . . . 12
⊢
(ℂfld ∈ Ring → ℂfld ∈
Grp) | 
| 38 | 27, 37 | mp1i 13 | . . . . . . . . . . 11
⊢ (𝜑 → ℂfld
∈ Grp) | 
| 39 |  | ringgrp 20236 | . . . . . . . . . . . 12
⊢
((ℂfld ↾s 𝐾) ∈ Ring → (ℂfld
↾s 𝐾)
∈ Grp) | 
| 40 | 26, 39 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (ℂfld
↾s 𝐾)
∈ Grp) | 
| 41 | 16 | issubg 19145 | . . . . . . . . . . 11
⊢ (𝐾 ∈
(SubGrp‘ℂfld) ↔ (ℂfld ∈ Grp
∧ 𝐾 ⊆ ℂ
∧ (ℂfld ↾s 𝐾) ∈ Grp)) | 
| 42 | 38, 31, 40, 41 | syl3anbrc 1343 | . . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈
(SubGrp‘ℂfld)) | 
| 43 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(ℂfld ↾s 𝐾) = (ℂfld
↾s 𝐾) | 
| 44 |  | cnfld0 21406 | . . . . . . . . . . 11
⊢ 0 =
(0g‘ℂfld) | 
| 45 | 43, 44 | subg0 19151 | . . . . . . . . . 10
⊢ (𝐾 ∈
(SubGrp‘ℂfld) → 0 =
(0g‘(ℂfld ↾s 𝐾))) | 
| 46 | 42, 45 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 0 =
(0g‘(ℂfld ↾s 𝐾))) | 
| 47 | 36, 46 | eqtr4d 2779 | . . . . . . . 8
⊢ (𝜑 → (0g‘𝐹) = 0) | 
| 48 | 35, 47 | neeqtrd 3009 | . . . . . . 7
⊢ (𝜑 → (1r‘𝐹) ≠ 0) | 
| 49 | 48 | neneqd 2944 | . . . . . 6
⊢ (𝜑 → ¬
(1r‘𝐹) =
0) | 
| 50 | 2, 33 | ringidcl 20263 | . . . . . . . . . . . 12
⊢ (𝐹 ∈ Ring →
(1r‘𝐹)
∈ 𝐾) | 
| 51 | 6, 50 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (1r‘𝐹) ∈ 𝐾) | 
| 52 | 31, 51 | sseldd 3983 | . . . . . . . . . 10
⊢ (𝜑 → (1r‘𝐹) ∈
ℂ) | 
| 53 | 52 | sqvald 14184 | . . . . . . . . 9
⊢ (𝜑 →
((1r‘𝐹)↑2) = ((1r‘𝐹) ·
(1r‘𝐹))) | 
| 54 | 25 | fveq2d 6909 | . . . . . . . . . 10
⊢ (𝜑 → (1r‘𝐹) =
(1r‘(ℂfld ↾s 𝐾))) | 
| 55 | 54 | oveq1d 7447 | . . . . . . . . 9
⊢ (𝜑 →
((1r‘𝐹)
· (1r‘𝐹)) =
((1r‘(ℂfld ↾s 𝐾)) ·
(1r‘𝐹))) | 
| 56 | 25 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ (𝜑 → (Base‘𝐹) =
(Base‘(ℂfld ↾s 𝐾))) | 
| 57 | 2, 56 | eqtrid 2788 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐾 = (Base‘(ℂfld
↾s 𝐾))) | 
| 58 | 51, 57 | eleqtrd 2842 | . . . . . . . . . 10
⊢ (𝜑 → (1r‘𝐹) ∈
(Base‘(ℂfld ↾s 𝐾))) | 
| 59 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(Base‘(ℂfld ↾s 𝐾)) = (Base‘(ℂfld
↾s 𝐾)) | 
| 60 | 2 | fvexi 6919 | . . . . . . . . . . . 12
⊢ 𝐾 ∈ V | 
| 61 |  | cnfldmul 21373 | . . . . . . . . . . . . 13
⊢  ·
= (.r‘ℂfld) | 
| 62 | 43, 61 | ressmulr 17352 | . . . . . . . . . . . 12
⊢ (𝐾 ∈ V → · =
(.r‘(ℂfld ↾s 𝐾))) | 
| 63 | 60, 62 | ax-mp 5 | . . . . . . . . . . 11
⊢  ·
= (.r‘(ℂfld ↾s 𝐾)) | 
| 64 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(1r‘(ℂfld ↾s 𝐾)) =
(1r‘(ℂfld ↾s 𝐾)) | 
| 65 | 59, 63, 64 | ringlidm 20267 | . . . . . . . . . 10
⊢
(((ℂfld ↾s 𝐾) ∈ Ring ∧
(1r‘𝐹)
∈ (Base‘(ℂfld ↾s 𝐾))) →
((1r‘(ℂfld ↾s 𝐾)) ·
(1r‘𝐹)) =
(1r‘𝐹)) | 
| 66 | 26, 58, 65 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 →
((1r‘(ℂfld ↾s 𝐾)) ·
(1r‘𝐹)) =
(1r‘𝐹)) | 
| 67 | 53, 55, 66 | 3eqtrd 2780 | . . . . . . . 8
⊢ (𝜑 →
((1r‘𝐹)↑2) = (1r‘𝐹)) | 
| 68 |  | sq01 14265 | . . . . . . . . 9
⊢
((1r‘𝐹) ∈ ℂ →
(((1r‘𝐹)↑2) = (1r‘𝐹) ↔
((1r‘𝐹) =
0 ∨ (1r‘𝐹) = 1))) | 
| 69 | 52, 68 | syl 17 | . . . . . . . 8
⊢ (𝜑 →
(((1r‘𝐹)↑2) = (1r‘𝐹) ↔
((1r‘𝐹) =
0 ∨ (1r‘𝐹) = 1))) | 
| 70 | 67, 69 | mpbid 232 | . . . . . . 7
⊢ (𝜑 →
((1r‘𝐹) =
0 ∨ (1r‘𝐹) = 1)) | 
| 71 | 70 | ord 864 | . . . . . 6
⊢ (𝜑 → (¬
(1r‘𝐹) = 0
→ (1r‘𝐹) = 1)) | 
| 72 | 49, 71 | mpd 15 | . . . . 5
⊢ (𝜑 → (1r‘𝐹) = 1) | 
| 73 | 72, 51 | eqeltrrd 2841 | . . . 4
⊢ (𝜑 → 1 ∈ 𝐾) | 
| 74 | 31, 73 | jca 511 | . . 3
⊢ (𝜑 → (𝐾 ⊆ ℂ ∧ 1 ∈ 𝐾)) | 
| 75 |  | cnfld1 21407 | . . . 4
⊢ 1 =
(1r‘ℂfld) | 
| 76 | 16, 75 | issubrg 20572 | . . 3
⊢ (𝐾 ∈
(SubRing‘ℂfld) ↔ ((ℂfld ∈
Ring ∧ (ℂfld ↾s 𝐾) ∈ Ring) ∧ (𝐾 ⊆ ℂ ∧ 1 ∈ 𝐾))) | 
| 77 | 28, 74, 76 | sylanbrc 583 | . 2
⊢ (𝜑 → 𝐾 ∈
(SubRing‘ℂfld)) | 
| 78 | 25, 20, 77 | 3jca 1128 | 1
⊢ (𝜑 → (𝐹 = (ℂfld
↾s 𝐾)
∧ 𝐾 = (𝐴 ∩ ℂ) ∧ 𝐾 ∈
(SubRing‘ℂfld))) |