Step |
Hyp |
Ref |
Expression |
0 |
|
cir |
⊢ Irred |
1 |
|
vw |
⊢ 𝑤 |
2 |
|
cvv |
⊢ V |
3 |
|
cbs |
⊢ Base |
4 |
1
|
cv |
⊢ 𝑤 |
5 |
4 3
|
cfv |
⊢ ( Base ‘ 𝑤 ) |
6 |
|
cui |
⊢ Unit |
7 |
4 6
|
cfv |
⊢ ( Unit ‘ 𝑤 ) |
8 |
5 7
|
cdif |
⊢ ( ( Base ‘ 𝑤 ) ∖ ( Unit ‘ 𝑤 ) ) |
9 |
|
vb |
⊢ 𝑏 |
10 |
|
vz |
⊢ 𝑧 |
11 |
9
|
cv |
⊢ 𝑏 |
12 |
|
vx |
⊢ 𝑥 |
13 |
|
vy |
⊢ 𝑦 |
14 |
12
|
cv |
⊢ 𝑥 |
15 |
|
cmulr |
⊢ .r |
16 |
4 15
|
cfv |
⊢ ( .r ‘ 𝑤 ) |
17 |
13
|
cv |
⊢ 𝑦 |
18 |
14 17 16
|
co |
⊢ ( 𝑥 ( .r ‘ 𝑤 ) 𝑦 ) |
19 |
10
|
cv |
⊢ 𝑧 |
20 |
18 19
|
wne |
⊢ ( 𝑥 ( .r ‘ 𝑤 ) 𝑦 ) ≠ 𝑧 |
21 |
20 13 11
|
wral |
⊢ ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑤 ) 𝑦 ) ≠ 𝑧 |
22 |
21 12 11
|
wral |
⊢ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑤 ) 𝑦 ) ≠ 𝑧 |
23 |
22 10 11
|
crab |
⊢ { 𝑧 ∈ 𝑏 ∣ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑤 ) 𝑦 ) ≠ 𝑧 } |
24 |
9 8 23
|
csb |
⊢ ⦋ ( ( Base ‘ 𝑤 ) ∖ ( Unit ‘ 𝑤 ) ) / 𝑏 ⦌ { 𝑧 ∈ 𝑏 ∣ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑤 ) 𝑦 ) ≠ 𝑧 } |
25 |
1 2 24
|
cmpt |
⊢ ( 𝑤 ∈ V ↦ ⦋ ( ( Base ‘ 𝑤 ) ∖ ( Unit ‘ 𝑤 ) ) / 𝑏 ⦌ { 𝑧 ∈ 𝑏 ∣ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑤 ) 𝑦 ) ≠ 𝑧 } ) |
26 |
0 25
|
wceq |
⊢ Irred = ( 𝑤 ∈ V ↦ ⦋ ( ( Base ‘ 𝑤 ) ∖ ( Unit ‘ 𝑤 ) ) / 𝑏 ⦌ { 𝑧 ∈ 𝑏 ∣ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑤 ) 𝑦 ) ≠ 𝑧 } ) |