ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  isdomn GIF version

Theorem isdomn 13743
Description: Expand definition of a domain. (Contributed by Mario Carneiro, 28-Mar-2015.)
Hypotheses
Ref Expression
isdomn.b 𝐵 = (Base‘𝑅)
isdomn.t · = (.r𝑅)
isdomn.z 0 = (0g𝑅)
Assertion
Ref Expression
isdomn (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ ∀𝑥𝐵𝑦𝐵 ((𝑥 · 𝑦) = 0 → (𝑥 = 0𝑦 = 0 ))))
Distinct variable groups:   𝑥,𝐵,𝑦   𝑥,𝑅,𝑦   𝑥, 0 ,𝑦
Allowed substitution hints:   · (𝑥,𝑦)

Proof of Theorem isdomn
Dummy variables 𝑏 𝑟 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 basfn 12663 . . . . 5 Base Fn V
2 vex 2763 . . . . 5 𝑟 ∈ V
3 funfvex 5563 . . . . . 6 ((Fun Base ∧ 𝑟 ∈ dom Base) → (Base‘𝑟) ∈ V)
43funfni 5346 . . . . 5 ((Base Fn V ∧ 𝑟 ∈ V) → (Base‘𝑟) ∈ V)
51, 2, 4mp2an 426 . . . 4 (Base‘𝑟) ∈ V
65a1i 9 . . 3 (𝑟 = 𝑅 → (Base‘𝑟) ∈ V)
7 fveq2 5546 . . . 4 (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅))
8 isdomn.b . . . 4 𝐵 = (Base‘𝑅)
97, 8eqtr4di 2244 . . 3 (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵)
10 fn0g 12945 . . . . . 6 0g Fn V
11 funfvex 5563 . . . . . . 7 ((Fun 0g𝑟 ∈ dom 0g) → (0g𝑟) ∈ V)
1211funfni 5346 . . . . . 6 ((0g Fn V ∧ 𝑟 ∈ V) → (0g𝑟) ∈ V)
1310, 2, 12mp2an 426 . . . . 5 (0g𝑟) ∈ V
1413a1i 9 . . . 4 ((𝑟 = 𝑅𝑏 = 𝐵) → (0g𝑟) ∈ V)
15 fveq2 5546 . . . . . 6 (𝑟 = 𝑅 → (0g𝑟) = (0g𝑅))
1615adantr 276 . . . . 5 ((𝑟 = 𝑅𝑏 = 𝐵) → (0g𝑟) = (0g𝑅))
17 isdomn.z . . . . 5 0 = (0g𝑅)
1816, 17eqtr4di 2244 . . . 4 ((𝑟 = 𝑅𝑏 = 𝐵) → (0g𝑟) = 0 )
19 simplr 528 . . . . 5 (((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑧 = 0 ) → 𝑏 = 𝐵)
20 fveq2 5546 . . . . . . . . . 10 (𝑟 = 𝑅 → (.r𝑟) = (.r𝑅))
21 isdomn.t . . . . . . . . . 10 · = (.r𝑅)
2220, 21eqtr4di 2244 . . . . . . . . 9 (𝑟 = 𝑅 → (.r𝑟) = · )
2322oveqdr 5938 . . . . . . . 8 ((𝑟 = 𝑅𝑏 = 𝐵) → (𝑥(.r𝑟)𝑦) = (𝑥 · 𝑦))
24 id 19 . . . . . . . 8 (𝑧 = 0𝑧 = 0 )
2523, 24eqeqan12d 2209 . . . . . . 7 (((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑧 = 0 ) → ((𝑥(.r𝑟)𝑦) = 𝑧 ↔ (𝑥 · 𝑦) = 0 ))
26 eqeq2 2203 . . . . . . . . 9 (𝑧 = 0 → (𝑥 = 𝑧𝑥 = 0 ))
27 eqeq2 2203 . . . . . . . . 9 (𝑧 = 0 → (𝑦 = 𝑧𝑦 = 0 ))
2826, 27orbi12d 794 . . . . . . . 8 (𝑧 = 0 → ((𝑥 = 𝑧𝑦 = 𝑧) ↔ (𝑥 = 0𝑦 = 0 )))
2928adantl 277 . . . . . . 7 (((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑧 = 0 ) → ((𝑥 = 𝑧𝑦 = 𝑧) ↔ (𝑥 = 0𝑦 = 0 )))
3025, 29imbi12d 234 . . . . . 6 (((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑧 = 0 ) → (((𝑥(.r𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧𝑦 = 𝑧)) ↔ ((𝑥 · 𝑦) = 0 → (𝑥 = 0𝑦 = 0 ))))
3119, 30raleqbidv 2706 . . . . 5 (((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑧 = 0 ) → (∀𝑦𝑏 ((𝑥(.r𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧𝑦 = 𝑧)) ↔ ∀𝑦𝐵 ((𝑥 · 𝑦) = 0 → (𝑥 = 0𝑦 = 0 ))))
3219, 31raleqbidv 2706 . . . 4 (((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑧 = 0 ) → (∀𝑥𝑏𝑦𝑏 ((𝑥(.r𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧𝑦 = 𝑧)) ↔ ∀𝑥𝐵𝑦𝐵 ((𝑥 · 𝑦) = 0 → (𝑥 = 0𝑦 = 0 ))))
3314, 18, 32sbcied2 3023 . . 3 ((𝑟 = 𝑅𝑏 = 𝐵) → ([(0g𝑟) / 𝑧]𝑥𝑏𝑦𝑏 ((𝑥(.r𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧𝑦 = 𝑧)) ↔ ∀𝑥𝐵𝑦𝐵 ((𝑥 · 𝑦) = 0 → (𝑥 = 0𝑦 = 0 ))))
346, 9, 33sbcied2 3023 . 2 (𝑟 = 𝑅 → ([(Base‘𝑟) / 𝑏][(0g𝑟) / 𝑧]𝑥𝑏𝑦𝑏 ((𝑥(.r𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧𝑦 = 𝑧)) ↔ ∀𝑥𝐵𝑦𝐵 ((𝑥 · 𝑦) = 0 → (𝑥 = 0𝑦 = 0 ))))
35 df-domn 13733 . 2 Domn = {𝑟 ∈ NzRing ∣ [(Base‘𝑟) / 𝑏][(0g𝑟) / 𝑧]𝑥𝑏𝑦𝑏 ((𝑥(.r𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧𝑦 = 𝑧))}
3634, 35elrab2 2919 1 (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ ∀𝑥𝐵𝑦𝐵 ((𝑥 · 𝑦) = 0 → (𝑥 = 0𝑦 = 0 ))))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  wo 709   = wceq 1364  wcel 2164  wral 2472  Vcvv 2760  [wsbc 2985   Fn wfn 5241  cfv 5246  (class class class)co 5910  Basecbs 12605  .rcmulr 12683  0gc0g 12854  NzRingcnzr 13653  Domncdomn 13730
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-pow 4203  ax-pr 4238  ax-un 4462  ax-cnex 7953  ax-resscn 7954  ax-1re 7956  ax-addrcl 7959
This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-rab 2481  df-v 2762  df-sbc 2986  df-un 3157  df-in 3159  df-ss 3166  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-int 3871  df-br 4030  df-opab 4091  df-mpt 4092  df-id 4322  df-xp 4661  df-rel 4662  df-cnv 4663  df-co 4664  df-dm 4665  df-rn 4666  df-res 4667  df-iota 5207  df-fun 5248  df-fn 5249  df-fv 5254  df-riota 5865  df-ov 5913  df-inn 8973  df-ndx 12608  df-slot 12609  df-base 12611  df-0g 12856  df-domn 13733
This theorem is referenced by:  domnnzr  13744  domneq0  13746  opprdomnbg  13748  znidom  14116
  Copyright terms: Public domain W3C validator