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