Step | Hyp | Ref
| Expression |
1 | | elfvdm 6220 |
. . . 4
⊢ (𝑋 ∈ (Irred‘𝑅) → 𝑅 ∈ dom Irred) |
2 | | irred.3 |
. . . 4
⊢ 𝐼 = (Irred‘𝑅) |
3 | 1, 2 | eleq2s 2719 |
. . 3
⊢ (𝑋 ∈ 𝐼 → 𝑅 ∈ dom Irred) |
4 | | elex 3212 |
. . 3
⊢ (𝑅 ∈ dom Irred → 𝑅 ∈ V) |
5 | 3, 4 | syl 17 |
. 2
⊢ (𝑋 ∈ 𝐼 → 𝑅 ∈ V) |
6 | | eldifi 3732 |
. . . . . 6
⊢ (𝑋 ∈ (𝐵 ∖ 𝑈) → 𝑋 ∈ 𝐵) |
7 | | irred.4 |
. . . . . 6
⊢ 𝑁 = (𝐵 ∖ 𝑈) |
8 | 6, 7 | eleq2s 2719 |
. . . . 5
⊢ (𝑋 ∈ 𝑁 → 𝑋 ∈ 𝐵) |
9 | | irred.1 |
. . . . 5
⊢ 𝐵 = (Base‘𝑅) |
10 | 8, 9 | syl6eleq 2711 |
. . . 4
⊢ (𝑋 ∈ 𝑁 → 𝑋 ∈ (Base‘𝑅)) |
11 | 10 | elfvexd 6222 |
. . 3
⊢ (𝑋 ∈ 𝑁 → 𝑅 ∈ V) |
12 | 11 | adantr 481 |
. 2
⊢ ((𝑋 ∈ 𝑁 ∧ ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥 · 𝑦) ≠ 𝑋) → 𝑅 ∈ V) |
13 | | fvex 6201 |
. . . . . . . 8
⊢
(Base‘𝑟)
∈ V |
14 | | difexg 4808 |
. . . . . . . 8
⊢
((Base‘𝑟)
∈ V → ((Base‘𝑟) ∖ (Unit‘𝑟)) ∈ V) |
15 | 13, 14 | mp1i 13 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → ((Base‘𝑟) ∖ (Unit‘𝑟)) ∈ V) |
16 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) |
17 | | simpl 473 |
. . . . . . . . . . . . 13
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → 𝑟 = 𝑅) |
18 | 17 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (Base‘𝑟) = (Base‘𝑅)) |
19 | 18, 9 | syl6eqr 2674 |
. . . . . . . . . . 11
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (Base‘𝑟) = 𝐵) |
20 | 17 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (Unit‘𝑟) = (Unit‘𝑅)) |
21 | | irred.2 |
. . . . . . . . . . . 12
⊢ 𝑈 = (Unit‘𝑅) |
22 | 20, 21 | syl6eqr 2674 |
. . . . . . . . . . 11
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (Unit‘𝑟) = 𝑈) |
23 | 19, 22 | difeq12d 3729 |
. . . . . . . . . 10
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → ((Base‘𝑟) ∖ (Unit‘𝑟)) = (𝐵 ∖ 𝑈)) |
24 | 23, 7 | syl6eqr 2674 |
. . . . . . . . 9
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → ((Base‘𝑟) ∖ (Unit‘𝑟)) = 𝑁) |
25 | 16, 24 | eqtrd 2656 |
. . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → 𝑏 = 𝑁) |
26 | 17 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (.r‘𝑟) = (.r‘𝑅)) |
27 | | irred.5 |
. . . . . . . . . . . . 13
⊢ · =
(.r‘𝑅) |
28 | 26, 27 | syl6eqr 2674 |
. . . . . . . . . . . 12
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (.r‘𝑟) = · ) |
29 | 28 | oveqd 6667 |
. . . . . . . . . . 11
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (𝑥(.r‘𝑟)𝑦) = (𝑥 · 𝑦)) |
30 | 29 | neeq1d 2853 |
. . . . . . . . . 10
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → ((𝑥(.r‘𝑟)𝑦) ≠ 𝑧 ↔ (𝑥 · 𝑦) ≠ 𝑧)) |
31 | 25, 30 | raleqbidv 3152 |
. . . . . . . . 9
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ≠ 𝑧 ↔ ∀𝑦 ∈ 𝑁 (𝑥 · 𝑦) ≠ 𝑧)) |
32 | 25, 31 | raleqbidv 3152 |
. . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ≠ 𝑧 ↔ ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥 · 𝑦) ≠ 𝑧)) |
33 | 25, 32 | rabeqbidv 3195 |
. . . . . . 7
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → {𝑧 ∈ 𝑏 ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ≠ 𝑧} = {𝑧 ∈ 𝑁 ∣ ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥 · 𝑦) ≠ 𝑧}) |
34 | 15, 33 | csbied 3560 |
. . . . . 6
⊢ (𝑟 = 𝑅 → ⦋((Base‘𝑟) ∖ (Unit‘𝑟)) / 𝑏⦌{𝑧 ∈ 𝑏 ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ≠ 𝑧} = {𝑧 ∈ 𝑁 ∣ ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥 · 𝑦) ≠ 𝑧}) |
35 | | df-irred 18643 |
. . . . . 6
⊢ Irred =
(𝑟 ∈ V ↦
⦋((Base‘𝑟) ∖ (Unit‘𝑟)) / 𝑏⦌{𝑧 ∈ 𝑏 ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ≠ 𝑧}) |
36 | | fvex 6201 |
. . . . . . . . . 10
⊢
(Base‘𝑅)
∈ V |
37 | 9, 36 | eqeltri 2697 |
. . . . . . . . 9
⊢ 𝐵 ∈ V |
38 | | difexg 4808 |
. . . . . . . . 9
⊢ (𝐵 ∈ V → (𝐵 ∖ 𝑈) ∈ V) |
39 | 37, 38 | ax-mp 5 |
. . . . . . . 8
⊢ (𝐵 ∖ 𝑈) ∈ V |
40 | 7, 39 | eqeltri 2697 |
. . . . . . 7
⊢ 𝑁 ∈ V |
41 | 40 | rabex 4813 |
. . . . . 6
⊢ {𝑧 ∈ 𝑁 ∣ ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥 · 𝑦) ≠ 𝑧} ∈ V |
42 | 34, 35, 41 | fvmpt 6282 |
. . . . 5
⊢ (𝑅 ∈ V →
(Irred‘𝑅) = {𝑧 ∈ 𝑁 ∣ ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥 · 𝑦) ≠ 𝑧}) |
43 | 2, 42 | syl5eq 2668 |
. . . 4
⊢ (𝑅 ∈ V → 𝐼 = {𝑧 ∈ 𝑁 ∣ ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥 · 𝑦) ≠ 𝑧}) |
44 | 43 | eleq2d 2687 |
. . 3
⊢ (𝑅 ∈ V → (𝑋 ∈ 𝐼 ↔ 𝑋 ∈ {𝑧 ∈ 𝑁 ∣ ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥 · 𝑦) ≠ 𝑧})) |
45 | | neeq2 2857 |
. . . . 5
⊢ (𝑧 = 𝑋 → ((𝑥 · 𝑦) ≠ 𝑧 ↔ (𝑥 · 𝑦) ≠ 𝑋)) |
46 | 45 | 2ralbidv 2989 |
. . . 4
⊢ (𝑧 = 𝑋 → (∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥 · 𝑦) ≠ 𝑧 ↔ ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥 · 𝑦) ≠ 𝑋)) |
47 | 46 | elrab 3363 |
. . 3
⊢ (𝑋 ∈ {𝑧 ∈ 𝑁 ∣ ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥 · 𝑦) ≠ 𝑧} ↔ (𝑋 ∈ 𝑁 ∧ ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥 · 𝑦) ≠ 𝑋)) |
48 | 44, 47 | syl6bb 276 |
. 2
⊢ (𝑅 ∈ V → (𝑋 ∈ 𝐼 ↔ (𝑋 ∈ 𝑁 ∧ ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥 · 𝑦) ≠ 𝑋))) |
49 | 5, 12, 48 | pm5.21nii 368 |
1
⊢ (𝑋 ∈ 𝐼 ↔ (𝑋 ∈ 𝑁 ∧ ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥 · 𝑦) ≠ 𝑋)) |