Step | Hyp | Ref
| Expression |
1 | | opprunitd.1 |
. . . . . 6
⊢ (𝜑 → 𝑈 = (Unit‘𝑅)) |
2 | | eqidd 2178 |
. . . . . 6
⊢ (𝜑 → (1r‘𝑅) = (1r‘𝑅)) |
3 | | eqidd 2178 |
. . . . . 6
⊢ (𝜑 →
(∥r‘𝑅) = (∥r‘𝑅)) |
4 | | opprunitd.2 |
. . . . . 6
⊢ (𝜑 → 𝑆 = (oppr‘𝑅)) |
5 | | eqidd 2178 |
. . . . . 6
⊢ (𝜑 →
(∥r‘𝑆) = (∥r‘𝑆)) |
6 | | opprunitd.r |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Ring) |
7 | | ringsrg 13155 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑅 ∈ SRing) |
8 | 6, 7 | syl 14 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ SRing) |
9 | 1, 2, 3, 4, 5, 8 | isunitd 13206 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝑈 ↔ (𝑥(∥r‘𝑅)(1r‘𝑅) ∧ 𝑥(∥r‘𝑆)(1r‘𝑅)))) |
10 | | eqid 2177 |
. . . . . . . . . . . . . . 15
⊢
(oppr‘𝑅) = (oppr‘𝑅) |
11 | 10 | opprring 13180 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ Ring →
(oppr‘𝑅) ∈ Ring) |
12 | 6, 11 | syl 14 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(oppr‘𝑅) ∈ Ring) |
13 | 4, 12 | eqeltrd 2254 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ Ring) |
14 | | vex 2740 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ V |
15 | 14 | a1i 9 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑦 ∈ V) |
16 | | vex 2740 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
17 | 16 | a1i 9 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑥 ∈ V) |
18 | | eqid 2177 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑆) =
(Base‘𝑆) |
19 | | eqid 2177 |
. . . . . . . . . . . . 13
⊢
(.r‘𝑆) = (.r‘𝑆) |
20 | | eqid 2177 |
. . . . . . . . . . . . 13
⊢
(oppr‘𝑆) = (oppr‘𝑆) |
21 | | eqid 2177 |
. . . . . . . . . . . . 13
⊢
(.r‘(oppr‘𝑆)) =
(.r‘(oppr‘𝑆)) |
22 | 18, 19, 20, 21 | opprmulg 13174 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Ring ∧ 𝑦 ∈ V ∧ 𝑥 ∈ V) → (𝑦(.r‘(oppr‘𝑆))𝑥) = (𝑥(.r‘𝑆)𝑦)) |
23 | 13, 15, 17, 22 | syl3anc 1238 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑦(.r‘(oppr‘𝑆))𝑥) = (𝑥(.r‘𝑆)𝑦)) |
24 | 4 | fveq2d 5518 |
. . . . . . . . . . . 12
⊢ (𝜑 → (.r‘𝑆) =
(.r‘(oppr‘𝑅))) |
25 | 24 | oveqd 5889 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥(.r‘𝑆)𝑦) = (𝑥(.r‘(oppr‘𝑅))𝑦)) |
26 | | eqid 2177 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑅) =
(Base‘𝑅) |
27 | | eqid 2177 |
. . . . . . . . . . . . 13
⊢
(.r‘𝑅) = (.r‘𝑅) |
28 | | eqid 2177 |
. . . . . . . . . . . . 13
⊢
(.r‘(oppr‘𝑅)) =
(.r‘(oppr‘𝑅)) |
29 | 26, 27, 10, 28 | opprmulg 13174 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ V ∧ 𝑦 ∈ V) → (𝑥(.r‘(oppr‘𝑅))𝑦) = (𝑦(.r‘𝑅)𝑥)) |
30 | 6, 17, 15, 29 | syl3anc 1238 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥(.r‘(oppr‘𝑅))𝑦) = (𝑦(.r‘𝑅)𝑥)) |
31 | 23, 25, 30 | 3eqtrrd 2215 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦(.r‘𝑅)𝑥) = (𝑦(.r‘(oppr‘𝑆))𝑥)) |
32 | 31 | eqeq1d 2186 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ↔ (𝑦(.r‘(oppr‘𝑆))𝑥) = (1r‘𝑅))) |
33 | 32 | rexbidv 2478 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑦 ∈ (Base‘𝑅)(𝑦(.r‘𝑅)𝑥) = (1r‘𝑅) ↔ ∃𝑦 ∈ (Base‘𝑅)(𝑦(.r‘(oppr‘𝑆))𝑥) = (1r‘𝑅))) |
34 | 33 | anbi2d 464 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ (Base‘𝑅) ∧ ∃𝑦 ∈ (Base‘𝑅)(𝑦(.r‘𝑅)𝑥) = (1r‘𝑅)) ↔ (𝑥 ∈ (Base‘𝑅) ∧ ∃𝑦 ∈ (Base‘𝑅)(𝑦(.r‘(oppr‘𝑆))𝑥) = (1r‘𝑅)))) |
35 | | eqidd 2178 |
. . . . . . . 8
⊢ (𝜑 → (Base‘𝑅) = (Base‘𝑅)) |
36 | | eqidd 2178 |
. . . . . . . 8
⊢ (𝜑 → (.r‘𝑅) = (.r‘𝑅)) |
37 | 35, 3, 8, 36 | dvdsrd 13194 |
. . . . . . 7
⊢ (𝜑 → (𝑥(∥r‘𝑅)(1r‘𝑅) ↔ (𝑥 ∈ (Base‘𝑅) ∧ ∃𝑦 ∈ (Base‘𝑅)(𝑦(.r‘𝑅)𝑥) = (1r‘𝑅)))) |
38 | 10, 26 | opprbasg 13178 |
. . . . . . . . . 10
⊢ (𝑅 ∈ SRing →
(Base‘𝑅) =
(Base‘(oppr‘𝑅))) |
39 | 8, 38 | syl 14 |
. . . . . . . . 9
⊢ (𝜑 → (Base‘𝑅) =
(Base‘(oppr‘𝑅))) |
40 | 4 | fveq2d 5518 |
. . . . . . . . 9
⊢ (𝜑 → (Base‘𝑆) =
(Base‘(oppr‘𝑅))) |
41 | 20, 18 | opprbasg 13178 |
. . . . . . . . . 10
⊢ (𝑆 ∈ Ring →
(Base‘𝑆) =
(Base‘(oppr‘𝑆))) |
42 | 13, 41 | syl 14 |
. . . . . . . . 9
⊢ (𝜑 → (Base‘𝑆) =
(Base‘(oppr‘𝑆))) |
43 | 39, 40, 42 | 3eqtr2d 2216 |
. . . . . . . 8
⊢ (𝜑 → (Base‘𝑅) =
(Base‘(oppr‘𝑆))) |
44 | | eqidd 2178 |
. . . . . . . 8
⊢ (𝜑 →
(∥r‘(oppr‘𝑆)) =
(∥r‘(oppr‘𝑆))) |
45 | 20 | opprring 13180 |
. . . . . . . . . 10
⊢ (𝑆 ∈ Ring →
(oppr‘𝑆) ∈ Ring) |
46 | 13, 45 | syl 14 |
. . . . . . . . 9
⊢ (𝜑 →
(oppr‘𝑆) ∈ Ring) |
47 | | ringsrg 13155 |
. . . . . . . . 9
⊢
((oppr‘𝑆) ∈ Ring →
(oppr‘𝑆) ∈ SRing) |
48 | 46, 47 | syl 14 |
. . . . . . . 8
⊢ (𝜑 →
(oppr‘𝑆) ∈ SRing) |
49 | | eqidd 2178 |
. . . . . . . 8
⊢ (𝜑 →
(.r‘(oppr‘𝑆)) =
(.r‘(oppr‘𝑆))) |
50 | 43, 44, 48, 49 | dvdsrd 13194 |
. . . . . . 7
⊢ (𝜑 → (𝑥(∥r‘(oppr‘𝑆))(1r‘𝑅) ↔ (𝑥 ∈ (Base‘𝑅) ∧ ∃𝑦 ∈ (Base‘𝑅)(𝑦(.r‘(oppr‘𝑆))𝑥) = (1r‘𝑅)))) |
51 | 34, 37, 50 | 3bitr4d 220 |
. . . . . 6
⊢ (𝜑 → (𝑥(∥r‘𝑅)(1r‘𝑅) ↔ 𝑥(∥r‘(oppr‘𝑆))(1r‘𝑅))) |
52 | 51 | anbi1d 465 |
. . . . 5
⊢ (𝜑 → ((𝑥(∥r‘𝑅)(1r‘𝑅) ∧ 𝑥(∥r‘𝑆)(1r‘𝑅)) ↔ (𝑥(∥r‘(oppr‘𝑆))(1r‘𝑅) ∧ 𝑥(∥r‘𝑆)(1r‘𝑅)))) |
53 | 9, 52 | bitrd 188 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑈 ↔ (𝑥(∥r‘(oppr‘𝑆))(1r‘𝑅) ∧ 𝑥(∥r‘𝑆)(1r‘𝑅)))) |
54 | 53 | biancomd 271 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝑈 ↔ (𝑥(∥r‘𝑆)(1r‘𝑅) ∧ 𝑥(∥r‘(oppr‘𝑆))(1r‘𝑅)))) |
55 | | eqidd 2178 |
. . . 4
⊢ (𝜑 → (Unit‘𝑆) = (Unit‘𝑆)) |
56 | | eqid 2177 |
. . . . . . 7
⊢
(1r‘𝑅) = (1r‘𝑅) |
57 | 10, 56 | oppr1g 13183 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
(1r‘𝑅) =
(1r‘(oppr‘𝑅))) |
58 | 6, 57 | syl 14 |
. . . . 5
⊢ (𝜑 → (1r‘𝑅) =
(1r‘(oppr‘𝑅))) |
59 | 4 | fveq2d 5518 |
. . . . 5
⊢ (𝜑 → (1r‘𝑆) =
(1r‘(oppr‘𝑅))) |
60 | 58, 59 | eqtr4d 2213 |
. . . 4
⊢ (𝜑 → (1r‘𝑅) = (1r‘𝑆)) |
61 | | eqidd 2178 |
. . . 4
⊢ (𝜑 →
(oppr‘𝑆) = (oppr‘𝑆)) |
62 | | ringsrg 13155 |
. . . . 5
⊢ (𝑆 ∈ Ring → 𝑆 ∈ SRing) |
63 | 13, 62 | syl 14 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ SRing) |
64 | 55, 60, 5, 61, 44, 63 | isunitd 13206 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (Unit‘𝑆) ↔ (𝑥(∥r‘𝑆)(1r‘𝑅) ∧ 𝑥(∥r‘(oppr‘𝑆))(1r‘𝑅)))) |
65 | 54, 64 | bitr4d 191 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑈 ↔ 𝑥 ∈ (Unit‘𝑆))) |
66 | 65 | eqrdv 2175 |
1
⊢ (𝜑 → 𝑈 = (Unit‘𝑆)) |