Step |
Hyp |
Ref |
Expression |
1 |
|
isirred2.1 |
⊢ 𝐵 = ( Base ‘ 𝑅 ) |
2 |
|
isirred2.2 |
⊢ 𝑈 = ( Unit ‘ 𝑅 ) |
3 |
|
isirred2.3 |
⊢ 𝐼 = ( Irred ‘ 𝑅 ) |
4 |
|
isirred2.4 |
⊢ · = ( .r ‘ 𝑅 ) |
5 |
|
eldif |
⊢ ( 𝑋 ∈ ( 𝐵 ∖ 𝑈 ) ↔ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ∈ 𝑈 ) ) |
6 |
|
eldif |
⊢ ( 𝑥 ∈ ( 𝐵 ∖ 𝑈 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝑈 ) ) |
7 |
|
eldif |
⊢ ( 𝑦 ∈ ( 𝐵 ∖ 𝑈 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ 𝑈 ) ) |
8 |
6 7
|
anbi12i |
⊢ ( ( 𝑥 ∈ ( 𝐵 ∖ 𝑈 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝑈 ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ 𝑈 ) ) ) |
9 |
|
an4 |
⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ 𝑈 ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ¬ 𝑥 ∈ 𝑈 ∧ ¬ 𝑦 ∈ 𝑈 ) ) ) |
10 |
8 9
|
bitri |
⊢ ( ( 𝑥 ∈ ( 𝐵 ∖ 𝑈 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝑈 ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ¬ 𝑥 ∈ 𝑈 ∧ ¬ 𝑦 ∈ 𝑈 ) ) ) |
11 |
10
|
imbi1i |
⊢ ( ( ( 𝑥 ∈ ( 𝐵 ∖ 𝑈 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝑈 ) ) → ( 𝑥 · 𝑦 ) ≠ 𝑋 ) ↔ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ¬ 𝑥 ∈ 𝑈 ∧ ¬ 𝑦 ∈ 𝑈 ) ) → ( 𝑥 · 𝑦 ) ≠ 𝑋 ) ) |
12 |
|
impexp |
⊢ ( ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ¬ 𝑥 ∈ 𝑈 ∧ ¬ 𝑦 ∈ 𝑈 ) ) → ( 𝑥 · 𝑦 ) ≠ 𝑋 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( ¬ 𝑥 ∈ 𝑈 ∧ ¬ 𝑦 ∈ 𝑈 ) → ( 𝑥 · 𝑦 ) ≠ 𝑋 ) ) ) |
13 |
|
pm4.56 |
⊢ ( ( ¬ 𝑥 ∈ 𝑈 ∧ ¬ 𝑦 ∈ 𝑈 ) ↔ ¬ ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) |
14 |
|
df-ne |
⊢ ( ( 𝑥 · 𝑦 ) ≠ 𝑋 ↔ ¬ ( 𝑥 · 𝑦 ) = 𝑋 ) |
15 |
13 14
|
imbi12i |
⊢ ( ( ( ¬ 𝑥 ∈ 𝑈 ∧ ¬ 𝑦 ∈ 𝑈 ) → ( 𝑥 · 𝑦 ) ≠ 𝑋 ) ↔ ( ¬ ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) → ¬ ( 𝑥 · 𝑦 ) = 𝑋 ) ) |
16 |
|
con34b |
⊢ ( ( ( 𝑥 · 𝑦 ) = 𝑋 → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) ↔ ( ¬ ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) → ¬ ( 𝑥 · 𝑦 ) = 𝑋 ) ) |
17 |
15 16
|
bitr4i |
⊢ ( ( ( ¬ 𝑥 ∈ 𝑈 ∧ ¬ 𝑦 ∈ 𝑈 ) → ( 𝑥 · 𝑦 ) ≠ 𝑋 ) ↔ ( ( 𝑥 · 𝑦 ) = 𝑋 → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) ) |
18 |
17
|
imbi2i |
⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( ¬ 𝑥 ∈ 𝑈 ∧ ¬ 𝑦 ∈ 𝑈 ) → ( 𝑥 · 𝑦 ) ≠ 𝑋 ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 · 𝑦 ) = 𝑋 → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) ) ) |
19 |
12 18
|
bitri |
⊢ ( ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ¬ 𝑥 ∈ 𝑈 ∧ ¬ 𝑦 ∈ 𝑈 ) ) → ( 𝑥 · 𝑦 ) ≠ 𝑋 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 · 𝑦 ) = 𝑋 → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) ) ) |
20 |
11 19
|
bitri |
⊢ ( ( ( 𝑥 ∈ ( 𝐵 ∖ 𝑈 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝑈 ) ) → ( 𝑥 · 𝑦 ) ≠ 𝑋 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 · 𝑦 ) = 𝑋 → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) ) ) |
21 |
20
|
2albii |
⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ ( 𝐵 ∖ 𝑈 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝑈 ) ) → ( 𝑥 · 𝑦 ) ≠ 𝑋 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 · 𝑦 ) = 𝑋 → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) ) ) |
22 |
|
r2al |
⊢ ( ∀ 𝑥 ∈ ( 𝐵 ∖ 𝑈 ) ∀ 𝑦 ∈ ( 𝐵 ∖ 𝑈 ) ( 𝑥 · 𝑦 ) ≠ 𝑋 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ ( 𝐵 ∖ 𝑈 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝑈 ) ) → ( 𝑥 · 𝑦 ) ≠ 𝑋 ) ) |
23 |
|
r2al |
⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 𝑋 → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 · 𝑦 ) = 𝑋 → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) ) ) |
24 |
21 22 23
|
3bitr4i |
⊢ ( ∀ 𝑥 ∈ ( 𝐵 ∖ 𝑈 ) ∀ 𝑦 ∈ ( 𝐵 ∖ 𝑈 ) ( 𝑥 · 𝑦 ) ≠ 𝑋 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 𝑋 → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) ) |
25 |
5 24
|
anbi12i |
⊢ ( ( 𝑋 ∈ ( 𝐵 ∖ 𝑈 ) ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ 𝑈 ) ∀ 𝑦 ∈ ( 𝐵 ∖ 𝑈 ) ( 𝑥 · 𝑦 ) ≠ 𝑋 ) ↔ ( ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ∈ 𝑈 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 𝑋 → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) ) ) |
26 |
|
eqid |
⊢ ( 𝐵 ∖ 𝑈 ) = ( 𝐵 ∖ 𝑈 ) |
27 |
1 2 3 26 4
|
isirred |
⊢ ( 𝑋 ∈ 𝐼 ↔ ( 𝑋 ∈ ( 𝐵 ∖ 𝑈 ) ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ 𝑈 ) ∀ 𝑦 ∈ ( 𝐵 ∖ 𝑈 ) ( 𝑥 · 𝑦 ) ≠ 𝑋 ) ) |
28 |
|
df-3an |
⊢ ( ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ∈ 𝑈 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 𝑋 → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) ) ↔ ( ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ∈ 𝑈 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 𝑋 → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) ) ) |
29 |
25 27 28
|
3bitr4i |
⊢ ( 𝑋 ∈ 𝐼 ↔ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ∈ 𝑈 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 𝑋 → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) ) ) |