Theorem isdomn 20684

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.

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∨ wo 853   = wceq 1547   ∈ wcel 2119  ∀wral 3054  Vcvv 3432  [wsbc 3730  ‘cfv 6492  (class class class)co 7363  Basecbs 17177  ._rcmulr 17219  0_gc0g 17400  NzRingcnzr 20491  Domncdomn 20671

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-nul 5235

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rab 3393  df-v 3434  df-sbc 3731  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-ov 7366  df-domn 20674

This theorem is referenced by:  domnnzr  20685  domneq0  20687  isdomn2  20690  isdomn2OLD  20691  isdomn3  20694  isdomn4  20695  opprdomnb  20696  abvn0b  20815  znfld  21542  ply1domn  26114  fta1b  26162  domnpropd  33365  subrdom  33373  ricdomn1  33377  prmidl0  33540  qsidomlem2  33543  mplidomlem  33718