Metamath Proof Explorer

Theorem opprdomnb

Description: A class is a domain if and only if its opposite is a domain, biconditional form of opprdomn . (Contributed by SN, 15-Jun-2015)

Ref Expression
Hypothesis opprdomn.1 ⊢ 𝑂 = ( oppr ‘ 𝑅 )
Assertion opprdomnb ( 𝑅 ∈ Domn ↔ 𝑂 ∈ Domn )

Proof

Step Hyp Ref Expression
1 opprdomn.1 ⊢ 𝑂 = ( oppr ‘ 𝑅 )
2 1 opprnzrb ⊢ ( 𝑅 ∈ NzRing ↔ 𝑂 ∈ NzRing )
3 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4 1 3 opprbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 )
5 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
6 eqid ⊢ ( .r ‘ 𝑂 ) = ( .r ‘ 𝑂 )
7 3 5 1 6 opprmul ⊢ ( 𝑦 ( .r ‘ 𝑂 ) 𝑥 ) = ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 )
8 7 eqcomi ⊢ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝑂 ) 𝑥 )
9 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
10 1 9 oppr0 ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑂 )
11 8 10 eqeq12i ⊢ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 0g ‘ 𝑅 ) ↔ ( 𝑦 ( .r ‘ 𝑂 ) 𝑥 ) = ( 0g ‘ 𝑂 ) )
12 10 eqeq2i ⊢ ( 𝑥 = ( 0g ‘ 𝑅 ) ↔ 𝑥 = ( 0g ‘ 𝑂 ) )
13 10 eqeq2i ⊢ ( 𝑦 = ( 0g ‘ 𝑅 ) ↔ 𝑦 = ( 0g ‘ 𝑂 ) )
14 12 13 orbi12i ⊢ ( ( 𝑥 = ( 0g ‘ 𝑅 ) ∨ 𝑦 = ( 0g ‘ 𝑅 ) ) ↔ ( 𝑥 = ( 0g ‘ 𝑂 ) ∨ 𝑦 = ( 0g ‘ 𝑂 ) ) )
15 orcom ⊢ ( ( 𝑥 = ( 0g ‘ 𝑂 ) ∨ 𝑦 = ( 0g ‘ 𝑂 ) ) ↔ ( 𝑦 = ( 0g ‘ 𝑂 ) ∨ 𝑥 = ( 0g ‘ 𝑂 ) ) )
16 14 15 bitri ⊢ ( ( 𝑥 = ( 0g ‘ 𝑅 ) ∨ 𝑦 = ( 0g ‘ 𝑅 ) ) ↔ ( 𝑦 = ( 0g ‘ 𝑂 ) ∨ 𝑥 = ( 0g ‘ 𝑂 ) ) )
17 11 16 imbi12i ⊢ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 0g ‘ 𝑅 ) → ( 𝑥 = ( 0g ‘ 𝑅 ) ∨ 𝑦 = ( 0g ‘ 𝑅 ) ) ) ↔ ( ( 𝑦 ( .r ‘ 𝑂 ) 𝑥 ) = ( 0g ‘ 𝑂 ) → ( 𝑦 = ( 0g ‘ 𝑂 ) ∨ 𝑥 = ( 0g ‘ 𝑂 ) ) ) )
18 4 17 raleqbii ⊢ ( ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 0g ‘ 𝑅 ) → ( 𝑥 = ( 0g ‘ 𝑅 ) ∨ 𝑦 = ( 0g ‘ 𝑅 ) ) ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝑂 ) ( ( 𝑦 ( .r ‘ 𝑂 ) 𝑥 ) = ( 0g ‘ 𝑂 ) → ( 𝑦 = ( 0g ‘ 𝑂 ) ∨ 𝑥 = ( 0g ‘ 𝑂 ) ) ) )
19 4 18 raleqbii ⊢ ( ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 0g ‘ 𝑅 ) → ( 𝑥 = ( 0g ‘ 𝑅 ) ∨ 𝑦 = ( 0g ‘ 𝑅 ) ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑂 ) ∀ 𝑦 ∈ ( Base ‘ 𝑂 ) ( ( 𝑦 ( .r ‘ 𝑂 ) 𝑥 ) = ( 0g ‘ 𝑂 ) → ( 𝑦 = ( 0g ‘ 𝑂 ) ∨ 𝑥 = ( 0g ‘ 𝑂 ) ) ) )
20 ralcom ⊢ ( ∀ 𝑥 ∈ ( Base ‘ 𝑂 ) ∀ 𝑦 ∈ ( Base ‘ 𝑂 ) ( ( 𝑦 ( .r ‘ 𝑂 ) 𝑥 ) = ( 0g ‘ 𝑂 ) → ( 𝑦 = ( 0g ‘ 𝑂 ) ∨ 𝑥 = ( 0g ‘ 𝑂 ) ) ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝑂 ) ∀ 𝑥 ∈ ( Base ‘ 𝑂 ) ( ( 𝑦 ( .r ‘ 𝑂 ) 𝑥 ) = ( 0g ‘ 𝑂 ) → ( 𝑦 = ( 0g ‘ 𝑂 ) ∨ 𝑥 = ( 0g ‘ 𝑂 ) ) ) )
21 19 20 bitri ⊢ ( ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 0g ‘ 𝑅 ) → ( 𝑥 = ( 0g ‘ 𝑅 ) ∨ 𝑦 = ( 0g ‘ 𝑅 ) ) ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝑂 ) ∀ 𝑥 ∈ ( Base ‘ 𝑂 ) ( ( 𝑦 ( .r ‘ 𝑂 ) 𝑥 ) = ( 0g ‘ 𝑂 ) → ( 𝑦 = ( 0g ‘ 𝑂 ) ∨ 𝑥 = ( 0g ‘ 𝑂 ) ) ) )
22 2 21 anbi12i ⊢ ( ( 𝑅 ∈ NzRing ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 0g ‘ 𝑅 ) → ( 𝑥 = ( 0g ‘ 𝑅 ) ∨ 𝑦 = ( 0g ‘ 𝑅 ) ) ) ) ↔ ( 𝑂 ∈ NzRing ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑂 ) ∀ 𝑥 ∈ ( Base ‘ 𝑂 ) ( ( 𝑦 ( .r ‘ 𝑂 ) 𝑥 ) = ( 0g ‘ 𝑂 ) → ( 𝑦 = ( 0g ‘ 𝑂 ) ∨ 𝑥 = ( 0g ‘ 𝑂 ) ) ) ) )
23 3 5 9 isdomn ⊢ ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ NzRing ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 0g ‘ 𝑅 ) → ( 𝑥 = ( 0g ‘ 𝑅 ) ∨ 𝑦 = ( 0g ‘ 𝑅 ) ) ) ) )
24 eqid ⊢ ( Base ‘ 𝑂 ) = ( Base ‘ 𝑂 )
25 eqid ⊢ ( 0g ‘ 𝑂 ) = ( 0g ‘ 𝑂 )
26 24 6 25 isdomn ⊢ ( 𝑂 ∈ Domn ↔ ( 𝑂 ∈ NzRing ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑂 ) ∀ 𝑥 ∈ ( Base ‘ 𝑂 ) ( ( 𝑦 ( .r ‘ 𝑂 ) 𝑥 ) = ( 0g ‘ 𝑂 ) → ( 𝑦 = ( 0g ‘ 𝑂 ) ∨ 𝑥 = ( 0g ‘ 𝑂 ) ) ) ) )
27 22 23 26 3bitr4i ⊢ ( 𝑅 ∈ Domn ↔ 𝑂 ∈ Domn )