Step | Hyp | Ref
| Expression |
1 | | isunitd.1 |
. . . 4
⊢ (𝜑 → 𝑈 = (Unit‘𝑅)) |
2 | | df-unit 13265 |
. . . . 5
⊢ Unit =
(𝑟 ∈ V ↦ (◡((∥r‘𝑟) ∩
(∥r‘(oppr‘𝑟))) “ {(1r‘𝑟)})) |
3 | | fveq2 5517 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (∥r‘𝑟) =
(∥r‘𝑅)) |
4 | | 2fveq3 5522 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 →
(∥r‘(oppr‘𝑟)) =
(∥r‘(oppr‘𝑅))) |
5 | 3, 4 | ineq12d 3339 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → ((∥r‘𝑟) ∩
(∥r‘(oppr‘𝑟))) = ((∥r‘𝑅) ∩
(∥r‘(oppr‘𝑅)))) |
6 | 5 | cnveqd 4805 |
. . . . . 6
⊢ (𝑟 = 𝑅 → ◡((∥r‘𝑟) ∩
(∥r‘(oppr‘𝑟))) = ◡((∥r‘𝑅) ∩
(∥r‘(oppr‘𝑅)))) |
7 | | fveq2 5517 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (1r‘𝑟) = (1r‘𝑅)) |
8 | 7 | sneqd 3607 |
. . . . . 6
⊢ (𝑟 = 𝑅 → {(1r‘𝑟)} = {(1r‘𝑅)}) |
9 | 6, 8 | imaeq12d 4973 |
. . . . 5
⊢ (𝑟 = 𝑅 → (◡((∥r‘𝑟) ∩
(∥r‘(oppr‘𝑟))) “ {(1r‘𝑟)}) = (◡((∥r‘𝑅) ∩
(∥r‘(oppr‘𝑅))) “ {(1r‘𝑅)})) |
10 | | isunitd.r |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ SRing) |
11 | 10 | elexd 2752 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ V) |
12 | | dvdsrex 13273 |
. . . . . . 7
⊢ (𝑅 ∈ SRing →
(∥r‘𝑅) ∈ V) |
13 | | inex1g 4141 |
. . . . . . 7
⊢
((∥r‘𝑅) ∈ V →
((∥r‘𝑅) ∩
(∥r‘(oppr‘𝑅))) ∈ V) |
14 | 10, 12, 13 | 3syl 17 |
. . . . . 6
⊢ (𝜑 →
((∥r‘𝑅) ∩
(∥r‘(oppr‘𝑅))) ∈ V) |
15 | | cnvexg 5168 |
. . . . . 6
⊢
(((∥r‘𝑅) ∩
(∥r‘(oppr‘𝑅))) ∈ V → ◡((∥r‘𝑅) ∩
(∥r‘(oppr‘𝑅))) ∈ V) |
16 | | imaexg 4984 |
. . . . . 6
⊢ (◡((∥r‘𝑅) ∩
(∥r‘(oppr‘𝑅))) ∈ V → (◡((∥r‘𝑅) ∩
(∥r‘(oppr‘𝑅))) “ {(1r‘𝑅)}) ∈ V) |
17 | 14, 15, 16 | 3syl 17 |
. . . . 5
⊢ (𝜑 → (◡((∥r‘𝑅) ∩
(∥r‘(oppr‘𝑅))) “ {(1r‘𝑅)}) ∈ V) |
18 | 2, 9, 11, 17 | fvmptd3 5612 |
. . . 4
⊢ (𝜑 → (Unit‘𝑅) = (◡((∥r‘𝑅) ∩
(∥r‘(oppr‘𝑅))) “ {(1r‘𝑅)})) |
19 | 1, 18 | eqtrd 2210 |
. . 3
⊢ (𝜑 → 𝑈 = (◡((∥r‘𝑅) ∩
(∥r‘(oppr‘𝑅))) “ {(1r‘𝑅)})) |
20 | 19 | eleq2d 2247 |
. 2
⊢ (𝜑 → (𝑋 ∈ 𝑈 ↔ 𝑋 ∈ (◡((∥r‘𝑅) ∩
(∥r‘(oppr‘𝑅))) “ {(1r‘𝑅)}))) |
21 | | isunitd.3 |
. . . . . 6
⊢ (𝜑 → ∥ =
(∥r‘𝑅)) |
22 | | isunitd.5 |
. . . . . . 7
⊢ (𝜑 → 𝐸 = (∥r‘𝑆)) |
23 | | isunitd.4 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 = (oppr‘𝑅)) |
24 | 23 | fveq2d 5521 |
. . . . . . 7
⊢ (𝜑 →
(∥r‘𝑆) =
(∥r‘(oppr‘𝑅))) |
25 | 22, 24 | eqtrd 2210 |
. . . . . 6
⊢ (𝜑 → 𝐸 =
(∥r‘(oppr‘𝑅))) |
26 | 21, 25 | ineq12d 3339 |
. . . . 5
⊢ (𝜑 → ( ∥ ∩ 𝐸) =
((∥r‘𝑅) ∩
(∥r‘(oppr‘𝑅)))) |
27 | 26 | cnveqd 4805 |
. . . 4
⊢ (𝜑 → ◡( ∥ ∩ 𝐸) = ◡((∥r‘𝑅) ∩
(∥r‘(oppr‘𝑅)))) |
28 | | isunitd.2 |
. . . . 5
⊢ (𝜑 → 1 =
(1r‘𝑅)) |
29 | 28 | sneqd 3607 |
. . . 4
⊢ (𝜑 → { 1 } =
{(1r‘𝑅)}) |
30 | 27, 29 | imaeq12d 4973 |
. . 3
⊢ (𝜑 → (◡( ∥ ∩ 𝐸) “ { 1 }) = (◡((∥r‘𝑅) ∩
(∥r‘(oppr‘𝑅))) “ {(1r‘𝑅)})) |
31 | 30 | eleq2d 2247 |
. 2
⊢ (𝜑 → (𝑋 ∈ (◡( ∥ ∩ 𝐸) “ { 1 }) ↔ 𝑋 ∈ (◡((∥r‘𝑅) ∩
(∥r‘(oppr‘𝑅))) “ {(1r‘𝑅)}))) |
32 | | reldvdsrsrg 13267 |
. . . . . 6
⊢ (𝑅 ∈ SRing → Rel
(∥r‘𝑅)) |
33 | 10, 32 | syl 14 |
. . . . 5
⊢ (𝜑 → Rel
(∥r‘𝑅)) |
34 | 21 | releqd 4712 |
. . . . 5
⊢ (𝜑 → (Rel ∥ ↔ Rel
(∥r‘𝑅))) |
35 | 33, 34 | mpbird 167 |
. . . 4
⊢ (𝜑 → Rel ∥ ) |
36 | | relin1 4746 |
. . . 4
⊢ (Rel
∥
→ Rel ( ∥ ∩ 𝐸)) |
37 | | eliniseg2 5010 |
. . . 4
⊢ (Rel (
∥
∩ 𝐸) → (𝑋 ∈ (◡( ∥ ∩ 𝐸) “ { 1 }) ↔ 𝑋( ∥ ∩ 𝐸) 1 )) |
38 | 35, 36, 37 | 3syl 17 |
. . 3
⊢ (𝜑 → (𝑋 ∈ (◡( ∥ ∩ 𝐸) “ { 1 }) ↔ 𝑋( ∥ ∩ 𝐸) 1 )) |
39 | | brin 4057 |
. . 3
⊢ (𝑋( ∥ ∩ 𝐸) 1 ↔ (𝑋 ∥ 1 ∧ 𝑋𝐸 1 )) |
40 | 38, 39 | bitrdi 196 |
. 2
⊢ (𝜑 → (𝑋 ∈ (◡( ∥ ∩ 𝐸) “ { 1 }) ↔ (𝑋 ∥ 1 ∧ 𝑋𝐸 1 ))) |
41 | 20, 31, 40 | 3bitr2d 216 |
1
⊢ (𝜑 → (𝑋 ∈ 𝑈 ↔ (𝑋 ∥ 1 ∧ 𝑋𝐸 1 ))) |