Theorem isdrngo3 38532

Description: A division ring is a ring in which 1 ≠ 0 and every nonzero element is invertible. (Contributed by Jeff Madsen, 10-Jun-2010.)

Hypotheses

Ref	Expression
isdivrng1.1	⊢ 𝐺 = (1st ‘𝑅)
isdivrng1.2	⊢ 𝐻 = (2nd ‘𝑅)
isdivrng1.3	⊢ 𝑍 = (GId‘𝐺)
isdivrng1.4	⊢ 𝑋 = ran 𝐺
isdivrng2.5	⊢ 𝑈 = (GId‘𝐻)

Assertion

Ref	Expression
isdrngo3	⊢ (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ 𝑋 (𝑦𝐻𝑥) = 𝑈)))

Distinct variable groups:   𝑥,𝐻,𝑦   𝑥,𝑋,𝑦   𝑥,𝑍,𝑦   𝑥,𝑅,𝑦   𝑥,𝑈,𝑦

Allowed substitution hints:   𝐺(𝑥,𝑦)

Proof of Theorem isdrngo3

Step	Hyp	Ref	Expression
1		isdivrng1.1	. . 3 ⊢ 𝐺 = (1st ‘𝑅)
2		isdivrng1.2	. . 3 ⊢ 𝐻 = (2nd ‘𝑅)
3		isdivrng1.3	. . 3 ⊢ 𝑍 = (GId‘𝐺)
4		isdivrng1.4	. . 3 ⊢ 𝑋 = ran 𝐺
5		isdivrng2.5	. . 3 ⊢ 𝑈 = (GId‘𝐻)
6	1, 2, 3, 4, 5	isdrngo2 38531	. 2 ⊢ (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)))
7		eldifi 4093	. . . . . 6 ⊢ (𝑥 ∈ (𝑋 ∖ {𝑍}) → 𝑥 ∈ 𝑋)
8		difss 4098	. . . . . . . 8 ⊢ (𝑋 ∖ {𝑍}) ⊆ 𝑋
9		ssrexv 4015	. . . . . . . 8 ⊢ ((𝑋 ∖ {𝑍}) ⊆ 𝑋 → (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈 → ∃𝑦 ∈ 𝑋 (𝑦𝐻𝑥) = 𝑈))
10	8, 9	ax-mp 5	. . . . . . 7 ⊢ (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈 → ∃𝑦 ∈ 𝑋 (𝑦𝐻𝑥) = 𝑈)
11		neeq1 3026	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦𝐻𝑥) = 𝑈 → ((𝑦𝐻𝑥) ≠ 𝑍 ↔ 𝑈 ≠ 𝑍))
12	11	biimparc 484	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ≠ 𝑍 ∧ (𝑦𝐻𝑥) = 𝑈) → (𝑦𝐻𝑥) ≠ 𝑍)
13	3, 4, 1, 2	rngolz 38495	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑋) → (𝑍𝐻𝑥) = 𝑍)
14		oveq1 7418	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑍 → (𝑦𝐻𝑥) = (𝑍𝐻𝑥))
15	14	eqeq1d 2771	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑍 → ((𝑦𝐻𝑥) = 𝑍 ↔ (𝑍𝐻𝑥) = 𝑍))
16	13, 15	syl5ibrcom 250	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑋) → (𝑦 = 𝑍 → (𝑦𝐻𝑥) = 𝑍))
17	16	necon3d 2985	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑋) → ((𝑦𝐻𝑥) ≠ 𝑍 → 𝑦 ≠ 𝑍))
18	17	imp 411	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑋) ∧ (𝑦𝐻𝑥) ≠ 𝑍) → 𝑦 ≠ 𝑍)
19	12, 18	sylan2 604	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑋) ∧ (𝑈 ≠ 𝑍 ∧ (𝑦𝐻𝑥) = 𝑈)) → 𝑦 ≠ 𝑍)
20	19	an4s 672	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦𝐻𝑥) = 𝑈)) → 𝑦 ≠ 𝑍)
21	20	anassrs 472	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) ∧ 𝑥 ∈ 𝑋) ∧ (𝑦𝐻𝑥) = 𝑈) → 𝑦 ≠ 𝑍)
22		pm3.2 474	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝑋 → (𝑦 ≠ 𝑍 → (𝑦 ∈ 𝑋 ∧ 𝑦 ≠ 𝑍)))
23	21, 22	syl5com 32	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) ∧ 𝑥 ∈ 𝑋) ∧ (𝑦𝐻𝑥) = 𝑈) → (𝑦 ∈ 𝑋 → (𝑦 ∈ 𝑋 ∧ 𝑦 ≠ 𝑍)))
24		eldifsn 4758	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (𝑋 ∖ {𝑍}) ↔ (𝑦 ∈ 𝑋 ∧ 𝑦 ≠ 𝑍))
25	23, 24	imbitrrdi 255	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) ∧ 𝑥 ∈ 𝑋) ∧ (𝑦𝐻𝑥) = 𝑈) → (𝑦 ∈ 𝑋 → 𝑦 ∈ (𝑋 ∖ {𝑍})))
26	25	imdistanda 581	. . . . . . . . 9 ⊢ (((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) ∧ 𝑥 ∈ 𝑋) → (((𝑦𝐻𝑥) = 𝑈 ∧ 𝑦 ∈ 𝑋) → ((𝑦𝐻𝑥) = 𝑈 ∧ 𝑦 ∈ (𝑋 ∖ {𝑍}))))
27		ancom 465	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝑋 ∧ (𝑦𝐻𝑥) = 𝑈) ↔ ((𝑦𝐻𝑥) = 𝑈 ∧ 𝑦 ∈ 𝑋))
28		ancom 465	. . . . . . . . 9 ⊢ ((𝑦 ∈ (𝑋 ∖ {𝑍}) ∧ (𝑦𝐻𝑥) = 𝑈) ↔ ((𝑦𝐻𝑥) = 𝑈 ∧ 𝑦 ∈ (𝑋 ∖ {𝑍})))
29	26, 27, 28	3imtr4g 299	. . . . . . . 8 ⊢ (((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) ∧ 𝑥 ∈ 𝑋) → ((𝑦 ∈ 𝑋 ∧ (𝑦𝐻𝑥) = 𝑈) → (𝑦 ∈ (𝑋 ∖ {𝑍}) ∧ (𝑦𝐻𝑥) = 𝑈)))
30	29	reximdv2 3181	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) ∧ 𝑥 ∈ 𝑋) → (∃𝑦 ∈ 𝑋 (𝑦𝐻𝑥) = 𝑈 → ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈))
31	10, 30	impbid2 229	. . . . . 6 ⊢ (((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) ∧ 𝑥 ∈ 𝑋) → (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈 ↔ ∃𝑦 ∈ 𝑋 (𝑦𝐻𝑥) = 𝑈))
32	7, 31	sylan2 604	. . . . 5 ⊢ (((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈 ↔ ∃𝑦 ∈ 𝑋 (𝑦𝐻𝑥) = 𝑈))
33	32	ralbidva 3192	. . . 4 ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → (∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈 ↔ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ 𝑋 (𝑦𝐻𝑥) = 𝑈))
34	33	pm5.32da 589	. . 3 ⊢ (𝑅 ∈ RingOps → ((𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈) ↔ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ 𝑋 (𝑦𝐻𝑥) = 𝑈)))
35	34	pm5.32i 584	. 2 ⊢ ((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ↔ (𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ 𝑋 (𝑦𝐻𝑥) = 𝑈)))
36	6, 35	bitri 278	1 ⊢ (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ 𝑋 (𝑦𝐻𝑥) = 𝑈)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   ∈ wcel 2149   ≠ wne 2964  ∀wral 3085  ∃wrex 3095   ∖ cdif 3910   ⊆ wss 3913  {csn 4594  ran crn 5663  ‘cfv 6537  (class class class)co 7411  1^st c1st 7984  2^nd c2nd 7985  GIdcgi 30783  RingOpscrngo 38467  DivRingOpscdrng 38521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5242  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7368  df-ov 7414  df-1st 7986  df-2nd 7987  df-1o 8453  df-en 8944  df-grpo 30786  df-gid 30787  df-ginv 30788  df-ablo 30838  df-ass 38416  df-exid 38418  df-mgmOLD 38422  df-sgrOLD 38434  df-mndo 38440  df-rngo 38468  df-drngo 38522

This theorem is referenced by:  isfldidl  38641