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 ⊢ O = opp r ⁡ R
Assertion opprdomnb ⊢ R ∈ Domn ↔ O ∈ Domn

Proof

Step Hyp Ref Expression
1 opprdomn.1 ⊢ O = opp r ⁡ R
2 1 opprnzrb ⊢ R ∈ NzRing ↔ O ∈ NzRing
3 eqid ⊢ Base R = Base R
4 1 3 opprbas ⊢ Base R = Base O
5 eqid ⊢ ⋅ R = ⋅ R
6 eqid ⊢ ⋅ O = ⋅ O
7 3 5 1 6 opprmul ⊢ y ⋅ O x = x ⋅ R y
8 7 eqcomi ⊢ x ⋅ R y = y ⋅ O x
9 eqid ⊢ 0 R = 0 R
10 1 9 oppr0 ⊢ 0 R = 0 O
11 8 10 eqeq12i ⊢ x ⋅ R y = 0 R ↔ y ⋅ O x = 0 O
12 10 eqeq2i ⊢ x = 0 R ↔ x = 0 O
13 10 eqeq2i ⊢ y = 0 R ↔ y = 0 O
14 12 13 orbi12i ⊢ x = 0 R ∨ y = 0 R ↔ x = 0 O ∨ y = 0 O
15 orcom ⊢ x = 0 O ∨ y = 0 O ↔ y = 0 O ∨ x = 0 O
16 14 15 bitri ⊢ x = 0 R ∨ y = 0 R ↔ y = 0 O ∨ x = 0 O
17 11 16 imbi12i ⊢ x ⋅ R y = 0 R → x = 0 R ∨ y = 0 R ↔ y ⋅ O x = 0 O → y = 0 O ∨ x = 0 O
18 4 17 raleqbii ⊢ ∀ y ∈ Base R x ⋅ R y = 0 R → x = 0 R ∨ y = 0 R ↔ ∀ y ∈ Base O y ⋅ O x = 0 O → y = 0 O ∨ x = 0 O
19 4 18 raleqbii ⊢ ∀ x ∈ Base R ∀ y ∈ Base R x ⋅ R y = 0 R → x = 0 R ∨ y = 0 R ↔ ∀ x ∈ Base O ∀ y ∈ Base O y ⋅ O x = 0 O → y = 0 O ∨ x = 0 O
20 ralcom ⊢ ∀ x ∈ Base O ∀ y ∈ Base O y ⋅ O x = 0 O → y = 0 O ∨ x = 0 O ↔ ∀ y ∈ Base O ∀ x ∈ Base O y ⋅ O x = 0 O → y = 0 O ∨ x = 0 O
21 19 20 bitri ⊢ ∀ x ∈ Base R ∀ y ∈ Base R x ⋅ R y = 0 R → x = 0 R ∨ y = 0 R ↔ ∀ y ∈ Base O ∀ x ∈ Base O y ⋅ O x = 0 O → y = 0 O ∨ x = 0 O
22 2 21 anbi12i ⊢ R ∈ NzRing ∧ ∀ x ∈ Base R ∀ y ∈ Base R x ⋅ R y = 0 R → x = 0 R ∨ y = 0 R ↔ O ∈ NzRing ∧ ∀ y ∈ Base O ∀ x ∈ Base O y ⋅ O x = 0 O → y = 0 O ∨ x = 0 O
23 3 5 9 isdomn ⊢ R ∈ Domn ↔ R ∈ NzRing ∧ ∀ x ∈ Base R ∀ y ∈ Base R x ⋅ R y = 0 R → x = 0 R ∨ y = 0 R
24 eqid ⊢ Base O = Base O
25 eqid ⊢ 0 O = 0 O
26 24 6 25 isdomn ⊢ O ∈ Domn ↔ O ∈ NzRing ∧ ∀ y ∈ Base O ∀ x ∈ Base O y ⋅ O x = 0 O → y = 0 O ∨ x = 0 O
27 22 23 26 3bitr4i ⊢ R ∈ Domn ↔ O ∈ Domn