| Step | Hyp | Ref
| Expression |
| 1 | | fldcrngo 38011 |
. . 3
⊢ (𝐾 ∈ Fld → 𝐾 ∈
CRingOps) |
| 2 | | flddivrng 38006 |
. . . 4
⊢ (𝐾 ∈ Fld → 𝐾 ∈
DivRingOps) |
| 3 | | isfldidl.1 |
. . . . 5
⊢ 𝐺 = (1st ‘𝐾) |
| 4 | | isfldidl.2 |
. . . . 5
⊢ 𝐻 = (2nd ‘𝐾) |
| 5 | | isfldidl.3 |
. . . . 5
⊢ 𝑋 = ran 𝐺 |
| 6 | | isfldidl.4 |
. . . . 5
⊢ 𝑍 = (GId‘𝐺) |
| 7 | | isfldidl.5 |
. . . . 5
⊢ 𝑈 = (GId‘𝐻) |
| 8 | 3, 4, 5, 6, 7 | dvrunz 37961 |
. . . 4
⊢ (𝐾 ∈ DivRingOps → 𝑈 ≠ 𝑍) |
| 9 | 2, 8 | syl 17 |
. . 3
⊢ (𝐾 ∈ Fld → 𝑈 ≠ 𝑍) |
| 10 | 3, 4, 5, 6 | divrngidl 38035 |
. . . 4
⊢ (𝐾 ∈ DivRingOps →
(Idl‘𝐾) = {{𝑍}, 𝑋}) |
| 11 | 2, 10 | syl 17 |
. . 3
⊢ (𝐾 ∈ Fld →
(Idl‘𝐾) = {{𝑍}, 𝑋}) |
| 12 | 1, 9, 11 | 3jca 1129 |
. 2
⊢ (𝐾 ∈ Fld → (𝐾 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝐾) = {{𝑍}, 𝑋})) |
| 13 | | crngorngo 38007 |
. . . . . 6
⊢ (𝐾 ∈ CRingOps → 𝐾 ∈
RingOps) |
| 14 | 13 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝐾 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) → 𝐾 ∈ RingOps) |
| 15 | | simp2 1138 |
. . . . 5
⊢ ((𝐾 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) → 𝑈 ≠ 𝑍) |
| 16 | 3 | rneqi 5948 |
. . . . . . . . . . . . . . 15
⊢ ran 𝐺 = ran (1st
‘𝐾) |
| 17 | 5, 16 | eqtri 2765 |
. . . . . . . . . . . . . 14
⊢ 𝑋 = ran (1st
‘𝐾) |
| 18 | 17, 4, 7 | rngo1cl 37946 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ RingOps → 𝑈 ∈ 𝑋) |
| 19 | 13, 18 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ CRingOps → 𝑈 ∈ 𝑋) |
| 20 | 19 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ CRingOps ∧
(Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → 𝑈 ∈ 𝑋) |
| 21 | | eldif 3961 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝑋 ∖ {𝑍}) ↔ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ {𝑍})) |
| 22 | | snssi 4808 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ 𝑋 → {𝑥} ⊆ 𝑋) |
| 23 | 3, 5 | igenss 38069 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐾 ∈ RingOps ∧ {𝑥} ⊆ 𝑋) → {𝑥} ⊆ (𝐾 IdlGen {𝑥})) |
| 24 | 22, 23 | sylan2 593 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 ∈ RingOps ∧ 𝑥 ∈ 𝑋) → {𝑥} ⊆ (𝐾 IdlGen {𝑥})) |
| 25 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑥 ∈ V |
| 26 | 25 | snss 4785 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (𝐾 IdlGen {𝑥}) ↔ {𝑥} ⊆ (𝐾 IdlGen {𝑥})) |
| 27 | 26 | biimpri 228 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ({𝑥} ⊆ (𝐾 IdlGen {𝑥}) → 𝑥 ∈ (𝐾 IdlGen {𝑥})) |
| 28 | | eleq2 2830 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐾 IdlGen {𝑥}) = {𝑍} → (𝑥 ∈ (𝐾 IdlGen {𝑥}) ↔ 𝑥 ∈ {𝑍})) |
| 29 | 27, 28 | syl5ibcom 245 |
. . . . . . . . . . . . . . . . . . 19
⊢ ({𝑥} ⊆ (𝐾 IdlGen {𝑥}) → ((𝐾 IdlGen {𝑥}) = {𝑍} → 𝑥 ∈ {𝑍})) |
| 30 | 29 | con3dimp 408 |
. . . . . . . . . . . . . . . . . 18
⊢ (({𝑥} ⊆ (𝐾 IdlGen {𝑥}) ∧ ¬ 𝑥 ∈ {𝑍}) → ¬ (𝐾 IdlGen {𝑥}) = {𝑍}) |
| 31 | 24, 30 | sylan 580 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐾 ∈ RingOps ∧ 𝑥 ∈ 𝑋) ∧ ¬ 𝑥 ∈ {𝑍}) → ¬ (𝐾 IdlGen {𝑥}) = {𝑍}) |
| 32 | 31 | anasss 466 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ RingOps ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ {𝑍})) → ¬ (𝐾 IdlGen {𝑥}) = {𝑍}) |
| 33 | 21, 32 | sylan2b 594 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ RingOps ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → ¬ (𝐾 IdlGen {𝑥}) = {𝑍}) |
| 34 | 33 | adantlr 715 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ RingOps ∧
(Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → ¬ (𝐾 IdlGen {𝑥}) = {𝑍}) |
| 35 | | eldifi 4131 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (𝑋 ∖ {𝑍}) → 𝑥 ∈ 𝑋) |
| 36 | 35 | snssd 4809 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (𝑋 ∖ {𝑍}) → {𝑥} ⊆ 𝑋) |
| 37 | 3, 5 | igenidl 38070 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐾 ∈ RingOps ∧ {𝑥} ⊆ 𝑋) → (𝐾 IdlGen {𝑥}) ∈ (Idl‘𝐾)) |
| 38 | 36, 37 | sylan2 593 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐾 ∈ RingOps ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (𝐾 IdlGen {𝑥}) ∈ (Idl‘𝐾)) |
| 39 | | eleq2 2830 |
. . . . . . . . . . . . . . . . . . 19
⊢
((Idl‘𝐾) =
{{𝑍}, 𝑋} → ((𝐾 IdlGen {𝑥}) ∈ (Idl‘𝐾) ↔ (𝐾 IdlGen {𝑥}) ∈ {{𝑍}, 𝑋})) |
| 40 | 38, 39 | syl5ibcom 245 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 ∈ RingOps ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → ((Idl‘𝐾) = {{𝑍}, 𝑋} → (𝐾 IdlGen {𝑥}) ∈ {{𝑍}, 𝑋})) |
| 41 | 40 | imp 406 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐾 ∈ RingOps ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) → (𝐾 IdlGen {𝑥}) ∈ {{𝑍}, 𝑋}) |
| 42 | 41 | an32s 652 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐾 ∈ RingOps ∧
(Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (𝐾 IdlGen {𝑥}) ∈ {{𝑍}, 𝑋}) |
| 43 | | ovex 7464 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐾 IdlGen {𝑥}) ∈ V |
| 44 | 43 | elpr 4650 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 IdlGen {𝑥}) ∈ {{𝑍}, 𝑋} ↔ ((𝐾 IdlGen {𝑥}) = {𝑍} ∨ (𝐾 IdlGen {𝑥}) = 𝑋)) |
| 45 | 42, 44 | sylib 218 |
. . . . . . . . . . . . . . 15
⊢ (((𝐾 ∈ RingOps ∧
(Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → ((𝐾 IdlGen {𝑥}) = {𝑍} ∨ (𝐾 IdlGen {𝑥}) = 𝑋)) |
| 46 | 45 | ord 865 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ RingOps ∧
(Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (¬ (𝐾 IdlGen {𝑥}) = {𝑍} → (𝐾 IdlGen {𝑥}) = 𝑋)) |
| 47 | 34, 46 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (((𝐾 ∈ RingOps ∧
(Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (𝐾 IdlGen {𝑥}) = 𝑋) |
| 48 | 13, 47 | sylanl1 680 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ CRingOps ∧
(Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (𝐾 IdlGen {𝑥}) = 𝑋) |
| 49 | 3, 4, 5 | prnc 38074 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ CRingOps ∧ 𝑥 ∈ 𝑋) → (𝐾 IdlGen {𝑥}) = {𝑧 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑧 = (𝑦𝐻𝑥)}) |
| 50 | 35, 49 | sylan2 593 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ CRingOps ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (𝐾 IdlGen {𝑥}) = {𝑧 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑧 = (𝑦𝐻𝑥)}) |
| 51 | 50 | adantlr 715 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ CRingOps ∧
(Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (𝐾 IdlGen {𝑥}) = {𝑧 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑧 = (𝑦𝐻𝑥)}) |
| 52 | 48, 51 | eqtr3d 2779 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ CRingOps ∧
(Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → 𝑋 = {𝑧 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑧 = (𝑦𝐻𝑥)}) |
| 53 | 20, 52 | eleqtrd 2843 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ CRingOps ∧
(Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → 𝑈 ∈ {𝑧 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑧 = (𝑦𝐻𝑥)}) |
| 54 | | eqeq1 2741 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑈 → (𝑧 = (𝑦𝐻𝑥) ↔ 𝑈 = (𝑦𝐻𝑥))) |
| 55 | 54 | rexbidv 3179 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑈 → (∃𝑦 ∈ 𝑋 𝑧 = (𝑦𝐻𝑥) ↔ ∃𝑦 ∈ 𝑋 𝑈 = (𝑦𝐻𝑥))) |
| 56 | 55 | elrab 3692 |
. . . . . . . . . 10
⊢ (𝑈 ∈ {𝑧 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑧 = (𝑦𝐻𝑥)} ↔ (𝑈 ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑋 𝑈 = (𝑦𝐻𝑥))) |
| 57 | 53, 56 | sylib 218 |
. . . . . . . . 9
⊢ (((𝐾 ∈ CRingOps ∧
(Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (𝑈 ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑋 𝑈 = (𝑦𝐻𝑥))) |
| 58 | 57 | simprd 495 |
. . . . . . . 8
⊢ (((𝐾 ∈ CRingOps ∧
(Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → ∃𝑦 ∈ 𝑋 𝑈 = (𝑦𝐻𝑥)) |
| 59 | | eqcom 2744 |
. . . . . . . . 9
⊢ ((𝑦𝐻𝑥) = 𝑈 ↔ 𝑈 = (𝑦𝐻𝑥)) |
| 60 | 59 | rexbii 3094 |
. . . . . . . 8
⊢
(∃𝑦 ∈
𝑋 (𝑦𝐻𝑥) = 𝑈 ↔ ∃𝑦 ∈ 𝑋 𝑈 = (𝑦𝐻𝑥)) |
| 61 | 58, 60 | sylibr 234 |
. . . . . . 7
⊢ (((𝐾 ∈ CRingOps ∧
(Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → ∃𝑦 ∈ 𝑋 (𝑦𝐻𝑥) = 𝑈) |
| 62 | 61 | ralrimiva 3146 |
. . . . . 6
⊢ ((𝐾 ∈ CRingOps ∧
(Idl‘𝐾) = {{𝑍}, 𝑋}) → ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ 𝑋 (𝑦𝐻𝑥) = 𝑈) |
| 63 | 62 | 3adant2 1132 |
. . . . 5
⊢ ((𝐾 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) → ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ 𝑋 (𝑦𝐻𝑥) = 𝑈) |
| 64 | 14, 15, 63 | jca32 515 |
. . . 4
⊢ ((𝐾 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) → (𝐾 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ 𝑋 (𝑦𝐻𝑥) = 𝑈))) |
| 65 | 3, 4, 6, 5, 7 | isdrngo3 37966 |
. . . 4
⊢ (𝐾 ∈ DivRingOps ↔ (𝐾 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ 𝑋 (𝑦𝐻𝑥) = 𝑈))) |
| 66 | 64, 65 | sylibr 234 |
. . 3
⊢ ((𝐾 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) → 𝐾 ∈ DivRingOps) |
| 67 | | simp1 1137 |
. . 3
⊢ ((𝐾 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) → 𝐾 ∈ CRingOps) |
| 68 | | isfld2 38012 |
. . 3
⊢ (𝐾 ∈ Fld ↔ (𝐾 ∈ DivRingOps ∧ 𝐾 ∈
CRingOps)) |
| 69 | 66, 67, 68 | sylanbrc 583 |
. 2
⊢ ((𝐾 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) → 𝐾 ∈ Fld) |
| 70 | 12, 69 | impbii 209 |
1
⊢ (𝐾 ∈ Fld ↔ (𝐾 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝐾) = {{𝑍}, 𝑋})) |