| Step | Hyp | Ref
| Expression |
| 1 | | imadrhmcl.h |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (𝑀 RingHom 𝑁)) |
| 2 | | imadrhmcl.s |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ (SubDRing‘𝑀)) |
| 3 | | sdrgsubrg 20792 |
. . . . 5
⊢ (𝑆 ∈ (SubDRing‘𝑀) → 𝑆 ∈ (SubRing‘𝑀)) |
| 4 | 2, 3 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑀)) |
| 5 | | rhmima 20604 |
. . . 4
⊢ ((𝐹 ∈ (𝑀 RingHom 𝑁) ∧ 𝑆 ∈ (SubRing‘𝑀)) → (𝐹 “ 𝑆) ∈ (SubRing‘𝑁)) |
| 6 | 1, 4, 5 | syl2anc 584 |
. . 3
⊢ (𝜑 → (𝐹 “ 𝑆) ∈ (SubRing‘𝑁)) |
| 7 | | imadrhmcl.r |
. . . 4
⊢ 𝑅 = (𝑁 ↾s (𝐹 “ 𝑆)) |
| 8 | 7 | subrgring 20574 |
. . 3
⊢ ((𝐹 “ 𝑆) ∈ (SubRing‘𝑁) → 𝑅 ∈ Ring) |
| 9 | 6, 8 | syl 17 |
. 2
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 10 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 11 | | eqid 2737 |
. . . . . 6
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
| 12 | 10, 11 | unitss 20376 |
. . . . 5
⊢
(Unit‘𝑅)
⊆ (Base‘𝑅) |
| 13 | 12 | a1i 11 |
. . . 4
⊢ (𝜑 → (Unit‘𝑅) ⊆ (Base‘𝑅)) |
| 14 | | imadrhmcl.1 |
. . . . . 6
⊢ (𝜑 → ran 𝐹 ≠ { 0 }) |
| 15 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(Base‘𝑀) =
(Base‘𝑀) |
| 16 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(Base‘𝑁) =
(Base‘𝑁) |
| 17 | 15, 16 | rhmf 20485 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (𝑀 RingHom 𝑁) → 𝐹:(Base‘𝑀)⟶(Base‘𝑁)) |
| 18 | 1, 17 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:(Base‘𝑀)⟶(Base‘𝑁)) |
| 19 | 18 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (1r‘𝑅) = (0g‘𝑅)) → 𝐹:(Base‘𝑀)⟶(Base‘𝑁)) |
| 20 | | rhmrcl2 20477 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (𝑀 RingHom 𝑁) → 𝑁 ∈ Ring) |
| 21 | 1, 20 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ Ring) |
| 22 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (1r‘𝑅) = (0g‘𝑅)) →
(1r‘𝑅) =
(0g‘𝑅)) |
| 23 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(1r‘𝑁) = (1r‘𝑁) |
| 24 | 7, 23 | subrg1 20582 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 “ 𝑆) ∈ (SubRing‘𝑁) → (1r‘𝑁) = (1r‘𝑅)) |
| 25 | 6, 24 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1r‘𝑁) = (1r‘𝑅)) |
| 26 | 25 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (1r‘𝑅) = (0g‘𝑅)) →
(1r‘𝑁) =
(1r‘𝑅)) |
| 27 | | imadrhmcl.0 |
. . . . . . . . . . . . . . 15
⊢ 0 =
(0g‘𝑁) |
| 28 | 7, 27 | subrg0 20579 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 “ 𝑆) ∈ (SubRing‘𝑁) → 0 =
(0g‘𝑅)) |
| 29 | 6, 28 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 =
(0g‘𝑅)) |
| 30 | 29 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (1r‘𝑅) = (0g‘𝑅)) → 0 =
(0g‘𝑅)) |
| 31 | 22, 26, 30 | 3eqtr4rd 2788 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (1r‘𝑅) = (0g‘𝑅)) → 0 =
(1r‘𝑁)) |
| 32 | 16, 27, 23 | 01eq0ring 20530 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Ring ∧ 0 =
(1r‘𝑁))
→ (Base‘𝑁) = {
0
}) |
| 33 | 21, 31, 32 | syl2an2r 685 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (1r‘𝑅) = (0g‘𝑅)) → (Base‘𝑁) = { 0 }) |
| 34 | 33 | feq3d 6723 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (1r‘𝑅) = (0g‘𝑅)) → (𝐹:(Base‘𝑀)⟶(Base‘𝑁) ↔ 𝐹:(Base‘𝑀)⟶{ 0 })) |
| 35 | 19, 34 | mpbid 232 |
. . . . . . . 8
⊢ ((𝜑 ∧ (1r‘𝑅) = (0g‘𝑅)) → 𝐹:(Base‘𝑀)⟶{ 0 }) |
| 36 | 27 | fvexi 6920 |
. . . . . . . . 9
⊢ 0 ∈
V |
| 37 | 36 | fconst2 7225 |
. . . . . . . 8
⊢ (𝐹:(Base‘𝑀)⟶{ 0 } ↔ 𝐹 = ((Base‘𝑀) × { 0 })) |
| 38 | 35, 37 | sylib 218 |
. . . . . . 7
⊢ ((𝜑 ∧ (1r‘𝑅) = (0g‘𝑅)) → 𝐹 = ((Base‘𝑀) × { 0 })) |
| 39 | 18 | ffnd 6737 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 Fn (Base‘𝑀)) |
| 40 | | sdrgrcl 20790 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ (SubDRing‘𝑀) → 𝑀 ∈ DivRing) |
| 41 | 2, 40 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ DivRing) |
| 42 | 41 | drngringd 20737 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ Ring) |
| 43 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(0g‘𝑀) = (0g‘𝑀) |
| 44 | 15, 43 | ring0cl 20264 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ Ring →
(0g‘𝑀)
∈ (Base‘𝑀)) |
| 45 | 42, 44 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (0g‘𝑀) ∈ (Base‘𝑀)) |
| 46 | 45 | ne0d 4342 |
. . . . . . . . 9
⊢ (𝜑 → (Base‘𝑀) ≠ ∅) |
| 47 | | fconst5 7226 |
. . . . . . . . 9
⊢ ((𝐹 Fn (Base‘𝑀) ∧ (Base‘𝑀) ≠ ∅) → (𝐹 = ((Base‘𝑀) × { 0 }) ↔ ran 𝐹 = { 0 })) |
| 48 | 39, 46, 47 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 = ((Base‘𝑀) × { 0 }) ↔ ran 𝐹 = { 0 })) |
| 49 | 48 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (1r‘𝑅) = (0g‘𝑅)) → (𝐹 = ((Base‘𝑀) × { 0 }) ↔ ran 𝐹 = { 0 })) |
| 50 | 38, 49 | mpbid 232 |
. . . . . 6
⊢ ((𝜑 ∧ (1r‘𝑅) = (0g‘𝑅)) → ran 𝐹 = { 0 }) |
| 51 | 14, 50 | mteqand 3033 |
. . . . 5
⊢ (𝜑 → (1r‘𝑅) ≠
(0g‘𝑅)) |
| 52 | | eqid 2737 |
. . . . . . . 8
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 53 | | eqid 2737 |
. . . . . . . 8
⊢
(1r‘𝑅) = (1r‘𝑅) |
| 54 | 11, 52, 53 | 0unit 20396 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
((0g‘𝑅)
∈ (Unit‘𝑅)
↔ (1r‘𝑅) = (0g‘𝑅))) |
| 55 | 9, 54 | syl 17 |
. . . . . 6
⊢ (𝜑 →
((0g‘𝑅)
∈ (Unit‘𝑅)
↔ (1r‘𝑅) = (0g‘𝑅))) |
| 56 | 55 | necon3bbid 2978 |
. . . . 5
⊢ (𝜑 → (¬
(0g‘𝑅)
∈ (Unit‘𝑅)
↔ (1r‘𝑅) ≠ (0g‘𝑅))) |
| 57 | 51, 56 | mpbird 257 |
. . . 4
⊢ (𝜑 → ¬
(0g‘𝑅)
∈ (Unit‘𝑅)) |
| 58 | | ssdifsn 4788 |
. . . 4
⊢
((Unit‘𝑅)
⊆ ((Base‘𝑅)
∖ {(0g‘𝑅)}) ↔ ((Unit‘𝑅) ⊆ (Base‘𝑅) ∧ ¬ (0g‘𝑅) ∈ (Unit‘𝑅))) |
| 59 | 13, 57, 58 | sylanbrc 583 |
. . 3
⊢ (𝜑 → (Unit‘𝑅) ⊆ ((Base‘𝑅) ∖
{(0g‘𝑅)})) |
| 60 | 39 | fnfund 6669 |
. . . . 5
⊢ (𝜑 → Fun 𝐹) |
| 61 | 7 | ressbasss2 17286 |
. . . . . 6
⊢
(Base‘𝑅)
⊆ (𝐹 “ 𝑆) |
| 62 | | eldifi 4131 |
. . . . . 6
⊢ (𝑥 ∈ ((Base‘𝑅) ∖
{(0g‘𝑅)})
→ 𝑥 ∈
(Base‘𝑅)) |
| 63 | 61, 62 | sselid 3981 |
. . . . 5
⊢ (𝑥 ∈ ((Base‘𝑅) ∖
{(0g‘𝑅)})
→ 𝑥 ∈ (𝐹 “ 𝑆)) |
| 64 | | fvelima 6974 |
. . . . 5
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ (𝐹 “ 𝑆)) → ∃𝑎 ∈ 𝑆 (𝐹‘𝑎) = 𝑥) |
| 65 | 60, 63, 64 | syl2an 596 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) → ∃𝑎 ∈ 𝑆 (𝐹‘𝑎) = 𝑥) |
| 66 | | simprr 773 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) → (𝐹‘𝑎) = 𝑥) |
| 67 | | simprl 771 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) → 𝑎 ∈ 𝑆) |
| 68 | 67 | fvresd 6926 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) → ((𝐹 ↾ 𝑆)‘𝑎) = (𝐹‘𝑎)) |
| 69 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑀 ↾s 𝑆) = (𝑀 ↾s 𝑆) |
| 70 | 69 | resrhm 20601 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (𝑀 RingHom 𝑁) ∧ 𝑆 ∈ (SubRing‘𝑀)) → (𝐹 ↾ 𝑆) ∈ ((𝑀 ↾s 𝑆) RingHom 𝑁)) |
| 71 | 1, 4, 70 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 ↾ 𝑆) ∈ ((𝑀 ↾s 𝑆) RingHom 𝑁)) |
| 72 | | df-ima 5698 |
. . . . . . . . . . 11
⊢ (𝐹 “ 𝑆) = ran (𝐹 ↾ 𝑆) |
| 73 | | eqimss2 4043 |
. . . . . . . . . . 11
⊢ ((𝐹 “ 𝑆) = ran (𝐹 ↾ 𝑆) → ran (𝐹 ↾ 𝑆) ⊆ (𝐹 “ 𝑆)) |
| 74 | 72, 73 | mp1i 13 |
. . . . . . . . . 10
⊢ (𝜑 → ran (𝐹 ↾ 𝑆) ⊆ (𝐹 “ 𝑆)) |
| 75 | 7 | resrhm2b 20602 |
. . . . . . . . . 10
⊢ (((𝐹 “ 𝑆) ∈ (SubRing‘𝑁) ∧ ran (𝐹 ↾ 𝑆) ⊆ (𝐹 “ 𝑆)) → ((𝐹 ↾ 𝑆) ∈ ((𝑀 ↾s 𝑆) RingHom 𝑁) ↔ (𝐹 ↾ 𝑆) ∈ ((𝑀 ↾s 𝑆) RingHom 𝑅))) |
| 76 | 6, 74, 75 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹 ↾ 𝑆) ∈ ((𝑀 ↾s 𝑆) RingHom 𝑁) ↔ (𝐹 ↾ 𝑆) ∈ ((𝑀 ↾s 𝑆) RingHom 𝑅))) |
| 77 | 71, 76 | mpbid 232 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ↾ 𝑆) ∈ ((𝑀 ↾s 𝑆) RingHom 𝑅)) |
| 78 | 77 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) → (𝐹 ↾ 𝑆) ∈ ((𝑀 ↾s 𝑆) RingHom 𝑅)) |
| 79 | | eldifsni 4790 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ((Base‘𝑅) ∖
{(0g‘𝑅)})
→ 𝑥 ≠
(0g‘𝑅)) |
| 80 | 79 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) → 𝑥 ≠ (0g‘𝑅)) |
| 81 | 68 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) ∧ 𝑎 = (0g‘𝑀)) → ((𝐹 ↾ 𝑆)‘𝑎) = (𝐹‘𝑎)) |
| 82 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) ∧ 𝑎 = (0g‘𝑀)) → 𝑎 = (0g‘𝑀)) |
| 83 | 82 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) ∧ 𝑎 = (0g‘𝑀)) → ((𝐹 ↾ 𝑆)‘𝑎) = ((𝐹 ↾ 𝑆)‘(0g‘𝑀))) |
| 84 | 69, 43 | subrg0 20579 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 ∈ (SubRing‘𝑀) →
(0g‘𝑀) =
(0g‘(𝑀
↾s 𝑆))) |
| 85 | 4, 84 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0g‘𝑀) = (0g‘(𝑀 ↾s 𝑆))) |
| 86 | 85 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐹 ↾ 𝑆)‘(0g‘𝑀)) = ((𝐹 ↾ 𝑆)‘(0g‘(𝑀 ↾s 𝑆)))) |
| 87 | | rhmghm 20484 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ↾ 𝑆) ∈ ((𝑀 ↾s 𝑆) RingHom 𝑅) → (𝐹 ↾ 𝑆) ∈ ((𝑀 ↾s 𝑆) GrpHom 𝑅)) |
| 88 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(0g‘(𝑀 ↾s 𝑆)) = (0g‘(𝑀 ↾s 𝑆)) |
| 89 | 88, 52 | ghmid 19240 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ↾ 𝑆) ∈ ((𝑀 ↾s 𝑆) GrpHom 𝑅) → ((𝐹 ↾ 𝑆)‘(0g‘(𝑀 ↾s 𝑆))) = (0g‘𝑅)) |
| 90 | 77, 87, 89 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐹 ↾ 𝑆)‘(0g‘(𝑀 ↾s 𝑆))) = (0g‘𝑅)) |
| 91 | 86, 90 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐹 ↾ 𝑆)‘(0g‘𝑀)) = (0g‘𝑅)) |
| 92 | 91 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) ∧ 𝑎 = (0g‘𝑀)) → ((𝐹 ↾ 𝑆)‘(0g‘𝑀)) = (0g‘𝑅)) |
| 93 | 83, 92 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) ∧ 𝑎 = (0g‘𝑀)) → ((𝐹 ↾ 𝑆)‘𝑎) = (0g‘𝑅)) |
| 94 | | simplrr 778 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) ∧ 𝑎 = (0g‘𝑀)) → (𝐹‘𝑎) = 𝑥) |
| 95 | 81, 93, 94 | 3eqtr3rd 2786 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) ∧ 𝑎 = (0g‘𝑀)) → 𝑥 = (0g‘𝑅)) |
| 96 | 80, 95 | mteqand 3033 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) → 𝑎 ≠ (0g‘𝑀)) |
| 97 | 2 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) → 𝑆 ∈ (SubDRing‘𝑀)) |
| 98 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Unit‘(𝑀
↾s 𝑆)) =
(Unit‘(𝑀
↾s 𝑆)) |
| 99 | 69, 43, 98 | sdrgunit 20797 |
. . . . . . . . 9
⊢ (𝑆 ∈ (SubDRing‘𝑀) → (𝑎 ∈ (Unit‘(𝑀 ↾s 𝑆)) ↔ (𝑎 ∈ 𝑆 ∧ 𝑎 ≠ (0g‘𝑀)))) |
| 100 | 97, 99 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) → (𝑎 ∈ (Unit‘(𝑀 ↾s 𝑆)) ↔ (𝑎 ∈ 𝑆 ∧ 𝑎 ≠ (0g‘𝑀)))) |
| 101 | 67, 96, 100 | mpbir2and 713 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) → 𝑎 ∈ (Unit‘(𝑀 ↾s 𝑆))) |
| 102 | | elrhmunit 20510 |
. . . . . . 7
⊢ (((𝐹 ↾ 𝑆) ∈ ((𝑀 ↾s 𝑆) RingHom 𝑅) ∧ 𝑎 ∈ (Unit‘(𝑀 ↾s 𝑆))) → ((𝐹 ↾ 𝑆)‘𝑎) ∈ (Unit‘𝑅)) |
| 103 | 78, 101, 102 | syl2anc 584 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) → ((𝐹 ↾ 𝑆)‘𝑎) ∈ (Unit‘𝑅)) |
| 104 | 68, 103 | eqeltrrd 2842 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) → (𝐹‘𝑎) ∈ (Unit‘𝑅)) |
| 105 | 66, 104 | eqeltrrd 2842 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) → 𝑥 ∈ (Unit‘𝑅)) |
| 106 | 65, 105 | rexlimddv 3161 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) → 𝑥 ∈ (Unit‘𝑅)) |
| 107 | 59, 106 | eqelssd 4005 |
. 2
⊢ (𝜑 → (Unit‘𝑅) = ((Base‘𝑅) ∖
{(0g‘𝑅)})) |
| 108 | 10, 11, 52 | isdrng 20733 |
. 2
⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧
(Unit‘𝑅) =
((Base‘𝑅) ∖
{(0g‘𝑅)}))) |
| 109 | 9, 107, 108 | sylanbrc 583 |
1
⊢ (𝜑 → 𝑅 ∈ DivRing) |