Metamath Proof Explorer

Theorem opprdomn

Description: The opposite of a domain is also a domain. (Contributed by Mario Carneiro, 15-Jun-2015)

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

Proof

Step Hyp Ref Expression
1 opprdomn.1 ⊢ 𝑂 = ( oppr ‘ 𝑅 )
2 domnnzr ⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ NzRing )
3 1 opprnzr ⊢ ( 𝑅 ∈ NzRing → 𝑂 ∈ NzRing )
4 2 3 syl ⊢ ( 𝑅 ∈ Domn → 𝑂 ∈ NzRing )
5 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
7 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
8 5 6 7 domneq0 ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) ↔ ( 𝑦 = ( 0g ‘ 𝑅 ) ∨ 𝑥 = ( 0g ‘ 𝑅 ) ) ) )
9 8 3com23 ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) ↔ ( 𝑦 = ( 0g ‘ 𝑅 ) ∨ 𝑥 = ( 0g ‘ 𝑅 ) ) ) )
10 eqid ⊢ ( .r ‘ 𝑂 ) = ( .r ‘ 𝑂 )
11 5 6 1 10 opprmul ⊢ ( 𝑥 ( .r ‘ 𝑂 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 )
12 11 eqeq1i ⊢ ( ( 𝑥 ( .r ‘ 𝑂 ) 𝑦 ) = ( 0g ‘ 𝑅 ) ↔ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) )
13 orcom ⊢ ( ( 𝑥 = ( 0g ‘ 𝑅 ) ∨ 𝑦 = ( 0g ‘ 𝑅 ) ) ↔ ( 𝑦 = ( 0g ‘ 𝑅 ) ∨ 𝑥 = ( 0g ‘ 𝑅 ) ) )
14 9 12 13 3bitr4g ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑥 ( .r ‘ 𝑂 ) 𝑦 ) = ( 0g ‘ 𝑅 ) ↔ ( 𝑥 = ( 0g ‘ 𝑅 ) ∨ 𝑦 = ( 0g ‘ 𝑅 ) ) ) )
15 14 biimpd ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑥 ( .r ‘ 𝑂 ) 𝑦 ) = ( 0g ‘ 𝑅 ) → ( 𝑥 = ( 0g ‘ 𝑅 ) ∨ 𝑦 = ( 0g ‘ 𝑅 ) ) ) )
16 15 3expb ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑂 ) 𝑦 ) = ( 0g ‘ 𝑅 ) → ( 𝑥 = ( 0g ‘ 𝑅 ) ∨ 𝑦 = ( 0g ‘ 𝑅 ) ) ) )
17 16 ralrimivva ⊢ ( 𝑅 ∈ Domn → ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑂 ) 𝑦 ) = ( 0g ‘ 𝑅 ) → ( 𝑥 = ( 0g ‘ 𝑅 ) ∨ 𝑦 = ( 0g ‘ 𝑅 ) ) ) )
18 1 5 opprbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 )
19 1 7 oppr0 ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑂 )
20 18 10 19 isdomn ⊢ ( 𝑂 ∈ Domn ↔ ( 𝑂 ∈ NzRing ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑂 ) 𝑦 ) = ( 0g ‘ 𝑅 ) → ( 𝑥 = ( 0g ‘ 𝑅 ) ∨ 𝑦 = ( 0g ‘ 𝑅 ) ) ) ) )
21 4 17 20 sylanbrc ⊢ ( 𝑅 ∈ Domn → 𝑂 ∈ Domn )