Theorem isdrngo2 37977

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 37975	. 2 ⊢ (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp))
6		isdivrng2.5	. . . . . . 7 ⊢ 𝑈 = (GId‘𝐻)
7	1, 2, 4, 3, 6	dvrunz 37973	. . . . . 6 ⊢ (𝑅 ∈ DivRingOps → 𝑈 ≠ 𝑍)
8	5, 7	sylbir 235	. . . . 5 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → 𝑈 ≠ 𝑍)
9		grporndm 30480	. . . . . . . . . . . 12 ⊢ ((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp → ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = dom dom (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))
10	9	adantl 481	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = dom dom (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))
11		difss 4084	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∖ {𝑍}) ⊆ 𝑋
12		xpss12 5629	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑋 ∖ {𝑍}) ⊆ 𝑋 ∧ (𝑋 ∖ {𝑍}) ⊆ 𝑋) → ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})) ⊆ (𝑋 × 𝑋))
13	11, 11, 12	mp2an 692	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})) ⊆ (𝑋 × 𝑋)
14	1, 2, 4	rngosm 37919	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ RingOps → 𝐻:(𝑋 × 𝑋)⟶𝑋)
15	14	fdmd 6657	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ RingOps → dom 𝐻 = (𝑋 × 𝑋))
16	13, 15	sseqtrrid 3976	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ RingOps → ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})) ⊆ dom 𝐻)
17	16	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})) ⊆ dom 𝐻)
18		ssdmres 5959	. . . . . . . . . . . . . 14 ⊢ (((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})) ⊆ dom 𝐻 ↔ dom (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))
19	17, 18	sylib 218	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → dom (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))
20	19	dmeqd 5843	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → dom dom (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = dom ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))
21		dmxpid 5867	. . . . . . . . . . . 12 ⊢ dom ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})) = (𝑋 ∖ {𝑍})
22	20, 21	eqtrdi 2781	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → dom dom (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = (𝑋 ∖ {𝑍}))
23	10, 22	eqtrd 2765	. . . . . . . . . 10 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = (𝑋 ∖ {𝑍}))
24	23	eleq2d 2815	. . . . . . . . 9 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → (𝑥 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ↔ 𝑥 ∈ (𝑋 ∖ {𝑍})))
25	24	biimpar 477	. . . . . . . 8 ⊢ (((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → 𝑥 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))
26		eqid 2730	. . . . . . . . . . 11 ⊢ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))
27		eqid 2730	. . . . . . . . . . 11 ⊢ (inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) = (inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))
28	26, 27	grpoinvcl 30494	. . . . . . . . . 10 ⊢ (((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp ∧ 𝑥 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) → ((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥) ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))
29	28	adantll 714	. . . . . . . . 9 ⊢ (((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ∧ 𝑥 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) → ((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥) ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))
30		eqid 2730	. . . . . . . . . . . 12 ⊢ (GId‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) = (GId‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))
31	26, 30, 27	grpolinv 30496	. . . . . . . . . . 11 ⊢ (((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp ∧ 𝑥 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) → (((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = (GId‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))))
32	31	adantll 714	. . . . . . . . . 10 ⊢ (((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ∧ 𝑥 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) → (((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = (GId‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))))
33	2	rngomndo 37954	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ RingOps → 𝐻 ∈ MndOp)
34		mndomgmid 37890	. . . . . . . . . . . . . 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 3981	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∖ {𝑍}) ⊆ ran 𝐺
38	2, 1	rngorn1eq 37953	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ RingOps → ran 𝐺 = ran 𝐻)
39	37, 38	sseqtrid 3975	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ RingOps → (𝑋 ∖ {𝑍}) ⊆ ran 𝐻)
40	39	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → (𝑋 ∖ {𝑍}) ⊆ ran 𝐻)
41	1	rneqi 5874	. . . . . . . . . . . . . . . 16 ⊢ ran 𝐺 = ran (1st ‘𝑅)
42	4, 41	eqtri 2753	. . . . . . . . . . . . . . 15 ⊢ 𝑋 = ran (1st ‘𝑅)
43	42, 2, 6	rngo1cl 37958	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ RingOps → 𝑈 ∈ 𝑋)
44	43	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → 𝑈 ∈ 𝑋)
45		eldifsn 4736	. . . . . . . . . . . . 13 ⊢ (𝑈 ∈ (𝑋 ∖ {𝑍}) ↔ (𝑈 ∈ 𝑋 ∧ 𝑈 ≠ 𝑍))
46	44, 8, 45	sylanbrc 583	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → 𝑈 ∈ (𝑋 ∖ {𝑍}))
47		grpomndo 37894	. . . . . . . . . . . . . 14 ⊢ ((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp → (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ MndOp)
48		mndoismgmOLD 37889	. . . . . . . . . . . . . 14 ⊢ ((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ MndOp → (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ Magma)
49	47, 48	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp → (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ Magma)
50	49	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ Magma)
51		eqid 2730	. . . . . . . . . . . . 13 ⊢ ran 𝐻 = ran 𝐻
52		eqid 2730	. . . . . . . . . . . . 13 ⊢ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))
53	51, 6, 52	exidresid 37898	. . . . . . . . . . . 12 ⊢ (((𝐻 ∈ (Magma ∩ ExId ) ∧ (𝑋 ∖ {𝑍}) ⊆ ran 𝐻 ∧ 𝑈 ∈ (𝑋 ∖ {𝑍})) ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ Magma) → (GId‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) = 𝑈)
54	36, 40, 46, 50, 53	syl31anc 1375	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → (GId‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) = 𝑈)
55	54	adantr 480	. . . . . . . . . 10 ⊢ (((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ∧ 𝑥 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) → (GId‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) = 𝑈)
56	32, 55	eqtrd 2765	. . . . . . . . 9 ⊢ (((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ∧ 𝑥 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) → (((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = 𝑈)
57		oveq1 7348	. . . . . . . . . . 11 ⊢ (𝑦 = ((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥) → (𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = (((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥))
58	57	eqeq1d 2732	. . . . . . . . . 10 ⊢ (𝑦 = ((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥) → ((𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = 𝑈 ↔ (((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = 𝑈))
59	58	rspcev 3575	. . . . . . . . 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 3291	. . . . . . . 8 ⊢ (((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (∃𝑦 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))(𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = 𝑈 ↔ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = 𝑈))
64		ovres 7507	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = (𝑦𝐻𝑥))
65	64	ancoms 458	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑦 ∈ (𝑋 ∖ {𝑍})) → (𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = (𝑦𝐻𝑥))
66	65	eqeq1d 2732	. . . . . . . . . 10 ⊢ ((𝑥 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑦 ∈ (𝑋 ∖ {𝑍})) → ((𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = 𝑈 ↔ (𝑦𝐻𝑥) = 𝑈))
67	66	rexbidva 3152	. . . . . . . . 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 3122	. . . . 5 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)
72	8, 71	jca 511	. . . 4 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈))
73	1	fvexi 6831	. . . . . . . 8 ⊢ 𝐺 ∈ V
74	73	rnex 7835	. . . . . . 7 ⊢ ran 𝐺 ∈ V
75	4, 74	eqeltri 2825	. . . . . 6 ⊢ 𝑋 ∈ V
76		difexg 5265	. . . . . 6 ⊢ (𝑋 ∈ V → (𝑋 ∖ {𝑍}) ∈ V)
77	75, 76	mp1i 13	. . . . 5 ⊢ ((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) → (𝑋 ∖ {𝑍}) ∈ V)
78	14	ffnd 6648	. . . . . . . 8 ⊢ (𝑅 ∈ RingOps → 𝐻 Fn (𝑋 × 𝑋))
79	78	adantr 480	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) → 𝐻 Fn (𝑋 × 𝑋))
80		fnssres 6600	. . . . . . 7 ⊢ ((𝐻 Fn (𝑋 × 𝑋) ∧ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})) ⊆ (𝑋 × 𝑋)) → (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) Fn ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))
81	79, 13, 80	sylancl 586	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) → (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) Fn ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))
82		ovres 7507	. . . . . . . . 9 ⊢ ((𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍})) → (𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣) = (𝑢𝐻𝑣))
83	82	adantl 481	. . . . . . . 8 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}))) → (𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣) = (𝑢𝐻𝑣))
84		eldifi 4079	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ (𝑋 ∖ {𝑍}) → 𝑢 ∈ 𝑋)
85		eldifi 4079	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ (𝑋 ∖ {𝑍}) → 𝑣 ∈ 𝑋)
86	84, 85	anim12i 613	. . . . . . . . . . 11 ⊢ ((𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍})) → (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋))
87	1, 2, 4	rngocl 37920	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ RingOps ∧ 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋) → (𝑢𝐻𝑣) ∈ 𝑋)
88	87	3expb 1120	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ RingOps ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑢𝐻𝑣) ∈ 𝑋)
89	86, 88	sylan2 593	. . . . . . . . . 10 ⊢ ((𝑅 ∈ RingOps ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}))) → (𝑢𝐻𝑣) ∈ 𝑋)
90	89	adantlr 715	. . . . . . . . 9 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}))) → (𝑢𝐻𝑣) ∈ 𝑋)
91		oveq2 7349	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑢 → (𝑦𝐻𝑥) = (𝑦𝐻𝑢))
92	91	eqeq1d 2732	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑢 → ((𝑦𝐻𝑥) = 𝑈 ↔ (𝑦𝐻𝑢) = 𝑈))
93	92	rexbidv 3154	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑢 → (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈 ↔ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈))
94	93	rspcv 3571	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ (𝑋 ∖ {𝑍}) → (∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈 → ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈))
95	94	imdistanri 569	. . . . . . . . . . . 12 ⊢ ((∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈 ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈 ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})))
96		eldifsn 4736	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ (𝑋 ∖ {𝑍}) ↔ (𝑣 ∈ 𝑋 ∧ 𝑣 ≠ 𝑍))
97		ssrexv 4002	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑋 ∖ {𝑍}) ⊆ 𝑋 → (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈 → ∃𝑦 ∈ 𝑋 (𝑦𝐻𝑢) = 𝑈))
98	11, 97	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈 → ∃𝑦 ∈ 𝑋 (𝑦𝐻𝑢) = 𝑈)
99	1, 2, 3, 4, 6	zerdivemp1x 37966	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ RingOps ∧ 𝑢 ∈ 𝑋 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐻𝑢) = 𝑈) → (𝑣 ∈ 𝑋 → ((𝑢𝐻𝑣) = 𝑍 → 𝑣 = 𝑍)))
100	98, 99	syl3an3 1165	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ RingOps ∧ 𝑢 ∈ 𝑋 ∧ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈) → (𝑣 ∈ 𝑋 → ((𝑢𝐻𝑣) = 𝑍 → 𝑣 = 𝑍)))
101	84, 100	syl3an2 1164	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ RingOps ∧ 𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈) → (𝑣 ∈ 𝑋 → ((𝑢𝐻𝑣) = 𝑍 → 𝑣 = 𝑍)))
102	101	3expb 1120	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ RingOps ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈)) → (𝑣 ∈ 𝑋 → ((𝑢𝐻𝑣) = 𝑍 → 𝑣 = 𝑍)))
103	102	imp 406	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ RingOps ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈)) ∧ 𝑣 ∈ 𝑋) → ((𝑢𝐻𝑣) = 𝑍 → 𝑣 = 𝑍))
104	103	necon3d 2947	. . . . . . . . . . . . . . . 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 4736	. . . . . . . . 9 ⊢ ((𝑢𝐻𝑣) ∈ (𝑋 ∖ {𝑍}) ↔ ((𝑢𝐻𝑣) ∈ 𝑋 ∧ (𝑢𝐻𝑣) ≠ 𝑍))
113	90, 111, 112	sylanbrc 583	. . . . . . . 8 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}))) → (𝑢𝐻𝑣) ∈ (𝑋 ∖ {𝑍}))
114	83, 113	eqeltrd 2829	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}))) → (𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣) ∈ (𝑋 ∖ {𝑍}))
115	114	ralrimivva 3173	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) → ∀𝑢 ∈ (𝑋 ∖ {𝑍})∀𝑣 ∈ (𝑋 ∖ {𝑍})(𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣) ∈ (𝑋 ∖ {𝑍}))
116		ffnov 7467	. . . . . 6 ⊢ ((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))):((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))⟶(𝑋 ∖ {𝑍}) ↔ ((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) Fn ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})) ∧ ∀𝑢 ∈ (𝑋 ∖ {𝑍})∀𝑣 ∈ (𝑋 ∖ {𝑍})(𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣) ∈ (𝑋 ∖ {𝑍})))
117	81, 115, 116	sylanbrc 583	. . . . 5 ⊢ ((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) → (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))):((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))⟶(𝑋 ∖ {𝑍}))
118	113	3adantr3 1172	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → (𝑢𝐻𝑣) ∈ (𝑋 ∖ {𝑍}))
119		simpr3 1197	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → 𝑤 ∈ (𝑋 ∖ {𝑍}))
120	118, 119	ovresd 7508	. . . . . 6 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → ((𝑢𝐻𝑣)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) = ((𝑢𝐻𝑣)𝐻𝑤))
121	82	3adant3 1132	. . . . . . . 8 ⊢ ((𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍})) → (𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣) = (𝑢𝐻𝑣))
122	121	adantl 481	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → (𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣) = (𝑢𝐻𝑣))
123	122	oveq1d 7356	. . . . . 6 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → ((𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) = ((𝑢𝐻𝑣)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤))
124		ovres 7507	. . . . . . . . . 10 ⊢ ((𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍})) → (𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) = (𝑣𝐻𝑤))
125	124	3adant1 1130	. . . . . . . . 9 ⊢ ((𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍})) → (𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) = (𝑣𝐻𝑤))
126	125	adantl 481	. . . . . . . 8 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → (𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) = (𝑣𝐻𝑤))
127	126	oveq2d 7357	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → (𝑢𝐻(𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤)) = (𝑢𝐻(𝑣𝐻𝑤)))
128		simpr1 1195	. . . . . . . 8 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → 𝑢 ∈ (𝑋 ∖ {𝑍}))
129		fovcdm 7511	. . . . . . . . . 10 ⊢ (((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))):((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))⟶(𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍})) → (𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) ∈ (𝑋 ∖ {𝑍}))
130	129	3adant3r1 1183	. . . . . . . . 9 ⊢ (((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))):((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))⟶(𝑋 ∖ {𝑍}) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → (𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) ∈ (𝑋 ∖ {𝑍}))
131	117, 130	sylan 580	. . . . . . . 8 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → (𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) ∈ (𝑋 ∖ {𝑍}))
132	128, 131	ovresd 7508	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → (𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))(𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤)) = (𝑢𝐻(𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤)))
133		eldifi 4079	. . . . . . . . . 10 ⊢ (𝑤 ∈ (𝑋 ∖ {𝑍}) → 𝑤 ∈ 𝑋)
134	84, 85, 133	3anim123i 1151	. . . . . . . . 9 ⊢ ((𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍})) → (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋))
135	1, 2, 4	rngoass 37925	. . . . . . . . 9 ⊢ ((𝑅 ∈ RingOps ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → ((𝑢𝐻𝑣)𝐻𝑤) = (𝑢𝐻(𝑣𝐻𝑤)))
136	134, 135	sylan2 593	. . . . . . . 8 ⊢ ((𝑅 ∈ RingOps ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → ((𝑢𝐻𝑣)𝐻𝑤) = (𝑢𝐻(𝑣𝐻𝑤)))
137	136	adantlr 715	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → ((𝑢𝐻𝑣)𝐻𝑤) = (𝑢𝐻(𝑣𝐻𝑤)))
138	127, 132, 137	3eqtr4d 2775	. . . . . 6 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → (𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))(𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤)) = ((𝑢𝐻𝑣)𝐻𝑤))
139	120, 123, 138	3eqtr4d 2775	. . . . 5 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → ((𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) = (𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))(𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤)))
140	43	anim1i 615	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → (𝑈 ∈ 𝑋 ∧ 𝑈 ≠ 𝑍))
141	140, 45	sylibr 234	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → 𝑈 ∈ (𝑋 ∖ {𝑍}))
142	141	adantrr 717	. . . . 5 ⊢ ((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) → 𝑈 ∈ (𝑋 ∖ {𝑍}))
143		ovres 7507	. . . . . . . 8 ⊢ ((𝑈 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → (𝑈(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = (𝑈𝐻𝑢))
144	141, 143	sylan 580	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → (𝑈(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = (𝑈𝐻𝑢))
145	2, 42, 6	rngolidm 37956	. . . . . . . . 9 ⊢ ((𝑅 ∈ RingOps ∧ 𝑢 ∈ 𝑋) → (𝑈𝐻𝑢) = 𝑢)
146	84, 145	sylan2 593	. . . . . . . 8 ⊢ ((𝑅 ∈ RingOps ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → (𝑈𝐻𝑢) = 𝑢)
147	146	adantlr 715	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → (𝑈𝐻𝑢) = 𝑢)
148	144, 147	eqtrd 2765	. . . . . 6 ⊢ (((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → (𝑈(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = 𝑢)
149	148	adantlrr 721	. . . . 5 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → (𝑈(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = 𝑢)
150	93	rspcva 3573	. . . . . . . . 9 ⊢ ((𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈) → ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈)
151		oveq1 7348	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (𝑦𝐻𝑢) = (𝑧𝐻𝑢))
152	151	eqeq1d 2732	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → ((𝑦𝐻𝑢) = 𝑈 ↔ (𝑧𝐻𝑢) = 𝑈))
153	152	cbvrexvw 3209	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈 ↔ ∃𝑧 ∈ (𝑋 ∖ {𝑍})(𝑧𝐻𝑢) = 𝑈)
154		ovres 7507	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → (𝑧(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = (𝑧𝐻𝑢))
155	154	eqeq1d 2732	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → ((𝑧(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = 𝑈 ↔ (𝑧𝐻𝑢) = 𝑈))
156	155	ancoms 458	. . . . . . . . . . . 12 ⊢ ((𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑧 ∈ (𝑋 ∖ {𝑍})) → ((𝑧(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = 𝑈 ↔ (𝑧𝐻𝑢) = 𝑈))
157	156	rexbidva 3152	. . . . . . . . . . 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 37974	. . . 4 ⊢ ((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) → (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp)
165	72, 164	impbida 800	. . 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 1541   ∈ wcel 2110   ≠ wne 2926  ∀wral 3045  ∃wrex 3054  Vcvv 3434   ∖ cdif 3897   ∩ cin 3899   ⊆ wss 3900  {csn 4574   × cxp 5612  dom cdm 5614  ran crn 5615   ↾ cres 5616   Fn wfn 6472  ⟶wf 6473  ‘cfv 6477  (class class class)co 7341  1^st c1st 7914  2^nd c2nd 7915  GrpOpcgr 30459  GIdcgi 30460  invcgn 30461   ExId cexid 37863  Magmacmagm 37867  MndOpcmndo 37885  RingOpscrngo 37913  DivRingOpscdrng 37967

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 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702  ax-rep 5215  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7663

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rmo 3344  df-reu 3345  df-rab 3394  df-v 3436  df-sbc 3740  df-csb 3849  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4282  df-if 4474  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-iun 4941  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-suc 6308  df-iota 6433  df-fun 6479  df-fn 6480  df-f 6481  df-f1 6482  df-fo 6483  df-f1o 6484  df-fv 6485  df-riota 7298  df-ov 7344  df-1st 7916  df-2nd 7917  df-1o 8380  df-en 8865  df-grpo 30463  df-gid 30464  df-ginv 30465  df-ablo 30515  df-ass 37862  df-exid 37864  df-mgmOLD 37868  df-sgrOLD 37880  df-mndo 37886  df-rngo 37914  df-drngo 37968

This theorem is referenced by:  isdrngo3  37978  divrngidl  38047