Step | Hyp | Ref
| Expression |
1 | | crngunit.1 |
. . . . 5
⊢ 𝑈 = (Unit‘𝑅) |
2 | 1 | a1i 9 |
. . . 4
⊢ (𝑅 ∈ CRing → 𝑈 = (Unit‘𝑅)) |
3 | | crngunit.2 |
. . . . 5
⊢ 1 =
(1r‘𝑅) |
4 | 3 | a1i 9 |
. . . 4
⊢ (𝑅 ∈ CRing → 1 =
(1r‘𝑅)) |
5 | | crngunit.3 |
. . . . 5
⊢ ∥ =
(∥r‘𝑅) |
6 | 5 | a1i 9 |
. . . 4
⊢ (𝑅 ∈ CRing → ∥ =
(∥r‘𝑅)) |
7 | | eqidd 2178 |
. . . 4
⊢ (𝑅 ∈ CRing →
(oppr‘𝑅) = (oppr‘𝑅)) |
8 | | eqidd 2178 |
. . . 4
⊢ (𝑅 ∈ CRing →
(∥r‘(oppr‘𝑅)) =
(∥r‘(oppr‘𝑅))) |
9 | | crngring 13122 |
. . . . 5
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
10 | | ringsrg 13155 |
. . . . 5
⊢ (𝑅 ∈ Ring → 𝑅 ∈ SRing) |
11 | 9, 10 | syl 14 |
. . . 4
⊢ (𝑅 ∈ CRing → 𝑅 ∈ SRing) |
12 | 2, 4, 6, 7, 8, 11 | isunitd 13206 |
. . 3
⊢ (𝑅 ∈ CRing → (𝑋 ∈ 𝑈 ↔ (𝑋 ∥ 1 ∧ 𝑋(∥r‘(oppr‘𝑅)) 1 ))) |
13 | | eqid 2177 |
. . . . . . . . . . . 12
⊢
(Base‘𝑅) =
(Base‘𝑅) |
14 | | eqid 2177 |
. . . . . . . . . . . 12
⊢
(.r‘𝑅) = (.r‘𝑅) |
15 | | eqid 2177 |
. . . . . . . . . . . 12
⊢
(oppr‘𝑅) = (oppr‘𝑅) |
16 | | eqid 2177 |
. . . . . . . . . . . 12
⊢
(.r‘(oppr‘𝑅)) =
(.r‘(oppr‘𝑅)) |
17 | 13, 14, 15, 16 | crngoppr 13175 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑋 ∈ (Base‘𝑅)) → (𝑦(.r‘𝑅)𝑋) = (𝑦(.r‘(oppr‘𝑅))𝑋)) |
18 | 17 | 3expa 1203 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑋 ∈ (Base‘𝑅)) → (𝑦(.r‘𝑅)𝑋) = (𝑦(.r‘(oppr‘𝑅))𝑋)) |
19 | 18 | eqcomd 2183 |
. . . . . . . . 9
⊢ (((𝑅 ∈ CRing ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑋 ∈ (Base‘𝑅)) → (𝑦(.r‘(oppr‘𝑅))𝑋) = (𝑦(.r‘𝑅)𝑋)) |
20 | 19 | an32s 568 |
. . . . . . . 8
⊢ (((𝑅 ∈ CRing ∧ 𝑋 ∈ (Base‘𝑅)) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑦(.r‘(oppr‘𝑅))𝑋) = (𝑦(.r‘𝑅)𝑋)) |
21 | 20 | eqeq1d 2186 |
. . . . . . 7
⊢ (((𝑅 ∈ CRing ∧ 𝑋 ∈ (Base‘𝑅)) ∧ 𝑦 ∈ (Base‘𝑅)) → ((𝑦(.r‘(oppr‘𝑅))𝑋) = 1 ↔ (𝑦(.r‘𝑅)𝑋)
= 1
)) |
22 | 21 | rexbidva 2474 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ (Base‘𝑅)) → (∃𝑦 ∈ (Base‘𝑅)(𝑦(.r‘(oppr‘𝑅))𝑋) = 1 ↔ ∃𝑦 ∈ (Base‘𝑅)(𝑦(.r‘𝑅)𝑋)
= 1
)) |
23 | 22 | pm5.32da 452 |
. . . . 5
⊢ (𝑅 ∈ CRing → ((𝑋 ∈ (Base‘𝑅) ∧ ∃𝑦 ∈ (Base‘𝑅)(𝑦(.r‘(oppr‘𝑅))𝑋) = 1 ) ↔ (𝑋 ∈ (Base‘𝑅) ∧ ∃𝑦 ∈ (Base‘𝑅)(𝑦(.r‘𝑅)𝑋)
= 1
))) |
24 | 15, 13 | opprbasg 13178 |
. . . . . 6
⊢ (𝑅 ∈ CRing →
(Base‘𝑅) =
(Base‘(oppr‘𝑅))) |
25 | 15 | opprring 13180 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
(oppr‘𝑅) ∈ Ring) |
26 | | ringsrg 13155 |
. . . . . . 7
⊢
((oppr‘𝑅) ∈ Ring →
(oppr‘𝑅) ∈ SRing) |
27 | 9, 25, 26 | 3syl 17 |
. . . . . 6
⊢ (𝑅 ∈ CRing →
(oppr‘𝑅) ∈ SRing) |
28 | | eqidd 2178 |
. . . . . 6
⊢ (𝑅 ∈ CRing →
(.r‘(oppr‘𝑅)) =
(.r‘(oppr‘𝑅))) |
29 | 24, 8, 27, 28 | dvdsrd 13194 |
. . . . 5
⊢ (𝑅 ∈ CRing → (𝑋(∥r‘(oppr‘𝑅)) 1 ↔ (𝑋 ∈ (Base‘𝑅) ∧ ∃𝑦 ∈ (Base‘𝑅)(𝑦(.r‘(oppr‘𝑅))𝑋) = 1 ))) |
30 | | eqidd 2178 |
. . . . . 6
⊢ (𝑅 ∈ CRing →
(Base‘𝑅) =
(Base‘𝑅)) |
31 | | eqidd 2178 |
. . . . . 6
⊢ (𝑅 ∈ CRing →
(.r‘𝑅) =
(.r‘𝑅)) |
32 | 30, 6, 11, 31 | dvdsrd 13194 |
. . . . 5
⊢ (𝑅 ∈ CRing → (𝑋 ∥ 1 ↔ (𝑋 ∈ (Base‘𝑅) ∧ ∃𝑦 ∈ (Base‘𝑅)(𝑦(.r‘𝑅)𝑋) = 1 ))) |
33 | 23, 29, 32 | 3bitr4d 220 |
. . . 4
⊢ (𝑅 ∈ CRing → (𝑋(∥r‘(oppr‘𝑅)) 1 ↔ 𝑋 ∥ 1 )) |
34 | 33 | anbi2d 464 |
. . 3
⊢ (𝑅 ∈ CRing → ((𝑋 ∥ 1 ∧ 𝑋(∥r‘(oppr‘𝑅)) 1 ) ↔ (𝑋 ∥ 1 ∧ 𝑋 ∥ 1 ))) |
35 | 12, 34 | bitrd 188 |
. 2
⊢ (𝑅 ∈ CRing → (𝑋 ∈ 𝑈 ↔ (𝑋 ∥ 1 ∧ 𝑋 ∥ 1 ))) |
36 | | pm4.24 395 |
. 2
⊢ (𝑋 ∥ 1 ↔ (𝑋 ∥ 1 ∧ 𝑋 ∥ 1 )) |
37 | 35, 36 | bitr4di 198 |
1
⊢ (𝑅 ∈ CRing → (𝑋 ∈ 𝑈 ↔ 𝑋 ∥ 1 )) |