Metamath Proof Explorer

Theorem isirred2

Description: Expand out the class difference from isirred . (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Hypotheses isirred2.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
isirred2.2 ⊢ 𝑈 = ( Unit ‘ 𝑅 )
isirred2.3 ⊢ 𝐼 = ( Irred ‘ 𝑅 )
isirred2.4 ⊢ · = ( .r ‘ 𝑅 )
Assertion isirred2 ( 𝑋 ∈ 𝐼 ↔ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ∈ 𝑈 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 𝑋 → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) ) )

Proof

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 ⊢ ( 𝑋 ∈ 𝐼 ↔ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ∈ 𝑈 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 𝑋 → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) ) )