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