Step | Hyp | Ref
| Expression |
1 | | df-rprm 19519 |
. 2
⊢ RPrime =
(𝑟 ∈ V ↦
⦋(Base‘𝑟) / 𝑏⦌{𝑝 ∈ (𝑏 ∖ ((Unit‘𝑟) ∪ {(0g‘𝑟)})) ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 [(∥r‘𝑟) / 𝑑](𝑝𝑑(𝑥(.r‘𝑟)𝑦) → (𝑝𝑑𝑥 ∨ 𝑝𝑑𝑦))}) |
2 | | fvexd 6666 |
. . 3
⊢ (𝑟 = 𝑅 → (Base‘𝑟) ∈ V) |
3 | | simpr 489 |
. . . . . . 7
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (Base‘𝑟)) → 𝑏 = (Base‘𝑟)) |
4 | | fveq2 6651 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅)) |
5 | 4 | adantr 485 |
. . . . . . 7
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (Base‘𝑟)) → (Base‘𝑟) = (Base‘𝑅)) |
6 | 3, 5 | eqtrd 2794 |
. . . . . 6
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (Base‘𝑟)) → 𝑏 = (Base‘𝑅)) |
7 | | rprmval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑅) |
8 | 6, 7 | eqtr4di 2812 |
. . . . 5
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (Base‘𝑟)) → 𝑏 = 𝐵) |
9 | | fveq2 6651 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (Unit‘𝑟) = (Unit‘𝑅)) |
10 | | rprmval.u |
. . . . . . . 8
⊢ 𝑈 = (Unit‘𝑅) |
11 | 9, 10 | eqtr4di 2812 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (Unit‘𝑟) = 𝑈) |
12 | | fveq2 6651 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (0g‘𝑟) = (0g‘𝑅)) |
13 | | rprmval.1 |
. . . . . . . . 9
⊢ 0 =
(0g‘𝑅) |
14 | 12, 13 | eqtr4di 2812 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (0g‘𝑟) = 0 ) |
15 | 14 | sneqd 4527 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → {(0g‘𝑟)} = { 0 }) |
16 | 11, 15 | uneq12d 4065 |
. . . . . 6
⊢ (𝑟 = 𝑅 → ((Unit‘𝑟) ∪ {(0g‘𝑟)}) = (𝑈 ∪ { 0 })) |
17 | 16 | adantr 485 |
. . . . 5
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (Base‘𝑟)) → ((Unit‘𝑟) ∪ {(0g‘𝑟)}) = (𝑈 ∪ { 0 })) |
18 | 8, 17 | difeq12d 4025 |
. . . 4
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (Base‘𝑟)) → (𝑏 ∖ ((Unit‘𝑟) ∪ {(0g‘𝑟)})) = (𝐵 ∖ (𝑈 ∪ { 0 }))) |
19 | | fvexd 6666 |
. . . . . . 7
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (Base‘𝑟)) → (∥r‘𝑟) ∈ V) |
20 | | eqidd 2760 |
. . . . . . . . 9
⊢ (((𝑟 = 𝑅 ∧ 𝑏 = (Base‘𝑟)) ∧ 𝑑 = (∥r‘𝑟)) → 𝑝 = 𝑝) |
21 | | simpr 489 |
. . . . . . . . . . 11
⊢ (((𝑟 = 𝑅 ∧ 𝑏 = (Base‘𝑟)) ∧ 𝑑 = (∥r‘𝑟)) → 𝑑 = (∥r‘𝑟)) |
22 | | fveq2 6651 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑅 → (∥r‘𝑟) =
(∥r‘𝑅)) |
23 | 22 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝑟 = 𝑅 ∧ 𝑏 = (Base‘𝑟)) ∧ 𝑑 = (∥r‘𝑟)) →
(∥r‘𝑟) = (∥r‘𝑅)) |
24 | 21, 23 | eqtrd 2794 |
. . . . . . . . . 10
⊢ (((𝑟 = 𝑅 ∧ 𝑏 = (Base‘𝑟)) ∧ 𝑑 = (∥r‘𝑟)) → 𝑑 = (∥r‘𝑅)) |
25 | | rprmval.d |
. . . . . . . . . 10
⊢ ∥ =
(∥r‘𝑅) |
26 | 24, 25 | eqtr4di 2812 |
. . . . . . . . 9
⊢ (((𝑟 = 𝑅 ∧ 𝑏 = (Base‘𝑟)) ∧ 𝑑 = (∥r‘𝑟)) → 𝑑 = ∥ ) |
27 | | fveq2 6651 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑅 → (.r‘𝑟) = (.r‘𝑅)) |
28 | | rprmval.m |
. . . . . . . . . . . 12
⊢ · =
(.r‘𝑅) |
29 | 27, 28 | eqtr4di 2812 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → (.r‘𝑟) = · ) |
30 | 29 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝑟 = 𝑅 ∧ 𝑏 = (Base‘𝑟)) ∧ 𝑑 = (∥r‘𝑟)) →
(.r‘𝑟) =
·
) |
31 | 30 | oveqd 7160 |
. . . . . . . . 9
⊢ (((𝑟 = 𝑅 ∧ 𝑏 = (Base‘𝑟)) ∧ 𝑑 = (∥r‘𝑟)) → (𝑥(.r‘𝑟)𝑦) = (𝑥 · 𝑦)) |
32 | 20, 26, 31 | breq123d 5039 |
. . . . . . . 8
⊢ (((𝑟 = 𝑅 ∧ 𝑏 = (Base‘𝑟)) ∧ 𝑑 = (∥r‘𝑟)) → (𝑝𝑑(𝑥(.r‘𝑟)𝑦) ↔ 𝑝 ∥ (𝑥 · 𝑦))) |
33 | 26 | breqd 5036 |
. . . . . . . . 9
⊢ (((𝑟 = 𝑅 ∧ 𝑏 = (Base‘𝑟)) ∧ 𝑑 = (∥r‘𝑟)) → (𝑝𝑑𝑥 ↔ 𝑝 ∥ 𝑥)) |
34 | 26 | breqd 5036 |
. . . . . . . . 9
⊢ (((𝑟 = 𝑅 ∧ 𝑏 = (Base‘𝑟)) ∧ 𝑑 = (∥r‘𝑟)) → (𝑝𝑑𝑦 ↔ 𝑝 ∥ 𝑦)) |
35 | 33, 34 | orbi12d 917 |
. . . . . . . 8
⊢ (((𝑟 = 𝑅 ∧ 𝑏 = (Base‘𝑟)) ∧ 𝑑 = (∥r‘𝑟)) → ((𝑝𝑑𝑥 ∨ 𝑝𝑑𝑦) ↔ (𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦))) |
36 | 32, 35 | imbi12d 349 |
. . . . . . 7
⊢ (((𝑟 = 𝑅 ∧ 𝑏 = (Base‘𝑟)) ∧ 𝑑 = (∥r‘𝑟)) → ((𝑝𝑑(𝑥(.r‘𝑟)𝑦) → (𝑝𝑑𝑥 ∨ 𝑝𝑑𝑦)) ↔ (𝑝 ∥ (𝑥 · 𝑦) → (𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦)))) |
37 | 19, 36 | sbcied 3735 |
. . . . . 6
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (Base‘𝑟)) →
([(∥r‘𝑟) / 𝑑](𝑝𝑑(𝑥(.r‘𝑟)𝑦) → (𝑝𝑑𝑥 ∨ 𝑝𝑑𝑦)) ↔ (𝑝 ∥ (𝑥 · 𝑦) → (𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦)))) |
38 | 8, 37 | raleqbidv 3317 |
. . . . 5
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (Base‘𝑟)) → (∀𝑦 ∈ 𝑏 [(∥r‘𝑟) / 𝑑](𝑝𝑑(𝑥(.r‘𝑟)𝑦) → (𝑝𝑑𝑥 ∨ 𝑝𝑑𝑦)) ↔ ∀𝑦 ∈ 𝐵 (𝑝 ∥ (𝑥 · 𝑦) → (𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦)))) |
39 | 8, 38 | raleqbidv 3317 |
. . . 4
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (Base‘𝑟)) → (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 [(∥r‘𝑟) / 𝑑](𝑝𝑑(𝑥(.r‘𝑟)𝑦) → (𝑝𝑑𝑥 ∨ 𝑝𝑑𝑦)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑝 ∥ (𝑥 · 𝑦) → (𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦)))) |
40 | 18, 39 | rabeqbidv 3396 |
. . 3
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (Base‘𝑟)) → {𝑝 ∈ (𝑏 ∖ ((Unit‘𝑟) ∪ {(0g‘𝑟)})) ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 [(∥r‘𝑟) / 𝑑](𝑝𝑑(𝑥(.r‘𝑟)𝑦) → (𝑝𝑑𝑥 ∨ 𝑝𝑑𝑦))} = {𝑝 ∈ (𝐵 ∖ (𝑈 ∪ { 0 })) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑝 ∥ (𝑥 · 𝑦) → (𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦))}) |
41 | 2, 40 | csbied 3837 |
. 2
⊢ (𝑟 = 𝑅 → ⦋(Base‘𝑟) / 𝑏⦌{𝑝 ∈ (𝑏 ∖ ((Unit‘𝑟) ∪ {(0g‘𝑟)})) ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 [(∥r‘𝑟) / 𝑑](𝑝𝑑(𝑥(.r‘𝑟)𝑦) → (𝑝𝑑𝑥 ∨ 𝑝𝑑𝑦))} = {𝑝 ∈ (𝐵 ∖ (𝑈 ∪ { 0 })) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑝 ∥ (𝑥 · 𝑦) → (𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦))}) |
42 | | elex 3427 |
. 2
⊢ (𝑅 ∈ 𝑉 → 𝑅 ∈ V) |
43 | 7 | fvexi 6665 |
. . . . 5
⊢ 𝐵 ∈ V |
44 | 43 | difexi 5191 |
. . . 4
⊢ (𝐵 ∖ (𝑈 ∪ { 0 })) ∈
V |
45 | 44 | rabex 5195 |
. . 3
⊢ {𝑝 ∈ (𝐵 ∖ (𝑈 ∪ { 0 })) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑝 ∥ (𝑥 · 𝑦) → (𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦))} ∈ V |
46 | 45 | a1i 11 |
. 2
⊢ (𝑅 ∈ 𝑉 → {𝑝 ∈ (𝐵 ∖ (𝑈 ∪ { 0 })) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑝 ∥ (𝑥 · 𝑦) → (𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦))} ∈ V) |
47 | 1, 41, 42, 46 | fvmptd3 6775 |
1
⊢ (𝑅 ∈ 𝑉 → (RPrime‘𝑅) = {𝑝 ∈ (𝐵 ∖ (𝑈 ∪ { 0 })) ∣ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑝 ∥ (𝑥 · 𝑦) → (𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦))}) |