Theorem isdomn 20069

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 6687	. . 3 ⊢ (𝑟 = 𝑅 → (Base‘𝑟) ∈ V)
2		fveq2 6672	. . . 4 ⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅))
3		isdomn.b	. . . 4 ⊢ 𝐵 = (Base‘𝑅)
4	2, 3	syl6eqr 2876	. . 3 ⊢ (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵)
5		fvexd 6687	. . . 4 ⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → (0g‘𝑟) ∈ V)
6		fveq2 6672	. . . . . 6 ⊢ (𝑟 = 𝑅 → (0g‘𝑟) = (0g‘𝑅))
7	6	adantr 483	. . . . 5 ⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → (0g‘𝑟) = (0g‘𝑅))
8		isdomn.z	. . . . 5 ⊢ 0 = (0g‘𝑅)
9	7, 8	syl6eqr 2876	. . . 4 ⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → (0g‘𝑟) = 0 )
10		simplr 767	. . . . 5 ⊢ (((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑧 = 0 ) → 𝑏 = 𝐵)
11		fveq2 6672	. . . . . . . . . 10 ⊢ (𝑟 = 𝑅 → (.r‘𝑟) = (.r‘𝑅))
12		isdomn.t	. . . . . . . . . 10 ⊢ · = (.r‘𝑅)
13	11, 12	syl6eqr 2876	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (.r‘𝑟) = · )
14	13	oveqdr 7186	. . . . . . . 8 ⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → (𝑥(.r‘𝑟)𝑦) = (𝑥 · 𝑦))
15		id 22	. . . . . . . 8 ⊢ (𝑧 = 0 → 𝑧 = 0 )
16	14, 15	eqeqan12d 2840	. . . . . . 7 ⊢ (((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑧 = 0 ) → ((𝑥(.r‘𝑟)𝑦) = 𝑧 ↔ (𝑥 · 𝑦) = 0 ))
17		eqeq2 2835	. . . . . . . . 9 ⊢ (𝑧 = 0 → (𝑥 = 𝑧 ↔ 𝑥 = 0 ))
18		eqeq2 2835	. . . . . . . . 9 ⊢ (𝑧 = 0 → (𝑦 = 𝑧 ↔ 𝑦 = 0 ))
19	17, 18	orbi12d 915	. . . . . . . 8 ⊢ (𝑧 = 0 → ((𝑥 = 𝑧 ∨ 𝑦 = 𝑧) ↔ (𝑥 = 0 ∨ 𝑦 = 0 )))
20	19	adantl 484	. . . . . . 7 ⊢ (((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑧 = 0 ) → ((𝑥 = 𝑧 ∨ 𝑦 = 𝑧) ↔ (𝑥 = 0 ∨ 𝑦 = 0 )))
21	16, 20	imbi12d 347	. . . . . 6 ⊢ (((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑧 = 0 ) → (((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧)) ↔ ((𝑥 · 𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))))
22	10, 21	raleqbidv 3403	. . . . 5 ⊢ (((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑧 = 0 ) → (∀𝑦 ∈ 𝑏 ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧)) ↔ ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))))
23	10, 22	raleqbidv 3403	. . . 4 ⊢ (((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) ∧ 𝑧 = 0 ) → (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))))
24	5, 9, 23	sbcied2 3817	. . 3 ⊢ ((𝑟 = 𝑅 ∧ 𝑏 = 𝐵) → ([(0g‘𝑟) / 𝑧]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))))
25	1, 4, 24	sbcied2 3817	. 2 ⊢ (𝑟 = 𝑅 → ([(Base‘𝑟) / 𝑏][(0g‘𝑟) / 𝑧]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))))
26		df-domn 20059	. 2 ⊢ Domn = {𝑟 ∈ NzRing ∣ [(Base‘𝑟) / 𝑏][(0g‘𝑟) / 𝑧]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥(.r‘𝑟)𝑦) = 𝑧 → (𝑥 = 𝑧 ∨ 𝑦 = 𝑧))}
27	25, 26	elrab2 3685	1 ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843   = wceq 1537   ∈ wcel 2114  ∀wral 3140  Vcvv 3496  [wsbc 3774  ‘cfv 6357  (class class class)co 7158  Basecbs 16485  ._rcmulr 16568  0_gc0g 16715  NzRingcnzr 20032  Domncdomn 20055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-nul 5212

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-iota 6316  df-fv 6365  df-ov 7161  df-domn 20059

This theorem is referenced by:  domnnzr  20070  domneq0  20072  isdomn2  20074  opprdomn  20076  abvn0b  20077  znfld  20709  ply1domn  24719  fta1b  24765  qsidomlem2  30968  isdomn3  39811