Metamath Proof Explorer

Theorem opprirred

Description: Irreducibility is symmetric, so the irreducible elements of the opposite ring are the same as the original ring. (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Hypotheses opprirred.1 ⊢ 𝑆 = ( oppr ‘ 𝑅 )
opprirred.2 ⊢ 𝐼 = ( Irred ‘ 𝑅 )
Assertion opprirred 𝐼 = ( Irred ‘ 𝑆 )

Proof

Step Hyp Ref Expression
1 opprirred.1 ⊢ 𝑆 = ( oppr ‘ 𝑅 )
2 opprirred.2 ⊢ 𝐼 = ( Irred ‘ 𝑅 )
3 ralcom ⊢ ( ∀ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ∀ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) ≠ 𝑥 ↔ ∀ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ∀ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) ≠ 𝑥 )
4 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
6 eqid ⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
7 4 5 1 6 opprmul ⊢ ( 𝑦 ( .r ‘ 𝑆 ) 𝑧 ) = ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 )
8 7 neeq1i ⊢ ( ( 𝑦 ( .r ‘ 𝑆 ) 𝑧 ) ≠ 𝑥 ↔ ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) ≠ 𝑥 )
9 8 2ralbii ⊢ ( ∀ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ∀ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ( 𝑦 ( .r ‘ 𝑆 ) 𝑧 ) ≠ 𝑥 ↔ ∀ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ∀ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) ≠ 𝑥 )
10 3 9 bitr4i ⊢ ( ∀ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ∀ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) ≠ 𝑥 ↔ ∀ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ∀ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ( 𝑦 ( .r ‘ 𝑆 ) 𝑧 ) ≠ 𝑥 )
11 10 anbi2i ⊢ ( ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ∧ ∀ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ∀ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) ≠ 𝑥 ) ↔ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ∧ ∀ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ∀ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ( 𝑦 ( .r ‘ 𝑆 ) 𝑧 ) ≠ 𝑥 ) )
12 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
13 eqid ⊢ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) = ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) )
14 4 12 2 13 5 isirred ⊢ ( 𝑥 ∈ 𝐼 ↔ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ∧ ∀ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ∀ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) ≠ 𝑥 ) )
15 1 4 opprbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑆 )
16 12 1 opprunit ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑆 )
17 eqid ⊢ ( Irred ‘ 𝑆 ) = ( Irred ‘ 𝑆 )
18 15 16 17 13 6 isirred ⊢ ( 𝑥 ∈ ( Irred ‘ 𝑆 ) ↔ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ∧ ∀ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ∀ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ( 𝑦 ( .r ‘ 𝑆 ) 𝑧 ) ≠ 𝑥 ) )
19 11 14 18 3bitr4i ⊢ ( 𝑥 ∈ 𝐼 ↔ 𝑥 ∈ ( Irred ‘ 𝑆 ) )
20 19 eqriv ⊢ 𝐼 = ( Irred ‘ 𝑆 )