Step | Hyp | Ref
| Expression |
1 | | imadrhmcl.h |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (𝑀 RingHom 𝑁)) |
2 | | imadrhmcl.s |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ (SubDRing‘𝑀)) |
3 | | sdrgsubrg 20672 |
. . . . 5
⊢ (𝑆 ∈ (SubDRing‘𝑀) → 𝑆 ∈ (SubRing‘𝑀)) |
4 | 2, 3 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑀)) |
5 | | rhmima 20536 |
. . . 4
⊢ ((𝐹 ∈ (𝑀 RingHom 𝑁) ∧ 𝑆 ∈ (SubRing‘𝑀)) → (𝐹 “ 𝑆) ∈ (SubRing‘𝑁)) |
6 | 1, 4, 5 | syl2anc 583 |
. . 3
⊢ (𝜑 → (𝐹 “ 𝑆) ∈ (SubRing‘𝑁)) |
7 | | imadrhmcl.r |
. . . 4
⊢ 𝑅 = (𝑁 ↾s (𝐹 “ 𝑆)) |
8 | 7 | subrgring 20506 |
. . 3
⊢ ((𝐹 “ 𝑆) ∈ (SubRing‘𝑁) → 𝑅 ∈ Ring) |
9 | 6, 8 | syl 17 |
. 2
⊢ (𝜑 → 𝑅 ∈ Ring) |
10 | | eqid 2727 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) |
11 | | eqid 2727 |
. . . . . 6
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
12 | 10, 11 | unitss 20308 |
. . . . 5
⊢
(Unit‘𝑅)
⊆ (Base‘𝑅) |
13 | 12 | a1i 11 |
. . . 4
⊢ (𝜑 → (Unit‘𝑅) ⊆ (Base‘𝑅)) |
14 | | imadrhmcl.1 |
. . . . . 6
⊢ (𝜑 → ran 𝐹 ≠ { 0 }) |
15 | | eqid 2727 |
. . . . . . . . . . . 12
⊢
(Base‘𝑀) =
(Base‘𝑀) |
16 | | eqid 2727 |
. . . . . . . . . . . 12
⊢
(Base‘𝑁) =
(Base‘𝑁) |
17 | 15, 16 | rhmf 20417 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (𝑀 RingHom 𝑁) → 𝐹:(Base‘𝑀)⟶(Base‘𝑁)) |
18 | 1, 17 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:(Base‘𝑀)⟶(Base‘𝑁)) |
19 | 18 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (1r‘𝑅) = (0g‘𝑅)) → 𝐹:(Base‘𝑀)⟶(Base‘𝑁)) |
20 | | rhmrcl2 20409 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (𝑀 RingHom 𝑁) → 𝑁 ∈ Ring) |
21 | 1, 20 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ Ring) |
22 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (1r‘𝑅) = (0g‘𝑅)) →
(1r‘𝑅) =
(0g‘𝑅)) |
23 | | eqid 2727 |
. . . . . . . . . . . . . . 15
⊢
(1r‘𝑁) = (1r‘𝑁) |
24 | 7, 23 | subrg1 20514 |
. . . . . . . . . . . . . 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 20511 |
. . . . . . . . . . . . . 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 2778 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (1r‘𝑅) = (0g‘𝑅)) → 0 =
(1r‘𝑁)) |
32 | 16, 27, 23 | 01eq0ring 20460 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Ring ∧ 0 =
(1r‘𝑁))
→ (Base‘𝑁) = {
0
}) |
33 | 21, 31, 32 | syl2an2r 684 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (1r‘𝑅) = (0g‘𝑅)) → (Base‘𝑁) = { 0 }) |
34 | 33 | feq3d 6703 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (1r‘𝑅) = (0g‘𝑅)) → (𝐹:(Base‘𝑀)⟶(Base‘𝑁) ↔ 𝐹:(Base‘𝑀)⟶{ 0 })) |
35 | 19, 34 | mpbid 231 |
. . . . . . . 8
⊢ ((𝜑 ∧ (1r‘𝑅) = (0g‘𝑅)) → 𝐹:(Base‘𝑀)⟶{ 0 }) |
36 | 27 | fvexi 6905 |
. . . . . . . . 9
⊢ 0 ∈
V |
37 | 36 | fconst2 7211 |
. . . . . . . 8
⊢ (𝐹:(Base‘𝑀)⟶{ 0 } ↔ 𝐹 = ((Base‘𝑀) × { 0 })) |
38 | 35, 37 | sylib 217 |
. . . . . . 7
⊢ ((𝜑 ∧ (1r‘𝑅) = (0g‘𝑅)) → 𝐹 = ((Base‘𝑀) × { 0 })) |
39 | 18 | ffnd 6717 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 Fn (Base‘𝑀)) |
40 | | sdrgrcl 20670 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ (SubDRing‘𝑀) → 𝑀 ∈ DivRing) |
41 | 2, 40 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ DivRing) |
42 | 41 | drngringd 20625 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ Ring) |
43 | | eqid 2727 |
. . . . . . . . . . . 12
⊢
(0g‘𝑀) = (0g‘𝑀) |
44 | 15, 43 | ring0cl 20196 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ Ring →
(0g‘𝑀)
∈ (Base‘𝑀)) |
45 | 42, 44 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (0g‘𝑀) ∈ (Base‘𝑀)) |
46 | 45 | ne0d 4331 |
. . . . . . . . 9
⊢ (𝜑 → (Base‘𝑀) ≠ ∅) |
47 | | fconst5 7212 |
. . . . . . . . 9
⊢ ((𝐹 Fn (Base‘𝑀) ∧ (Base‘𝑀) ≠ ∅) → (𝐹 = ((Base‘𝑀) × { 0 }) ↔ ran 𝐹 = { 0 })) |
48 | 39, 46, 47 | syl2anc 583 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 = ((Base‘𝑀) × { 0 }) ↔ ran 𝐹 = { 0 })) |
49 | 48 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (1r‘𝑅) = (0g‘𝑅)) → (𝐹 = ((Base‘𝑀) × { 0 }) ↔ ran 𝐹 = { 0 })) |
50 | 38, 49 | mpbid 231 |
. . . . . 6
⊢ ((𝜑 ∧ (1r‘𝑅) = (0g‘𝑅)) → ran 𝐹 = { 0 }) |
51 | 14, 50 | mteqand 3028 |
. . . . 5
⊢ (𝜑 → (1r‘𝑅) ≠
(0g‘𝑅)) |
52 | | eqid 2727 |
. . . . . . . 8
⊢
(0g‘𝑅) = (0g‘𝑅) |
53 | | eqid 2727 |
. . . . . . . 8
⊢
(1r‘𝑅) = (1r‘𝑅) |
54 | 11, 52, 53 | 0unit 20328 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
((0g‘𝑅)
∈ (Unit‘𝑅)
↔ (1r‘𝑅) = (0g‘𝑅))) |
55 | 9, 54 | syl 17 |
. . . . . 6
⊢ (𝜑 →
((0g‘𝑅)
∈ (Unit‘𝑅)
↔ (1r‘𝑅) = (0g‘𝑅))) |
56 | 55 | necon3bbid 2973 |
. . . . 5
⊢ (𝜑 → (¬
(0g‘𝑅)
∈ (Unit‘𝑅)
↔ (1r‘𝑅) ≠ (0g‘𝑅))) |
57 | 51, 56 | mpbird 257 |
. . . 4
⊢ (𝜑 → ¬
(0g‘𝑅)
∈ (Unit‘𝑅)) |
58 | | ssdifsn 4787 |
. . . 4
⊢
((Unit‘𝑅)
⊆ ((Base‘𝑅)
∖ {(0g‘𝑅)}) ↔ ((Unit‘𝑅) ⊆ (Base‘𝑅) ∧ ¬ (0g‘𝑅) ∈ (Unit‘𝑅))) |
59 | 13, 57, 58 | sylanbrc 582 |
. . 3
⊢ (𝜑 → (Unit‘𝑅) ⊆ ((Base‘𝑅) ∖
{(0g‘𝑅)})) |
60 | 39 | fnfund 6649 |
. . . . 5
⊢ (𝜑 → Fun 𝐹) |
61 | 7 | ressbasss2 17214 |
. . . . . 6
⊢
(Base‘𝑅)
⊆ (𝐹 “ 𝑆) |
62 | | eldifi 4122 |
. . . . . 6
⊢ (𝑥 ∈ ((Base‘𝑅) ∖
{(0g‘𝑅)})
→ 𝑥 ∈
(Base‘𝑅)) |
63 | 61, 62 | sselid 3976 |
. . . . 5
⊢ (𝑥 ∈ ((Base‘𝑅) ∖
{(0g‘𝑅)})
→ 𝑥 ∈ (𝐹 “ 𝑆)) |
64 | | fvelima 6958 |
. . . . 5
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ (𝐹 “ 𝑆)) → ∃𝑎 ∈ 𝑆 (𝐹‘𝑎) = 𝑥) |
65 | 60, 63, 64 | syl2an 595 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) → ∃𝑎 ∈ 𝑆 (𝐹‘𝑎) = 𝑥) |
66 | | simprr 772 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) → (𝐹‘𝑎) = 𝑥) |
67 | | simprl 770 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) → 𝑎 ∈ 𝑆) |
68 | 67 | fvresd 6911 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) → ((𝐹 ↾ 𝑆)‘𝑎) = (𝐹‘𝑎)) |
69 | | eqid 2727 |
. . . . . . . . . . 11
⊢ (𝑀 ↾s 𝑆) = (𝑀 ↾s 𝑆) |
70 | 69 | resrhm 20533 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (𝑀 RingHom 𝑁) ∧ 𝑆 ∈ (SubRing‘𝑀)) → (𝐹 ↾ 𝑆) ∈ ((𝑀 ↾s 𝑆) RingHom 𝑁)) |
71 | 1, 4, 70 | syl2anc 583 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 ↾ 𝑆) ∈ ((𝑀 ↾s 𝑆) RingHom 𝑁)) |
72 | | df-ima 5685 |
. . . . . . . . . . 11
⊢ (𝐹 “ 𝑆) = ran (𝐹 ↾ 𝑆) |
73 | | eqimss2 4037 |
. . . . . . . . . . 11
⊢ ((𝐹 “ 𝑆) = ran (𝐹 ↾ 𝑆) → ran (𝐹 ↾ 𝑆) ⊆ (𝐹 “ 𝑆)) |
74 | 72, 73 | mp1i 13 |
. . . . . . . . . 10
⊢ (𝜑 → ran (𝐹 ↾ 𝑆) ⊆ (𝐹 “ 𝑆)) |
75 | 7 | resrhm2b 20534 |
. . . . . . . . . 10
⊢ (((𝐹 “ 𝑆) ∈ (SubRing‘𝑁) ∧ ran (𝐹 ↾ 𝑆) ⊆ (𝐹 “ 𝑆)) → ((𝐹 ↾ 𝑆) ∈ ((𝑀 ↾s 𝑆) RingHom 𝑁) ↔ (𝐹 ↾ 𝑆) ∈ ((𝑀 ↾s 𝑆) RingHom 𝑅))) |
76 | 6, 74, 75 | syl2anc 583 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹 ↾ 𝑆) ∈ ((𝑀 ↾s 𝑆) RingHom 𝑁) ↔ (𝐹 ↾ 𝑆) ∈ ((𝑀 ↾s 𝑆) RingHom 𝑅))) |
77 | 71, 76 | mpbid 231 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ↾ 𝑆) ∈ ((𝑀 ↾s 𝑆) RingHom 𝑅)) |
78 | 77 | ad2antrr 725 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) → (𝐹 ↾ 𝑆) ∈ ((𝑀 ↾s 𝑆) RingHom 𝑅)) |
79 | | eldifsni 4789 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ((Base‘𝑅) ∖
{(0g‘𝑅)})
→ 𝑥 ≠
(0g‘𝑅)) |
80 | 79 | ad2antlr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) → 𝑥 ≠ (0g‘𝑅)) |
81 | 68 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) ∧ 𝑎 = (0g‘𝑀)) → ((𝐹 ↾ 𝑆)‘𝑎) = (𝐹‘𝑎)) |
82 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) ∧ 𝑎 = (0g‘𝑀)) → 𝑎 = (0g‘𝑀)) |
83 | 82 | fveq2d 6895 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) ∧ 𝑎 = (0g‘𝑀)) → ((𝐹 ↾ 𝑆)‘𝑎) = ((𝐹 ↾ 𝑆)‘(0g‘𝑀))) |
84 | 69, 43 | subrg0 20511 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 ∈ (SubRing‘𝑀) →
(0g‘𝑀) =
(0g‘(𝑀
↾s 𝑆))) |
85 | 4, 84 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0g‘𝑀) = (0g‘(𝑀 ↾s 𝑆))) |
86 | 85 | fveq2d 6895 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐹 ↾ 𝑆)‘(0g‘𝑀)) = ((𝐹 ↾ 𝑆)‘(0g‘(𝑀 ↾s 𝑆)))) |
87 | | rhmghm 20416 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ↾ 𝑆) ∈ ((𝑀 ↾s 𝑆) RingHom 𝑅) → (𝐹 ↾ 𝑆) ∈ ((𝑀 ↾s 𝑆) GrpHom 𝑅)) |
88 | | eqid 2727 |
. . . . . . . . . . . . . . 15
⊢
(0g‘(𝑀 ↾s 𝑆)) = (0g‘(𝑀 ↾s 𝑆)) |
89 | 88, 52 | ghmid 19169 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ↾ 𝑆) ∈ ((𝑀 ↾s 𝑆) GrpHom 𝑅) → ((𝐹 ↾ 𝑆)‘(0g‘(𝑀 ↾s 𝑆))) = (0g‘𝑅)) |
90 | 77, 87, 89 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐹 ↾ 𝑆)‘(0g‘(𝑀 ↾s 𝑆))) = (0g‘𝑅)) |
91 | 86, 90 | eqtrd 2767 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐹 ↾ 𝑆)‘(0g‘𝑀)) = (0g‘𝑅)) |
92 | 91 | ad3antrrr 729 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) ∧ 𝑎 = (0g‘𝑀)) → ((𝐹 ↾ 𝑆)‘(0g‘𝑀)) = (0g‘𝑅)) |
93 | 83, 92 | eqtrd 2767 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) ∧ 𝑎 = (0g‘𝑀)) → ((𝐹 ↾ 𝑆)‘𝑎) = (0g‘𝑅)) |
94 | | simplrr 777 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) ∧ 𝑎 = (0g‘𝑀)) → (𝐹‘𝑎) = 𝑥) |
95 | 81, 93, 94 | 3eqtr3rd 2776 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) ∧ 𝑎 = (0g‘𝑀)) → 𝑥 = (0g‘𝑅)) |
96 | 80, 95 | mteqand 3028 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) → 𝑎 ≠ (0g‘𝑀)) |
97 | 2 | ad2antrr 725 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) → 𝑆 ∈ (SubDRing‘𝑀)) |
98 | | eqid 2727 |
. . . . . . . . . 10
⊢
(Unit‘(𝑀
↾s 𝑆)) =
(Unit‘(𝑀
↾s 𝑆)) |
99 | 69, 43, 98 | sdrgunit 20677 |
. . . . . . . . 9
⊢ (𝑆 ∈ (SubDRing‘𝑀) → (𝑎 ∈ (Unit‘(𝑀 ↾s 𝑆)) ↔ (𝑎 ∈ 𝑆 ∧ 𝑎 ≠ (0g‘𝑀)))) |
100 | 97, 99 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) → (𝑎 ∈ (Unit‘(𝑀 ↾s 𝑆)) ↔ (𝑎 ∈ 𝑆 ∧ 𝑎 ≠ (0g‘𝑀)))) |
101 | 67, 96, 100 | mpbir2and 712 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) → 𝑎 ∈ (Unit‘(𝑀 ↾s 𝑆))) |
102 | | elrhmunit 20442 |
. . . . . . 7
⊢ (((𝐹 ↾ 𝑆) ∈ ((𝑀 ↾s 𝑆) RingHom 𝑅) ∧ 𝑎 ∈ (Unit‘(𝑀 ↾s 𝑆))) → ((𝐹 ↾ 𝑆)‘𝑎) ∈ (Unit‘𝑅)) |
103 | 78, 101, 102 | syl2anc 583 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) → ((𝐹 ↾ 𝑆)‘𝑎) ∈ (Unit‘𝑅)) |
104 | 68, 103 | eqeltrrd 2829 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) → (𝐹‘𝑎) ∈ (Unit‘𝑅)) |
105 | 66, 104 | eqeltrrd 2829 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∧ (𝑎 ∈ 𝑆 ∧ (𝐹‘𝑎) = 𝑥)) → 𝑥 ∈ (Unit‘𝑅)) |
106 | 65, 105 | rexlimddv 3156 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ {(0g‘𝑅)})) → 𝑥 ∈ (Unit‘𝑅)) |
107 | 59, 106 | eqelssd 3999 |
. 2
⊢ (𝜑 → (Unit‘𝑅) = ((Base‘𝑅) ∖
{(0g‘𝑅)})) |
108 | 10, 11, 52 | isdrng 20621 |
. 2
⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧
(Unit‘𝑅) =
((Base‘𝑅) ∖
{(0g‘𝑅)}))) |
109 | 9, 107, 108 | sylanbrc 582 |
1
⊢ (𝜑 → 𝑅 ∈ DivRing) |