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 ‘ 𝑆 )