Step |
Hyp |
Ref |
Expression |
1 |
|
irred.1 |
⊢ 𝐵 = ( Base ‘ 𝑅 ) |
2 |
|
irred.2 |
⊢ 𝑈 = ( Unit ‘ 𝑅 ) |
3 |
|
irred.3 |
⊢ 𝐼 = ( Irred ‘ 𝑅 ) |
4 |
|
irred.4 |
⊢ 𝑁 = ( 𝐵 ∖ 𝑈 ) |
5 |
|
irred.5 |
⊢ · = ( .r ‘ 𝑅 ) |
6 |
|
elfvdm |
⊢ ( 𝑋 ∈ ( Irred ‘ 𝑅 ) → 𝑅 ∈ dom Irred ) |
7 |
6 3
|
eleq2s |
⊢ ( 𝑋 ∈ 𝐼 → 𝑅 ∈ dom Irred ) |
8 |
7
|
elexd |
⊢ ( 𝑋 ∈ 𝐼 → 𝑅 ∈ V ) |
9 |
|
eldifi |
⊢ ( 𝑋 ∈ ( 𝐵 ∖ 𝑈 ) → 𝑋 ∈ 𝐵 ) |
10 |
9 4
|
eleq2s |
⊢ ( 𝑋 ∈ 𝑁 → 𝑋 ∈ 𝐵 ) |
11 |
10 1
|
eleqtrdi |
⊢ ( 𝑋 ∈ 𝑁 → 𝑋 ∈ ( Base ‘ 𝑅 ) ) |
12 |
11
|
elfvexd |
⊢ ( 𝑋 ∈ 𝑁 → 𝑅 ∈ V ) |
13 |
12
|
adantr |
⊢ ( ( 𝑋 ∈ 𝑁 ∧ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑋 ) → 𝑅 ∈ V ) |
14 |
|
fvex |
⊢ ( Base ‘ 𝑟 ) ∈ V |
15 |
|
difexg |
⊢ ( ( Base ‘ 𝑟 ) ∈ V → ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ∈ V ) |
16 |
14 15
|
mp1i |
⊢ ( 𝑟 = 𝑅 → ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ∈ V ) |
17 |
|
simpr |
⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) |
18 |
|
simpl |
⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → 𝑟 = 𝑅 ) |
19 |
18
|
fveq2d |
⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) ) |
20 |
19 1
|
eqtr4di |
⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( Base ‘ 𝑟 ) = 𝐵 ) |
21 |
18
|
fveq2d |
⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( Unit ‘ 𝑟 ) = ( Unit ‘ 𝑅 ) ) |
22 |
21 2
|
eqtr4di |
⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( Unit ‘ 𝑟 ) = 𝑈 ) |
23 |
20 22
|
difeq12d |
⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) = ( 𝐵 ∖ 𝑈 ) ) |
24 |
23 4
|
eqtr4di |
⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) = 𝑁 ) |
25 |
17 24
|
eqtrd |
⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → 𝑏 = 𝑁 ) |
26 |
18
|
fveq2d |
⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( .r ‘ 𝑟 ) = ( .r ‘ 𝑅 ) ) |
27 |
26 5
|
eqtr4di |
⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( .r ‘ 𝑟 ) = · ) |
28 |
27
|
oveqd |
⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) = ( 𝑥 · 𝑦 ) ) |
29 |
28
|
neeq1d |
⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ≠ 𝑧 ↔ ( 𝑥 · 𝑦 ) ≠ 𝑧 ) ) |
30 |
25 29
|
raleqbidv |
⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ≠ 𝑧 ↔ ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑧 ) ) |
31 |
25 30
|
raleqbidv |
⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ≠ 𝑧 ↔ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑧 ) ) |
32 |
25 31
|
rabeqbidv |
⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → { 𝑧 ∈ 𝑏 ∣ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ≠ 𝑧 } = { 𝑧 ∈ 𝑁 ∣ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑧 } ) |
33 |
16 32
|
csbied |
⊢ ( 𝑟 = 𝑅 → ⦋ ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) / 𝑏 ⦌ { 𝑧 ∈ 𝑏 ∣ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ≠ 𝑧 } = { 𝑧 ∈ 𝑁 ∣ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑧 } ) |
34 |
|
df-irred |
⊢ Irred = ( 𝑟 ∈ V ↦ ⦋ ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) / 𝑏 ⦌ { 𝑧 ∈ 𝑏 ∣ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ≠ 𝑧 } ) |
35 |
|
fvex |
⊢ ( Base ‘ 𝑅 ) ∈ V |
36 |
1 35
|
eqeltri |
⊢ 𝐵 ∈ V |
37 |
36
|
difexi |
⊢ ( 𝐵 ∖ 𝑈 ) ∈ V |
38 |
4 37
|
eqeltri |
⊢ 𝑁 ∈ V |
39 |
38
|
rabex |
⊢ { 𝑧 ∈ 𝑁 ∣ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑧 } ∈ V |
40 |
33 34 39
|
fvmpt |
⊢ ( 𝑅 ∈ V → ( Irred ‘ 𝑅 ) = { 𝑧 ∈ 𝑁 ∣ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑧 } ) |
41 |
3 40
|
eqtrid |
⊢ ( 𝑅 ∈ V → 𝐼 = { 𝑧 ∈ 𝑁 ∣ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑧 } ) |
42 |
41
|
eleq2d |
⊢ ( 𝑅 ∈ V → ( 𝑋 ∈ 𝐼 ↔ 𝑋 ∈ { 𝑧 ∈ 𝑁 ∣ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑧 } ) ) |
43 |
|
neeq2 |
⊢ ( 𝑧 = 𝑋 → ( ( 𝑥 · 𝑦 ) ≠ 𝑧 ↔ ( 𝑥 · 𝑦 ) ≠ 𝑋 ) ) |
44 |
43
|
2ralbidv |
⊢ ( 𝑧 = 𝑋 → ( ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑧 ↔ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑋 ) ) |
45 |
44
|
elrab |
⊢ ( 𝑋 ∈ { 𝑧 ∈ 𝑁 ∣ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑧 } ↔ ( 𝑋 ∈ 𝑁 ∧ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑋 ) ) |
46 |
42 45
|
bitrdi |
⊢ ( 𝑅 ∈ V → ( 𝑋 ∈ 𝐼 ↔ ( 𝑋 ∈ 𝑁 ∧ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑋 ) ) ) |
47 |
8 13 46
|
pm5.21nii |
⊢ ( 𝑋 ∈ 𝐼 ↔ ( 𝑋 ∈ 𝑁 ∧ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑋 ) ) |