| Step | Hyp | Ref
| Expression |
| 1 | | isdrng4.b |
. . . 4
⊢ 𝐵 = (Base‘𝑅) |
| 2 | | isdrng4.u |
. . . 4
⊢ 𝑈 = (Unit‘𝑅) |
| 3 | | isdrng4.0 |
. . . 4
⊢ 0 =
(0g‘𝑅) |
| 4 | 1, 2, 3 | isdrng 20733 |
. . 3
⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ 𝑈 = (𝐵 ∖ { 0 }))) |
| 5 | | isdrng4.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 6 | 5 | biantrurd 532 |
. . 3
⊢ (𝜑 → (𝑈 = (𝐵 ∖ { 0 }) ↔ (𝑅 ∈ Ring ∧ 𝑈 = (𝐵 ∖ { 0 })))) |
| 7 | 4, 6 | bitr4id 290 |
. 2
⊢ (𝜑 → (𝑅 ∈ DivRing ↔ 𝑈 = (𝐵 ∖ { 0 }))) |
| 8 | | isdrng4.1 |
. . . . . . . . 9
⊢ 1 =
(1r‘𝑅) |
| 9 | 2, 8 | 1unit 20374 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 1 ∈ 𝑈) |
| 10 | 5, 9 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 1 ∈ 𝑈) |
| 11 | 10 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑈 = (𝐵 ∖ { 0 })) → 1 ∈ 𝑈) |
| 12 | | simpr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑈 = (𝐵 ∖ { 0 })) → 𝑈 = (𝐵 ∖ { 0 })) |
| 13 | 11, 12 | eleqtrd 2843 |
. . . . 5
⊢ ((𝜑 ∧ 𝑈 = (𝐵 ∖ { 0 })) → 1 ∈ (𝐵 ∖ { 0 })) |
| 14 | | eldifsni 4790 |
. . . . 5
⊢ ( 1 ∈ (𝐵 ∖ { 0 }) → 1 ≠ 0
) |
| 15 | 13, 14 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑈 = (𝐵 ∖ { 0 })) → 1 ≠ 0
) |
| 16 | | simpll 767 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑈 = (𝐵 ∖ { 0 })) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) → 𝜑) |
| 17 | 12 | eleq2d 2827 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑈 = (𝐵 ∖ { 0 })) → (𝑥 ∈ 𝑈 ↔ 𝑥 ∈ (𝐵 ∖ { 0 }))) |
| 18 | 17 | biimpar 477 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑈 = (𝐵 ∖ { 0 })) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) → 𝑥 ∈ 𝑈) |
| 19 | | isdrng4.x |
. . . . . . . . . . . . 13
⊢ · =
(.r‘𝑅) |
| 20 | 5 | ad5antr 734 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑥) = 1 ) ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 · 𝑧) = 1 ) → 𝑅 ∈ Ring) |
| 21 | 1, 2 | unitcl 20375 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝑈 → 𝑥 ∈ 𝐵) |
| 22 | 21 | ad5antlr 735 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑥) = 1 ) ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 · 𝑧) = 1 ) → 𝑥 ∈ 𝐵) |
| 23 | | simp-4r 784 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑥) = 1 ) ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 · 𝑧) = 1 ) → 𝑦 ∈ 𝐵) |
| 24 | | simplr 769 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑥) = 1 ) ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 · 𝑧) = 1 ) → 𝑧 ∈ 𝐵) |
| 25 | | simpllr 776 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑥) = 1 ) ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 · 𝑧) = 1 ) → (𝑦 · 𝑥) = 1 ) |
| 26 | | simpr 484 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑥) = 1 ) ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 · 𝑧) = 1 ) → (𝑥 · 𝑧) = 1 ) |
| 27 | 1, 3, 8, 19, 2, 20, 22, 23, 24, 25, 26 | ringinveu 33297 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑥) = 1 ) ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 · 𝑧) = 1 ) → 𝑧 = 𝑦) |
| 28 | 27 | oveq2d 7447 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑥) = 1 ) ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 · 𝑧) = 1 ) → (𝑥 · 𝑧) = (𝑥 · 𝑦)) |
| 29 | 28, 26 | eqtr3d 2779 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑥) = 1 ) ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 · 𝑧) = 1 ) → (𝑥 · 𝑦) = 1 ) |
| 30 | 21 | ad3antlr 731 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑥) = 1 ) → 𝑥 ∈ 𝐵) |
| 31 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(∥r‘𝑅) = (∥r‘𝑅) |
| 32 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(oppr‘𝑅) = (oppr‘𝑅) |
| 33 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(∥r‘(oppr‘𝑅)) =
(∥r‘(oppr‘𝑅)) |
| 34 | 2, 8, 31, 32, 33 | isunit 20373 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝑈 ↔ (𝑥(∥r‘𝑅) 1 ∧ 𝑥(∥r‘(oppr‘𝑅)) 1 )) |
| 35 | 34 | simprbi 496 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝑈 → 𝑥(∥r‘(oppr‘𝑅)) 1 ) |
| 36 | 35 | ad3antlr 731 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑥) = 1 ) → 𝑥(∥r‘(oppr‘𝑅)) 1 ) |
| 37 | 32, 1 | opprbas 20341 |
. . . . . . . . . . . . . . 15
⊢ 𝐵 =
(Base‘(oppr‘𝑅)) |
| 38 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(.r‘(oppr‘𝑅)) =
(.r‘(oppr‘𝑅)) |
| 39 | 37, 33, 38 | dvdsr2 20363 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐵 → (𝑥(∥r‘(oppr‘𝑅)) 1 ↔ ∃𝑦 ∈ 𝐵
(𝑦(.r‘(oppr‘𝑅))𝑥) = 1 )) |
| 40 | 39 | biimpa 476 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥(∥r‘(oppr‘𝑅)) 1 ) → ∃𝑦 ∈ 𝐵
(𝑦(.r‘(oppr‘𝑅))𝑥) = 1 ) |
| 41 | 1, 19, 32, 38 | opprmul 20337 |
. . . . . . . . . . . . . . 15
⊢ (𝑦(.r‘(oppr‘𝑅))𝑥) = (𝑥 · 𝑦) |
| 42 | 41 | eqeq1i 2742 |
. . . . . . . . . . . . . 14
⊢ ((𝑦(.r‘(oppr‘𝑅))𝑥) = 1 ↔ (𝑥 · 𝑦) = 1 ) |
| 43 | 42 | rexbii 3094 |
. . . . . . . . . . . . 13
⊢
(∃𝑦 ∈
𝐵 (𝑦(.r‘(oppr‘𝑅))𝑥) = 1 ↔ ∃𝑦 ∈ 𝐵 (𝑥
· 𝑦) = 1 ) |
| 44 | 40, 43 | sylib 218 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥(∥r‘(oppr‘𝑅)) 1 ) → ∃𝑦 ∈ 𝐵
(𝑥 · 𝑦) = 1 ) |
| 45 | | oveq2 7439 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑧 → (𝑥 · 𝑦) = (𝑥 · 𝑧)) |
| 46 | 45 | eqeq1d 2739 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑧 → ((𝑥 · 𝑦) = 1 ↔ (𝑥 · 𝑧) = 1 )) |
| 47 | 46 | cbvrexvw 3238 |
. . . . . . . . . . . 12
⊢
(∃𝑦 ∈
𝐵 (𝑥 · 𝑦) = 1 ↔ ∃𝑧 ∈ 𝐵 (𝑥 · 𝑧) = 1 ) |
| 48 | 44, 47 | sylib 218 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥(∥r‘(oppr‘𝑅)) 1 ) → ∃𝑧 ∈ 𝐵
(𝑥 · 𝑧) = 1 ) |
| 49 | 30, 36, 48 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑥) = 1 ) → ∃𝑧 ∈ 𝐵 (𝑥 · 𝑧) = 1 ) |
| 50 | 29, 49 | r19.29a 3162 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑥) = 1 ) → (𝑥 · 𝑦) = 1 ) |
| 51 | | simpr 484 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑥) = 1 ) → (𝑦 · 𝑥) = 1 ) |
| 52 | 50, 51 | jca 511 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑈) ∧ 𝑦 ∈ 𝐵) ∧ (𝑦 · 𝑥) = 1 ) → ((𝑥 · 𝑦) = 1 ∧ (𝑦 · 𝑥) = 1 )) |
| 53 | 52 | anasss 466 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑈) ∧ (𝑦 ∈ 𝐵 ∧ (𝑦 · 𝑥) = 1 )) → ((𝑥 · 𝑦) = 1 ∧ (𝑦 · 𝑥) = 1 )) |
| 54 | 21 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → 𝑥 ∈ 𝐵) |
| 55 | 34 | simplbi 497 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑈 → 𝑥(∥r‘𝑅) 1 ) |
| 56 | 55 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → 𝑥(∥r‘𝑅) 1 ) |
| 57 | 1, 31, 19 | dvdsr2 20363 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐵 → (𝑥(∥r‘𝑅) 1 ↔ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑥) = 1 )) |
| 58 | 57 | biimpa 476 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥(∥r‘𝑅) 1 ) → ∃𝑦 ∈ 𝐵 (𝑦 · 𝑥) = 1 ) |
| 59 | 54, 56, 58 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → ∃𝑦 ∈ 𝐵 (𝑦 · 𝑥) = 1 ) |
| 60 | 53, 59 | reximddv 3171 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → ∃𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 1 ∧ (𝑦 · 𝑥) = 1 )) |
| 61 | 16, 18, 60 | syl2anc 584 |
. . . . 5
⊢ (((𝜑 ∧ 𝑈 = (𝐵 ∖ { 0 })) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) → ∃𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 1 ∧ (𝑦 · 𝑥) = 1 )) |
| 62 | 61 | ralrimiva 3146 |
. . . 4
⊢ ((𝜑 ∧ 𝑈 = (𝐵 ∖ { 0 })) → ∀𝑥 ∈ (𝐵 ∖ { 0 })∃𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 1 ∧ (𝑦 · 𝑥) = 1 )) |
| 63 | 15, 62 | jca 511 |
. . 3
⊢ ((𝜑 ∧ 𝑈 = (𝐵 ∖ { 0 })) → ( 1 ≠ 0 ∧
∀𝑥 ∈ (𝐵 ∖ { 0 })∃𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 1 ∧ (𝑦 · 𝑥) = 1 ))) |
| 64 | 1, 2 | unitss 20376 |
. . . . . 6
⊢ 𝑈 ⊆ 𝐵 |
| 65 | 64 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ ( 1 ≠ 0 ∧ ∀𝑥 ∈ (𝐵 ∖ { 0 })∃𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 1 ∧ (𝑦 · 𝑥) = 1 ))) → 𝑈 ⊆ 𝐵) |
| 66 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ( 1 ≠ 0 ∧ ∀𝑥 ∈ (𝐵 ∖ { 0 })∃𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 1 ∧ (𝑦 · 𝑥) = 1 ))) → 𝑅 ∈ Ring) |
| 67 | | simprl 771 |
. . . . . 6
⊢ ((𝜑 ∧ ( 1 ≠ 0 ∧ ∀𝑥 ∈ (𝐵 ∖ { 0 })∃𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 1 ∧ (𝑦 · 𝑥) = 1 ))) → 1 ≠ 0
) |
| 68 | 2, 3, 8 | 0unit 20396 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → ( 0 ∈ 𝑈 ↔ 1 = 0 )) |
| 69 | 68 | necon3bbid 2978 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → (¬ 0 ∈ 𝑈 ↔ 1 ≠ 0 )) |
| 70 | 69 | biimpar 477 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 1 ≠ 0 ) →
¬ 0
∈ 𝑈) |
| 71 | 66, 67, 70 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ ( 1 ≠ 0 ∧ ∀𝑥 ∈ (𝐵 ∖ { 0 })∃𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 1 ∧ (𝑦 · 𝑥) = 1 ))) → ¬ 0 ∈ 𝑈) |
| 72 | | ssdifsn 4788 |
. . . . 5
⊢ (𝑈 ⊆ (𝐵 ∖ { 0 }) ↔ (𝑈 ⊆ 𝐵 ∧ ¬ 0 ∈ 𝑈)) |
| 73 | 65, 71, 72 | sylanbrc 583 |
. . . 4
⊢ ((𝜑 ∧ ( 1 ≠ 0 ∧ ∀𝑥 ∈ (𝐵 ∖ { 0 })∃𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 1 ∧ (𝑦 · 𝑥) = 1 ))) → 𝑈 ⊆ (𝐵 ∖ { 0 })) |
| 74 | | simplr 769 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 1 ≠ 0 ) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) ∧ ∃𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 1 ∧ (𝑦 · 𝑥) = 1 )) → 𝑥 ∈ (𝐵 ∖ { 0 })) |
| 75 | 74 | eldifad 3963 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 1 ≠ 0 ) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) ∧ ∃𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 1 ∧ (𝑦 · 𝑥) = 1 )) → 𝑥 ∈ 𝐵) |
| 76 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝑥 · 𝑦) = 1 ∧ (𝑦 · 𝑥) = 1 ) → (𝑦 · 𝑥) = 1 ) |
| 77 | 76 | reximi 3084 |
. . . . . . . . . . 11
⊢
(∃𝑦 ∈
𝐵 ((𝑥 · 𝑦) = 1 ∧ (𝑦 · 𝑥) = 1 ) → ∃𝑦 ∈ 𝐵 (𝑦 · 𝑥) = 1 ) |
| 78 | 77 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 1 ≠ 0 ) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) ∧ ∃𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 1 ∧ (𝑦 · 𝑥) = 1 )) → ∃𝑦 ∈ 𝐵 (𝑦 · 𝑥) = 1 ) |
| 79 | 57 | biimpar 477 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐵 (𝑦 · 𝑥) = 1 ) → 𝑥(∥r‘𝑅) 1 ) |
| 80 | 75, 78, 79 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 1 ≠ 0 ) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) ∧ ∃𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 1 ∧ (𝑦 · 𝑥) = 1 )) → 𝑥(∥r‘𝑅) 1 ) |
| 81 | | simpl 482 |
. . . . . . . . . . . . 13
⊢ (((𝑥 · 𝑦) = 1 ∧ (𝑦 · 𝑥) = 1 ) → (𝑥 · 𝑦) = 1 ) |
| 82 | 81 | reximi 3084 |
. . . . . . . . . . . 12
⊢
(∃𝑦 ∈
𝐵 ((𝑥 · 𝑦) = 1 ∧ (𝑦 · 𝑥) = 1 ) → ∃𝑦 ∈ 𝐵 (𝑥 · 𝑦) = 1 ) |
| 83 | 82 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 1 ≠ 0 ) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) ∧ ∃𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 1 ∧ (𝑦 · 𝑥) = 1 )) → ∃𝑦 ∈ 𝐵 (𝑥 · 𝑦) = 1 ) |
| 84 | 83, 43 | sylibr 234 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 1 ≠ 0 ) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) ∧ ∃𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 1 ∧ (𝑦 · 𝑥) = 1 )) → ∃𝑦 ∈ 𝐵 (𝑦(.r‘(oppr‘𝑅))𝑥) = 1 ) |
| 85 | 39 | biimpar 477 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝐵 (𝑦(.r‘(oppr‘𝑅))𝑥) = 1 ) → 𝑥(∥r‘(oppr‘𝑅)) 1 ) |
| 86 | 75, 84, 85 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 1 ≠ 0 ) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) ∧ ∃𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 1 ∧ (𝑦 · 𝑥) = 1 )) → 𝑥(∥r‘(oppr‘𝑅)) 1 ) |
| 87 | 80, 86, 34 | sylanbrc 583 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 1 ≠ 0 ) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) ∧ ∃𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 1 ∧ (𝑦 · 𝑥) = 1 )) → 𝑥 ∈ 𝑈) |
| 88 | 87 | ex 412 |
. . . . . . 7
⊢ (((𝜑 ∧ 1 ≠ 0 ) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) → (∃𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 1 ∧ (𝑦 · 𝑥) = 1 ) → 𝑥 ∈ 𝑈)) |
| 89 | 88 | ralimdva 3167 |
. . . . . 6
⊢ ((𝜑 ∧ 1 ≠ 0 ) → (∀𝑥 ∈ (𝐵 ∖ { 0 })∃𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 1 ∧ (𝑦 · 𝑥) = 1 ) → ∀𝑥 ∈ (𝐵 ∖ { 0 })𝑥 ∈ 𝑈)) |
| 90 | 89 | impr 454 |
. . . . 5
⊢ ((𝜑 ∧ ( 1 ≠ 0 ∧ ∀𝑥 ∈ (𝐵 ∖ { 0 })∃𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 1 ∧ (𝑦 · 𝑥) = 1 ))) → ∀𝑥 ∈ (𝐵 ∖ { 0 })𝑥 ∈ 𝑈) |
| 91 | | dfss3 3972 |
. . . . 5
⊢ ((𝐵 ∖ { 0 }) ⊆ 𝑈 ↔ ∀𝑥 ∈ (𝐵 ∖ { 0 })𝑥 ∈ 𝑈) |
| 92 | 90, 91 | sylibr 234 |
. . . 4
⊢ ((𝜑 ∧ ( 1 ≠ 0 ∧ ∀𝑥 ∈ (𝐵 ∖ { 0 })∃𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 1 ∧ (𝑦 · 𝑥) = 1 ))) → (𝐵 ∖ { 0 }) ⊆ 𝑈) |
| 93 | 73, 92 | eqssd 4001 |
. . 3
⊢ ((𝜑 ∧ ( 1 ≠ 0 ∧ ∀𝑥 ∈ (𝐵 ∖ { 0 })∃𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 1 ∧ (𝑦 · 𝑥) = 1 ))) → 𝑈 = (𝐵 ∖ { 0 })) |
| 94 | 63, 93 | impbida 801 |
. 2
⊢ (𝜑 → (𝑈 = (𝐵 ∖ { 0 }) ↔ ( 1 ≠ 0 ∧
∀𝑥 ∈ (𝐵 ∖ { 0 })∃𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 1 ∧ (𝑦 · 𝑥) = 1 )))) |
| 95 | 7, 94 | bitrd 279 |
1
⊢ (𝜑 → (𝑅 ∈ DivRing ↔ ( 1 ≠ 0 ∧ ∀𝑥 ∈ (𝐵 ∖ { 0 })∃𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 1 ∧ (𝑦 · 𝑥) = 1 )))) |