Theorem isdomn 20685

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 6918	. . 3 ⊢ (𝑟 = 𝑅 → (Base‘𝑟) ∈ V)
2		fveq2 6903	. . . 4 ⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅))
3		isdomn.b	. . . 4 ⊢ 𝐵 = (Base‘𝑅)
4	2, 3	eqtr4di 2784	. . 3 ⊢ (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵)
5		fvexd 6918	. . . 4 ⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → (0g‘𝑟) ∈ V)
6		fveq2 6903	. . . . . 6 ⊢ (𝑟 = 𝑅 → (0g‘𝑟) = (0g‘𝑅))
7	6	adantr 479	. . . . 5 ⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → (0g‘𝑟) = (0g‘𝑅))
8		isdomn.z	. . . . 5 ⊢ 0 = (0g‘𝑅)
9	7, 8	eqtr4di 2784	. . . 4 ⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → (0g‘𝑟) = 0 )
10		simplr 767	. . . . 5 ⊢ (((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑧 = 0 ) → 𝑏 = 𝐵)
11		fveq2 6903	. . . . . . . . . 10 ⊢ (𝑟 = 𝑅 → (.r‘𝑟) = (.r‘𝑅))
12		isdomn.t	. . . . . . . . . 10 ⊢ · = (.r‘𝑅)
13	11, 12	eqtr4di 2784	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (.r‘𝑟) = · )
14	13	oveqdr 7454	. . . . . . . 8 ⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → (𝑥(.r‘𝑟)𝑦) = (𝑥 · 𝑦))
15		id 22	. . . . . . . 8 ⊢ (𝑧 = 0 → 𝑧 = 0 )
16	14, 15	eqeqan12d 2740	. . . . . . 7 ⊢ (((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑧 = 0 ) → ((𝑥(.r‘𝑟)𝑦) = 𝑧 ↔ (𝑥 · 𝑦) = 0 ))
17		eqeq2 2738	. . . . . . . . 9 ⊢ (𝑧 = 0 → (𝑥 = 𝑧 ↔ 𝑥 = 0 ))
18		eqeq2 2738	. . . . . . . . 9 ⊢ (𝑧 = 0 → (𝑦 = 𝑧 ↔ 𝑦 = 0 ))
19	17, 18	orbi12d 916	. . . . . . . 8 ⊢ (𝑧 = 0 → ((𝑥 = 𝑧 ∨ 𝑦 = 𝑧) ↔ (𝑥 = 0 ∨ 𝑦 = 0 )))
20	19	adantl 480	. . . . . . 7 ⊢ (((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑧 = 0 ) → ((𝑥 = 𝑧 ∨ 𝑦 = 𝑧) ↔ (𝑥 = 0 ∨ 𝑦 = 0 )))
21	16, 20	imbi12d 343	. . . . . 6 ⊢ (((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑧 = 0 ) → (((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧)) ↔ ((𝑥 · 𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))))
22	10, 21	raleqbidv 3330	. . . . 5 ⊢ (((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑧 = 0 ) → (∀𝑦 ∈ 𝑏 ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧)) ↔ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))))
23	10, 22	raleqbidv 3330	. . . 4 ⊢ (((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑧 = 0 ) → (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))))
24	5, 9, 23	sbcied2 3824	. . 3 ⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → ([(0g‘𝑟) / 𝑧]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))))
25	1, 4, 24	sbcied2 3824	. 2 ⊢ (𝑟 = 𝑅 → ([(Base‘𝑟) / 𝑏][(0g‘𝑟) / 𝑧]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))))
26		df-domn 20675	. 2 ⊢ Domn = {𝑟 ∈ NzRing ∣ [(Base‘𝑟) / 𝑏][(0g‘𝑟) / 𝑧]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧))}
27	25, 26	elrab2 3684	1 ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 845   = wceq 1534   ∈ wcel 2099  ∀wral 3051  Vcvv 3462  [wsbc 3776  ‘cfv 6556  (class class class)co 7426  Basecbs 17215  ._rcmulr 17269  0_gc0g 17456  NzRingcnzr 20496  Domncdomn 20672

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-nul 5313

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ne 2931  df-ral 3052  df-rab 3420  df-v 3464  df-sbc 3777  df-dif 3950  df-un 3952  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4916  df-br 5156  df-iota 6508  df-fv 6564  df-ov 7429  df-domn 20675

This theorem is referenced by:  domnnzr  20686  domneq0  20688  isdomn2  20691  isdomn2OLD  20692  isdomn3  20695  isdomn4  20696  opprdomnb  20697  abvn0b  20817  znfld  21560  ply1domn  26154  fta1b  26202  subrdom  33139  prmidl0  33327  qsidomlem2  33330