Theorem isdrngo2 37944

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

Hypotheses

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

Assertion

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

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

Allowed substitution hints:   𝐺(𝑥,𝑦)

Proof of Theorem isdrngo2

Dummy variables 𝑢 𝑣 𝑤 𝑧 are mutually distinct and distinct from all other variables.

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	1, 2, 3, 4	isdrngo1 37942	. 2 ⊢ (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp))
6		isdivrng2.5	. . . . . . 7 ⊢ 𝑈 = (GId‘𝐻)
7	1, 2, 4, 3, 6	dvrunz 37940	. . . . . 6 ⊢ (𝑅 ∈ DivRingOps → 𝑈 ≠ 𝑍)
8	5, 7	sylbir 235	. . . . 5 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → 𝑈 ≠ 𝑍)
9		grporndm 30538	. . . . . . . . . . . 12 ⊢ ((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp → ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = dom dom (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))
10	9	adantl 481	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = dom dom (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))
11		difss 4145	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∖ {𝑍}) ⊆ 𝑋
12		xpss12 5703	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑋 ∖ {𝑍}) ⊆ 𝑋 ∧ (𝑋 ∖ {𝑍}) ⊆ 𝑋) → ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})) ⊆ (𝑋 × 𝑋))
13	11, 11, 12	mp2an 692	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})) ⊆ (𝑋 × 𝑋)
14	1, 2, 4	rngosm 37886	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ RingOps → 𝐻:(𝑋 × 𝑋)⟶𝑋)
15	14	fdmd 6746	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ RingOps → dom 𝐻 = (𝑋 × 𝑋))
16	13, 15	sseqtrrid 4048	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ RingOps → ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})) ⊆ dom 𝐻)
17	16	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})) ⊆ dom 𝐻)
18		ssdmres 6032	. . . . . . . . . . . . . 14 ⊢ (((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})) ⊆ dom 𝐻 ↔ dom (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))
19	17, 18	sylib 218	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → dom (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))
20	19	dmeqd 5918	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → dom dom (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = dom ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))
21		dmxpid 5943	. . . . . . . . . . . 12 ⊢ dom ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})) = (𝑋 ∖ {𝑍})
22	20, 21	eqtrdi 2790	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → dom dom (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = (𝑋 ∖ {𝑍}))
23	10, 22	eqtrd 2774	. . . . . . . . . 10 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = (𝑋 ∖ {𝑍}))
24	23	eleq2d 2824	. . . . . . . . 9 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → (𝑥 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ↔ 𝑥 ∈ (𝑋 ∖ {𝑍})))
25	24	biimpar 477	. . . . . . . 8 ⊢ (((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → 𝑥 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))
26		eqid 2734	. . . . . . . . . . 11 ⊢ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))
27		eqid 2734	. . . . . . . . . . 11 ⊢ (inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) = (inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))
28	26, 27	grpoinvcl 30552	. . . . . . . . . 10 ⊢ (((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp ∧ 𝑥 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) → ((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥) ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))
29	28	adantll 714	. . . . . . . . 9 ⊢ (((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ∧ 𝑥 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) → ((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥) ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))
30		eqid 2734	. . . . . . . . . . . 12 ⊢ (GId‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) = (GId‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))
31	26, 30, 27	grpolinv 30554	. . . . . . . . . . 11 ⊢ (((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp ∧ 𝑥 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) → (((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = (GId‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))))
32	31	adantll 714	. . . . . . . . . 10 ⊢ (((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ∧ 𝑥 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) → (((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = (GId‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))))
33	2	rngomndo 37921	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ RingOps → 𝐻 ∈ MndOp)
34		mndomgmid 37857	. . . . . . . . . . . . . 14 ⊢ (𝐻 ∈ MndOp → 𝐻 ∈ (Magma ∩ ExId ))
35	33, 34	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ RingOps → 𝐻 ∈ (Magma ∩ ExId ))
36	35	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → 𝐻 ∈ (Magma ∩ ExId ))
37	11, 4	sseqtri 4031	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∖ {𝑍}) ⊆ ran 𝐺
38	2, 1	rngorn1eq 37920	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ RingOps → ran 𝐺 = ran 𝐻)
39	37, 38	sseqtrid 4047	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ RingOps → (𝑋 ∖ {𝑍}) ⊆ ran 𝐻)
40	39	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → (𝑋 ∖ {𝑍}) ⊆ ran 𝐻)
41	1	rneqi 5950	. . . . . . . . . . . . . . . 16 ⊢ ran 𝐺 = ran (1st ‘𝑅)
42	4, 41	eqtri 2762	. . . . . . . . . . . . . . 15 ⊢ 𝑋 = ran (1st ‘𝑅)
43	42, 2, 6	rngo1cl 37925	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ RingOps → 𝑈 ∈ 𝑋)
44	43	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → 𝑈 ∈ 𝑋)
45		eldifsn 4790	. . . . . . . . . . . . 13 ⊢ (𝑈 ∈ (𝑋 ∖ {𝑍}) ↔ (𝑈 ∈ 𝑋 ∧ 𝑈 ≠ 𝑍))
46	44, 8, 45	sylanbrc 583	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → 𝑈 ∈ (𝑋 ∖ {𝑍}))
47		grpomndo 37861	. . . . . . . . . . . . . 14 ⊢ ((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp → (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ MndOp)
48		mndoismgmOLD 37856	. . . . . . . . . . . . . 14 ⊢ ((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ MndOp → (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ Magma)
49	47, 48	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp → (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ Magma)
50	49	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ Magma)
51		eqid 2734	. . . . . . . . . . . . 13 ⊢ ran 𝐻 = ran 𝐻
52		eqid 2734	. . . . . . . . . . . . 13 ⊢ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))
53	51, 6, 52	exidresid 37865	. . . . . . . . . . . 12 ⊢ (((𝐻 ∈ (Magma ∩ ExId ) ∧ (𝑋 ∖ {𝑍}) ⊆ ran 𝐻 ∧ 𝑈 ∈ (𝑋 ∖ {𝑍})) ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ Magma) → (GId‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) = 𝑈)
54	36, 40, 46, 50, 53	syl31anc 1372	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → (GId‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) = 𝑈)
55	54	adantr 480	. . . . . . . . . 10 ⊢ (((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ∧ 𝑥 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) → (GId‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) = 𝑈)
56	32, 55	eqtrd 2774	. . . . . . . . 9 ⊢ (((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ∧ 𝑥 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) → (((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = 𝑈)
57		oveq1 7437	. . . . . . . . . . 11 ⊢ (𝑦 = ((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥) → (𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = (((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥))
58	57	eqeq1d 2736	. . . . . . . . . 10 ⊢ (𝑦 = ((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥) → ((𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = 𝑈 ↔ (((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = 𝑈))
59	58	rspcev 3621	. . . . . . . . 9 ⊢ ((((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥) ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∧ (((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = 𝑈) → ∃𝑦 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))(𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = 𝑈)
60	29, 56, 59	syl2anc 584	. . . . . . . 8 ⊢ (((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ∧ 𝑥 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) → ∃𝑦 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))(𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = 𝑈)
61	25, 60	syldan 591	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → ∃𝑦 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))(𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = 𝑈)
62	23	adantr 480	. . . . . . . . 9 ⊢ (((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = (𝑋 ∖ {𝑍}))
63	62	rexeqdv 3324	. . . . . . . 8 ⊢ (((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (∃𝑦 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))(𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = 𝑈 ↔ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = 𝑈))
64		ovres 7598	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = (𝑦𝐻𝑥))
65	64	ancoms 458	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑦 ∈ (𝑋 ∖ {𝑍})) → (𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = (𝑦𝐻𝑥))
66	65	eqeq1d 2736	. . . . . . . . . 10 ⊢ ((𝑥 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑦 ∈ (𝑋 ∖ {𝑍})) → ((𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = 𝑈 ↔ (𝑦𝐻𝑥) = 𝑈))
67	66	rexbidva 3174	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝑋 ∖ {𝑍}) → (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = 𝑈 ↔ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈))
68	67	adantl 481	. . . . . . . 8 ⊢ (((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = 𝑈 ↔ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈))
69	63, 68	bitrd 279	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (∃𝑦 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))(𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = 𝑈 ↔ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈))
70	61, 69	mpbid 232	. . . . . 6 ⊢ (((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)
71	70	ralrimiva 3143	. . . . 5 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)
72	8, 71	jca 511	. . . 4 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈))
73	1	fvexi 6920	. . . . . . . 8 ⊢ 𝐺 ∈ V
74	73	rnex 7932	. . . . . . 7 ⊢ ran 𝐺 ∈ V
75	4, 74	eqeltri 2834	. . . . . 6 ⊢ 𝑋 ∈ V
76		difexg 5334	. . . . . 6 ⊢ (𝑋 ∈ V → (𝑋 ∖ {𝑍}) ∈ V)
77	75, 76	mp1i 13	. . . . 5 ⊢ ((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) → (𝑋 ∖ {𝑍}) ∈ V)
78	14	ffnd 6737	. . . . . . . 8 ⊢ (𝑅 ∈ RingOps → 𝐻 Fn (𝑋 × 𝑋))
79	78	adantr 480	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) → 𝐻 Fn (𝑋 × 𝑋))
80		fnssres 6691	. . . . . . 7 ⊢ ((𝐻 Fn (𝑋 × 𝑋) ∧ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})) ⊆ (𝑋 × 𝑋)) → (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) Fn ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))
81	79, 13, 80	sylancl 586	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) → (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) Fn ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))
82		ovres 7598	. . . . . . . . 9 ⊢ ((𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍})) → (𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣) = (𝑢𝐻𝑣))
83	82	adantl 481	. . . . . . . 8 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}))) → (𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣) = (𝑢𝐻𝑣))
84		eldifi 4140	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ (𝑋 ∖ {𝑍}) → 𝑢 ∈ 𝑋)
85		eldifi 4140	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ (𝑋 ∖ {𝑍}) → 𝑣 ∈ 𝑋)
86	84, 85	anim12i 613	. . . . . . . . . . 11 ⊢ ((𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍})) → (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋))
87	1, 2, 4	rngocl 37887	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ RingOps ∧ 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋) → (𝑢𝐻𝑣) ∈ 𝑋)
88	87	3expb 1119	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ RingOps ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑢𝐻𝑣) ∈ 𝑋)
89	86, 88	sylan2 593	. . . . . . . . . 10 ⊢ ((𝑅 ∈ RingOps ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}))) → (𝑢𝐻𝑣) ∈ 𝑋)
90	89	adantlr 715	. . . . . . . . 9 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}))) → (𝑢𝐻𝑣) ∈ 𝑋)
91		oveq2 7438	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑢 → (𝑦𝐻𝑥) = (𝑦𝐻𝑢))
92	91	eqeq1d 2736	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑢 → ((𝑦𝐻𝑥) = 𝑈 ↔ (𝑦𝐻𝑢) = 𝑈))
93	92	rexbidv 3176	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑢 → (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈 ↔ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈))
94	93	rspcv 3617	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ (𝑋 ∖ {𝑍}) → (∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈 → ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈))
95	94	imdistanri 569	. . . . . . . . . . . 12 ⊢ ((∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈 ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈 ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})))
96		eldifsn 4790	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ (𝑋 ∖ {𝑍}) ↔ (𝑣 ∈ 𝑋 ∧ 𝑣 ≠ 𝑍))
97		ssrexv 4064	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑋 ∖ {𝑍}) ⊆ 𝑋 → (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈 → ∃𝑦 ∈ 𝑋 (𝑦𝐻𝑢) = 𝑈))
98	11, 97	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈 → ∃𝑦 ∈ 𝑋 (𝑦𝐻𝑢) = 𝑈)
99	1, 2, 3, 4, 6	zerdivemp1x 37933	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ RingOps ∧ 𝑢 ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐻𝑢) = 𝑈) → (𝑣 ∈ 𝑋 → ((𝑢𝐻𝑣) = 𝑍 → 𝑣 = 𝑍)))
100	98, 99	syl3an3 1164	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ RingOps ∧ 𝑢 ∈ 𝑋 ∧ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈) → (𝑣 ∈ 𝑋 → ((𝑢𝐻𝑣) = 𝑍 → 𝑣 = 𝑍)))
101	84, 100	syl3an2 1163	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ RingOps ∧ 𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈) → (𝑣 ∈ 𝑋 → ((𝑢𝐻𝑣) = 𝑍 → 𝑣 = 𝑍)))
102	101	3expb 1119	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ RingOps ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈)) → (𝑣 ∈ 𝑋 → ((𝑢𝐻𝑣) = 𝑍 → 𝑣 = 𝑍)))
103	102	imp 406	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ RingOps ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈)) ∧ 𝑣 ∈ 𝑋) → ((𝑢𝐻𝑣) = 𝑍 → 𝑣 = 𝑍))
104	103	necon3d 2958	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ RingOps ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈)) ∧ 𝑣 ∈ 𝑋) → (𝑣 ≠ 𝑍 → (𝑢𝐻𝑣) ≠ 𝑍))
105	104	impr 454	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ RingOps ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈)) ∧ (𝑣 ∈ 𝑋 ∧ 𝑣 ≠ 𝑍)) → (𝑢𝐻𝑣) ≠ 𝑍)
106	96, 105	sylan2b 594	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ RingOps ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈)) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍})) → (𝑢𝐻𝑣) ≠ 𝑍)
107	106	an32s 652	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ RingOps ∧ 𝑣 ∈ (𝑋 ∖ {𝑍})) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈)) → (𝑢𝐻𝑣) ≠ 𝑍)
108	107	ancom2s 650	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ RingOps ∧ 𝑣 ∈ (𝑋 ∖ {𝑍})) ∧ (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈 ∧ 𝑢 ∈ (𝑋 ∖ {𝑍}))) → (𝑢𝐻𝑣) ≠ 𝑍)
109	95, 108	sylan2 593	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ RingOps ∧ 𝑣 ∈ (𝑋 ∖ {𝑍})) ∧ (∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈 ∧ 𝑢 ∈ (𝑋 ∖ {𝑍}))) → (𝑢𝐻𝑣) ≠ 𝑍)
110	109	an42s 661	. . . . . . . . . 10 ⊢ (((𝑅 ∈ RingOps ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}))) → (𝑢𝐻𝑣) ≠ 𝑍)
111	110	adantlrl 720	. . . . . . . . 9 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}))) → (𝑢𝐻𝑣) ≠ 𝑍)
112		eldifsn 4790	. . . . . . . . 9 ⊢ ((𝑢𝐻𝑣) ∈ (𝑋 ∖ {𝑍}) ↔ ((𝑢𝐻𝑣) ∈ 𝑋 ∧ (𝑢𝐻𝑣) ≠ 𝑍))
113	90, 111, 112	sylanbrc 583	. . . . . . . 8 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}))) → (𝑢𝐻𝑣) ∈ (𝑋 ∖ {𝑍}))
114	83, 113	eqeltrd 2838	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}))) → (𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣) ∈ (𝑋 ∖ {𝑍}))
115	114	ralrimivva 3199	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) → ∀𝑢 ∈ (𝑋 ∖ {𝑍})∀𝑣 ∈ (𝑋 ∖ {𝑍})(𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣) ∈ (𝑋 ∖ {𝑍}))
116		ffnov 7558	. . . . . 6 ⊢ ((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))):((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))⟶(𝑋 ∖ {𝑍}) ↔ ((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) Fn ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})) ∧ ∀𝑢 ∈ (𝑋 ∖ {𝑍})∀𝑣 ∈ (𝑋 ∖ {𝑍})(𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣) ∈ (𝑋 ∖ {𝑍})))
117	81, 115, 116	sylanbrc 583	. . . . 5 ⊢ ((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) → (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))):((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))⟶(𝑋 ∖ {𝑍}))
118	113	3adantr3 1170	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → (𝑢𝐻𝑣) ∈ (𝑋 ∖ {𝑍}))
119		simpr3 1195	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → 𝑤 ∈ (𝑋 ∖ {𝑍}))
120	118, 119	ovresd 7599	. . . . . 6 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → ((𝑢𝐻𝑣)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) = ((𝑢𝐻𝑣)𝐻𝑤))
121	82	3adant3 1131	. . . . . . . 8 ⊢ ((𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍})) → (𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣) = (𝑢𝐻𝑣))
122	121	adantl 481	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → (𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣) = (𝑢𝐻𝑣))
123	122	oveq1d 7445	. . . . . 6 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → ((𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) = ((𝑢𝐻𝑣)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤))
124		ovres 7598	. . . . . . . . . 10 ⊢ ((𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍})) → (𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) = (𝑣𝐻𝑤))
125	124	3adant1 1129	. . . . . . . . 9 ⊢ ((𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍})) → (𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) = (𝑣𝐻𝑤))
126	125	adantl 481	. . . . . . . 8 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → (𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) = (𝑣𝐻𝑤))
127	126	oveq2d 7446	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → (𝑢𝐻(𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤)) = (𝑢𝐻(𝑣𝐻𝑤)))
128		simpr1 1193	. . . . . . . 8 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → 𝑢 ∈ (𝑋 ∖ {𝑍}))
129		fovcdm 7602	. . . . . . . . . 10 ⊢ (((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))):((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))⟶(𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍})) → (𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) ∈ (𝑋 ∖ {𝑍}))
130	129	3adant3r1 1181	. . . . . . . . 9 ⊢ (((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))):((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))⟶(𝑋 ∖ {𝑍}) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → (𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) ∈ (𝑋 ∖ {𝑍}))
131	117, 130	sylan 580	. . . . . . . 8 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → (𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) ∈ (𝑋 ∖ {𝑍}))
132	128, 131	ovresd 7599	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → (𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))(𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤)) = (𝑢𝐻(𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤)))
133		eldifi 4140	. . . . . . . . . 10 ⊢ (𝑤 ∈ (𝑋 ∖ {𝑍}) → 𝑤 ∈ 𝑋)
134	84, 85, 133	3anim123i 1150	. . . . . . . . 9 ⊢ ((𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍})) → (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋))
135	1, 2, 4	rngoass 37892	. . . . . . . . 9 ⊢ ((𝑅 ∈ RingOps ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → ((𝑢𝐻𝑣)𝐻𝑤) = (𝑢𝐻(𝑣𝐻𝑤)))
136	134, 135	sylan2 593	. . . . . . . 8 ⊢ ((𝑅 ∈ RingOps ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → ((𝑢𝐻𝑣)𝐻𝑤) = (𝑢𝐻(𝑣𝐻𝑤)))
137	136	adantlr 715	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → ((𝑢𝐻𝑣)𝐻𝑤) = (𝑢𝐻(𝑣𝐻𝑤)))
138	127, 132, 137	3eqtr4d 2784	. . . . . 6 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → (𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))(𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤)) = ((𝑢𝐻𝑣)𝐻𝑤))
139	120, 123, 138	3eqtr4d 2784	. . . . 5 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → ((𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) = (𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))(𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤)))
140	43	anim1i 615	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → (𝑈 ∈ 𝑋 ∧ 𝑈 ≠ 𝑍))
141	140, 45	sylibr 234	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → 𝑈 ∈ (𝑋 ∖ {𝑍}))
142	141	adantrr 717	. . . . 5 ⊢ ((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) → 𝑈 ∈ (𝑋 ∖ {𝑍}))
143		ovres 7598	. . . . . . . 8 ⊢ ((𝑈 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → (𝑈(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = (𝑈𝐻𝑢))
144	141, 143	sylan 580	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → (𝑈(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = (𝑈𝐻𝑢))
145	2, 42, 6	rngolidm 37923	. . . . . . . . 9 ⊢ ((𝑅 ∈ RingOps ∧ 𝑢 ∈ 𝑋) → (𝑈𝐻𝑢) = 𝑢)
146	84, 145	sylan2 593	. . . . . . . 8 ⊢ ((𝑅 ∈ RingOps ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → (𝑈𝐻𝑢) = 𝑢)
147	146	adantlr 715	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → (𝑈𝐻𝑢) = 𝑢)
148	144, 147	eqtrd 2774	. . . . . 6 ⊢ (((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → (𝑈(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = 𝑢)
149	148	adantlrr 721	. . . . 5 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → (𝑈(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = 𝑢)
150	93	rspcva 3619	. . . . . . . . 9 ⊢ ((𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈) → ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈)
151		oveq1 7437	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (𝑦𝐻𝑢) = (𝑧𝐻𝑢))
152	151	eqeq1d 2736	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → ((𝑦𝐻𝑢) = 𝑈 ↔ (𝑧𝐻𝑢) = 𝑈))
153	152	cbvrexvw 3235	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈 ↔ ∃𝑧 ∈ (𝑋 ∖ {𝑍})(𝑧𝐻𝑢) = 𝑈)
154		ovres 7598	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → (𝑧(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = (𝑧𝐻𝑢))
155	154	eqeq1d 2736	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → ((𝑧(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = 𝑈 ↔ (𝑧𝐻𝑢) = 𝑈))
156	155	ancoms 458	. . . . . . . . . . . 12 ⊢ ((𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑧 ∈ (𝑋 ∖ {𝑍})) → ((𝑧(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = 𝑈 ↔ (𝑧𝐻𝑢) = 𝑈))
157	156	rexbidva 3174	. . . . . . . . . . 11 ⊢ (𝑢 ∈ (𝑋 ∖ {𝑍}) → (∃𝑧 ∈ (𝑋 ∖ {𝑍})(𝑧(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = 𝑈 ↔ ∃𝑧 ∈ (𝑋 ∖ {𝑍})(𝑧𝐻𝑢) = 𝑈))
158	157	biimpar 477	. . . . . . . . . 10 ⊢ ((𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ ∃𝑧 ∈ (𝑋 ∖ {𝑍})(𝑧𝐻𝑢) = 𝑈) → ∃𝑧 ∈ (𝑋 ∖ {𝑍})(𝑧(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = 𝑈)
159	153, 158	sylan2b 594	. . . . . . . . 9 ⊢ ((𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈) → ∃𝑧 ∈ (𝑋 ∖ {𝑍})(𝑧(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = 𝑈)
160	150, 159	syldan 591	. . . . . . . 8 ⊢ ((𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈) → ∃𝑧 ∈ (𝑋 ∖ {𝑍})(𝑧(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = 𝑈)
161	160	ancoms 458	. . . . . . 7 ⊢ ((∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈 ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → ∃𝑧 ∈ (𝑋 ∖ {𝑍})(𝑧(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = 𝑈)
162	161	adantll 714	. . . . . 6 ⊢ (((𝑅 ∈ RingOps ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈) ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → ∃𝑧 ∈ (𝑋 ∖ {𝑍})(𝑧(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = 𝑈)
163	162	adantlrl 720	. . . . 5 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → ∃𝑧 ∈ (𝑋 ∖ {𝑍})(𝑧(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = 𝑈)
164	77, 117, 139, 142, 149, 163	isgrpda 37941	. . . 4 ⊢ ((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) → (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp)
165	72, 164	impbida 801	. . 3 ⊢ (𝑅 ∈ RingOps → ((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp ↔ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)))
166	165	pm5.32i 574	. 2 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ↔ (𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)))
167	5, 166	bitri 275	1 ⊢ (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1536   ∈ wcel 2105   ≠ wne 2937  ∀wral 3058  ∃wrex 3067  Vcvv 3477   ∖ cdif 3959   ∩ cin 3961   ⊆ wss 3962  {csn 4630   × cxp 5686  dom cdm 5688  ran crn 5689   ↾ cres 5690   Fn wfn 6557  ⟶wf 6558  ‘cfv 6562  (class class class)co 7430  1^st c1st 8010  2^nd c2nd 8011  GrpOpcgr 30517  GIdcgi 30518  invcgn 30519   ExId cexid 37830  Magmacmagm 37834  MndOpcmndo 37852  RingOpscrngo 37880  DivRingOpscdrng 37934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-1st 8012  df-2nd 8013  df-1o 8504  df-en 8984  df-grpo 30521  df-gid 30522  df-ginv 30523  df-ablo 30573  df-ass 37829  df-exid 37831  df-mgmOLD 37835  df-sgrOLD 37847  df-mndo 37853  df-rngo 37881  df-drngo 37935

This theorem is referenced by:  isdrngo3  37945  divrngidl  38014