Metamath Proof Explorer

Theorem isdomn

Description: Expand definition of a domain. (Contributed by Mario Carneiro, 28-Mar-2015)

Ref Expression
Hypotheses isdomn.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
isdomn.t ⊢ · = ( .r ‘ 𝑅 )
isdomn.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion isdomn ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ NzRing ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ) )

Proof

Step Hyp Ref Expression
1 isdomn.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 isdomn.t ⊢ · = ( .r ‘ 𝑅 )
3 isdomn.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 fvexd ⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) ∈ V )
5 fveq2 ⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
6 5 1 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = 𝐵 )
7 fvexd ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) → ( 0g ‘ 𝑟 ) ∈ V )
8 fveq2 ⊢ ( 𝑟 = 𝑅 → ( 0g ‘ 𝑟 ) = ( 0g ‘ 𝑅 ) )
9 8 adantr ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) → ( 0g ‘ 𝑟 ) = ( 0g ‘ 𝑅 ) )
10 9 3 eqtr4di ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) → ( 0g ‘ 𝑟 ) = 0 )
11 simplr ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑧 = 0 ) → 𝑏 = 𝐵 )
12 fveq2 ⊢ ( 𝑟 = 𝑅 → ( .r ‘ 𝑟 ) = ( .r ‘ 𝑅 ) )
13 12 2 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( .r ‘ 𝑟 ) = · )
14 13 oveqdr ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) → ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) = ( 𝑥 · 𝑦 ) )
15 id ⊢ ( 𝑧 = 0 → 𝑧 = 0 )
16 14 15 eqeqan12d ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑧 = 0 ) → ( ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) = 𝑧 ↔ ( 𝑥 · 𝑦 ) = 0 ) )
17 eqeq2 ⊢ ( 𝑧 = 0 → ( 𝑥 = 𝑧 ↔ 𝑥 = 0 ) )
18 eqeq2 ⊢ ( 𝑧 = 0 → ( 𝑦 = 𝑧 ↔ 𝑦 = 0 ) )
19 17 18 orbi12d ⊢ ( 𝑧 = 0 → ( ( 𝑥 = 𝑧 ∨ 𝑦 = 𝑧 ) ↔ ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) )
20 19 adantl ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑧 = 0 ) → ( ( 𝑥 = 𝑧 ∨ 𝑦 = 𝑧 ) ↔ ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) )
21 16 20 imbi12d ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑧 = 0 ) → ( ( ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) = 𝑧 → ( 𝑥 = 𝑧 ∨ 𝑦 = 𝑧 ) ) ↔ ( ( 𝑥 · 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ) )
22 11 21 raleqbidv ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑧 = 0 ) → ( ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) = 𝑧 → ( 𝑥 = 𝑧 ∨ 𝑦 = 𝑧 ) ) ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ) )
23 11 22 raleqbidv ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑧 = 0 ) → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) = 𝑧 → ( 𝑥 = 𝑧 ∨ 𝑦 = 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ) )
24 7 10 23 sbcied2 ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) → ( [ ( 0g ‘ 𝑟 ) / 𝑧 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) = 𝑧 → ( 𝑥 = 𝑧 ∨ 𝑦 = 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ) )
25 4 6 24 sbcied2 ⊢ ( 𝑟 = 𝑅 → ( [ ( Base ‘ 𝑟 ) / 𝑏 ] [ ( 0g ‘ 𝑟 ) / 𝑧 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) = 𝑧 → ( 𝑥 = 𝑧 ∨ 𝑦 = 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ) )
26 df-domn ⊢ Domn = { 𝑟 ∈ NzRing ∣ [ ( Base ‘ 𝑟 ) / 𝑏 ] [ ( 0g ‘ 𝑟 ) / 𝑧 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) = 𝑧 → ( 𝑥 = 𝑧 ∨ 𝑦 = 𝑧 ) ) }
27 25 26 elrab2 ⊢ ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ NzRing ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ) )