Theorem isdrngo3 35762

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 35761	. 2 ⊢ (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)))
7		eldifi 4017	. . . . . 6 ⊢ (𝑥 ∈ (𝑋 ∖ {𝑍}) → 𝑥 ∈ 𝑋)
8		difss 4022	. . . . . . . 8 ⊢ (𝑋 ∖ {𝑍}) ⊆ 𝑋
9		ssrexv 3944	. . . . . . . 8 ⊢ ((𝑋 ∖ {𝑍}) ⊆ 𝑋 → (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈 → ∃𝑦 ∈ 𝑋 (𝑦𝐻𝑥) = 𝑈))
10	8, 9	ax-mp 5	. . . . . . 7 ⊢ (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈 → ∃𝑦 ∈ 𝑋 (𝑦𝐻𝑥) = 𝑈)
11		neeq1 2996	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦𝐻𝑥) = 𝑈 → ((𝑦𝐻𝑥) ≠ 𝑍 ↔ 𝑈 ≠ 𝑍))
12	11	biimparc 483	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ≠ 𝑍 ∧ (𝑦𝐻𝑥) = 𝑈) → (𝑦𝐻𝑥) ≠ 𝑍)
13	3, 4, 1, 2	rngolz 35725	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑋) → (𝑍𝐻𝑥) = 𝑍)
14		oveq1 7179	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑍 → (𝑦𝐻𝑥) = (𝑍𝐻𝑥))
15	14	eqeq1d 2740	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑍 → ((𝑦𝐻𝑥) = 𝑍 ↔ (𝑍𝐻𝑥) = 𝑍))
16	13, 15	syl5ibrcom 250	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑋) → (𝑦 = 𝑍 → (𝑦𝐻𝑥) = 𝑍))
17	16	necon3d 2955	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑋) → ((𝑦𝐻𝑥) ≠ 𝑍 → 𝑦 ≠ 𝑍))
18	17	imp 410	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑋) ∧ (𝑦𝐻𝑥) ≠ 𝑍) → 𝑦 ≠ 𝑍)
19	12, 18	sylan2 596	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑋) ∧ (𝑈 ≠ 𝑍 ∧ (𝑦𝐻𝑥) = 𝑈)) → 𝑦 ≠ 𝑍)
20	19	an4s 660	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) ∧ (𝑥 ∈ 𝑋 ∧ (𝑦𝐻𝑥) = 𝑈)) → 𝑦 ≠ 𝑍)
21	20	anassrs 471	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) ∧ 𝑥 ∈ 𝑋) ∧ (𝑦𝐻𝑥) = 𝑈) → 𝑦 ≠ 𝑍)
22		pm3.2 473	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝑋 → (𝑦 ≠ 𝑍 → (𝑦 ∈ 𝑋 ∧ 𝑦 ≠ 𝑍)))
23	21, 22	syl5com 31	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) ∧ 𝑥 ∈ 𝑋) ∧ (𝑦𝐻𝑥) = 𝑈) → (𝑦 ∈ 𝑋 → (𝑦 ∈ 𝑋 ∧ 𝑦 ≠ 𝑍)))
24		eldifsn 4675	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (𝑋 ∖ {𝑍}) ↔ (𝑦 ∈ 𝑋 ∧ 𝑦 ≠ 𝑍))
25	23, 24	syl6ibr 255	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) ∧ 𝑥 ∈ 𝑋) ∧ (𝑦𝐻𝑥) = 𝑈) → (𝑦 ∈ 𝑋 → 𝑦 ∈ (𝑋 ∖ {𝑍})))
26	25	imdistanda 575	. . . . . . . . 9 ⊢ (((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) ∧ 𝑥 ∈ 𝑋) → (((𝑦𝐻𝑥) = 𝑈 ∧ 𝑦 ∈ 𝑋) → ((𝑦𝐻𝑥) = 𝑈 ∧ 𝑦 ∈ (𝑋 ∖ {𝑍}))))
27		ancom 464	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝑋 ∧ (𝑦𝐻𝑥) = 𝑈) ↔ ((𝑦𝐻𝑥) = 𝑈 ∧ 𝑦 ∈ 𝑋))
28		ancom 464	. . . . . . . . 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 596	. . . . 5 ⊢ (((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈 ↔ ∃𝑦 ∈ 𝑋 (𝑦𝐻𝑥) = 𝑈))
33	32	ralbidva 3108	. . . 4 ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → (∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈 ↔ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ 𝑋 (𝑦𝐻𝑥) = 𝑈))
34	33	pm5.32da 582	. . 3 ⊢ (𝑅 ∈ RingOps → ((𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈) ↔ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ 𝑋 (𝑦𝐻𝑥) = 𝑈)))
35	34	pm5.32i 578	. 2 ⊢ ((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ↔ (𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ 𝑋 (𝑦𝐻𝑥) = 𝑈)))
36	6, 35	bitri 278	1 ⊢ (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ 𝑋 (𝑦𝐻𝑥) = 𝑈)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1542   ∈ wcel 2114   ≠ wne 2934  ∀wral 3053  ∃wrex 3054   ∖ cdif 3840   ⊆ wss 3843  {csn 4516  ran crn 5526  ‘cfv 6339  (class class class)co 7172  1^st c1st 7714  2^nd c2nd 7715  GIdcgi 28427  RingOpscrngo 35697  DivRingOpscdrng 35751

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 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7481

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3400  df-sbc 3681  df-csb 3791  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-pss 3862  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-tp 4521  df-op 4523  df-uni 4797  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5483  df-we 5485  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-ord 6175  df-on 6176  df-lim 6177  df-suc 6178  df-iota 6297  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-riota 7129  df-ov 7175  df-om 7602  df-1st 7716  df-2nd 7717  df-1o 8133  df-er 8322  df-en 8558  df-dom 8559  df-sdom 8560  df-fin 8561  df-grpo 28430  df-gid 28431  df-ginv 28432  df-ablo 28482  df-ass 35646  df-exid 35648  df-mgmOLD 35652  df-sgrOLD 35664  df-mndo 35670  df-rngo 35698  df-drngo 35752

This theorem is referenced by:  isfldidl  35871