Theorem isdrngo2 37937

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 37935	. 2 ⊢ (𝑅 ∈ DivRingOps ↔ (𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp))
6		isdivrng2.5	. . . . . . 7 ⊢ 𝑈 = (GId‘𝐻)
7	1, 2, 4, 3, 6	dvrunz 37933	. . . . . 6 ⊢ (𝑅 ∈ DivRingOps → 𝑈 ≠ 𝑍)
8	5, 7	sylbir 235	. . . . 5 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → 𝑈 ≠ 𝑍)
9		grporndm 30472	. . . . . . . . . . . 12 ⊢ ((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp → ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = dom dom (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))
10	9	adantl 481	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = dom dom (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))
11		difss 4089	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∖ {𝑍}) ⊆ 𝑋
12		xpss12 5638	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑋 ∖ {𝑍}) ⊆ 𝑋 ∧ (𝑋 ∖ {𝑍}) ⊆ 𝑋) → ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})) ⊆ (𝑋 × 𝑋))
13	11, 11, 12	mp2an 692	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})) ⊆ (𝑋 × 𝑋)
14	1, 2, 4	rngosm 37879	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ RingOps → 𝐻:(𝑋 × 𝑋)⟶𝑋)
15	14	fdmd 6666	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ RingOps → dom 𝐻 = (𝑋 × 𝑋))
16	13, 15	sseqtrrid 3981	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ RingOps → ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})) ⊆ dom 𝐻)
17	16	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})) ⊆ dom 𝐻)
18		ssdmres 5968	. . . . . . . . . . . . . 14 ⊢ (((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})) ⊆ dom 𝐻 ↔ dom (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))
19	17, 18	sylib 218	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → dom (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))
20	19	dmeqd 5852	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → dom dom (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = dom ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))
21		dmxpid 5876	. . . . . . . . . . . 12 ⊢ dom ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})) = (𝑋 ∖ {𝑍})
22	20, 21	eqtrdi 2780	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → dom dom (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = (𝑋 ∖ {𝑍}))
23	10, 22	eqtrd 2764	. . . . . . . . . 10 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = (𝑋 ∖ {𝑍}))
24	23	eleq2d 2814	. . . . . . . . 9 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → (𝑥 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ↔ 𝑥 ∈ (𝑋 ∖ {𝑍})))
25	24	biimpar 477	. . . . . . . 8 ⊢ (((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → 𝑥 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))
26		eqid 2729	. . . . . . . . . . 11 ⊢ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))
27		eqid 2729	. . . . . . . . . . 11 ⊢ (inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) = (inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))
28	26, 27	grpoinvcl 30486	. . . . . . . . . 10 ⊢ (((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp ∧ 𝑥 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) → ((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥) ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))
29	28	adantll 714	. . . . . . . . 9 ⊢ (((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ∧ 𝑥 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) → ((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥) ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))
30		eqid 2729	. . . . . . . . . . . 12 ⊢ (GId‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) = (GId‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))
31	26, 30, 27	grpolinv 30488	. . . . . . . . . . 11 ⊢ (((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp ∧ 𝑥 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) → (((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = (GId‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))))
32	31	adantll 714	. . . . . . . . . 10 ⊢ (((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ∧ 𝑥 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) → (((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = (GId‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))))
33	2	rngomndo 37914	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ RingOps → 𝐻 ∈ MndOp)
34		mndomgmid 37850	. . . . . . . . . . . . . 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 3986	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∖ {𝑍}) ⊆ ran 𝐺
38	2, 1	rngorn1eq 37913	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ RingOps → ran 𝐺 = ran 𝐻)
39	37, 38	sseqtrid 3980	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ RingOps → (𝑋 ∖ {𝑍}) ⊆ ran 𝐻)
40	39	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → (𝑋 ∖ {𝑍}) ⊆ ran 𝐻)
41	1	rneqi 5883	. . . . . . . . . . . . . . . 16 ⊢ ran 𝐺 = ran (1st ‘𝑅)
42	4, 41	eqtri 2752	. . . . . . . . . . . . . . 15 ⊢ 𝑋 = ran (1st ‘𝑅)
43	42, 2, 6	rngo1cl 37918	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ RingOps → 𝑈 ∈ 𝑋)
44	43	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → 𝑈 ∈ 𝑋)
45		eldifsn 4740	. . . . . . . . . . . . 13 ⊢ (𝑈 ∈ (𝑋 ∖ {𝑍}) ↔ (𝑈 ∈ 𝑋 ∧ 𝑈 ≠ 𝑍))
46	44, 8, 45	sylanbrc 583	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → 𝑈 ∈ (𝑋 ∖ {𝑍}))
47		grpomndo 37854	. . . . . . . . . . . . . 14 ⊢ ((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp → (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ MndOp)
48		mndoismgmOLD 37849	. . . . . . . . . . . . . 14 ⊢ ((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ MndOp → (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ Magma)
49	47, 48	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp → (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ Magma)
50	49	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ Magma)
51		eqid 2729	. . . . . . . . . . . . 13 ⊢ ran 𝐻 = ran 𝐻
52		eqid 2729	. . . . . . . . . . . . 13 ⊢ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) = (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))
53	51, 6, 52	exidresid 37858	. . . . . . . . . . . 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 2764	. . . . . . . . 9 ⊢ (((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) ∧ 𝑥 ∈ ran (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))) → (((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = 𝑈)
57		oveq1 7360	. . . . . . . . . . 11 ⊢ (𝑦 = ((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥) → (𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = (((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥))
58	57	eqeq1d 2731	. . . . . . . . . 10 ⊢ (𝑦 = ((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥) → ((𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = 𝑈 ↔ (((inv‘(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))))‘𝑥)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = 𝑈))
59	58	rspcev 3579	. . . . . . . . 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 7519	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = (𝑦𝐻𝑥))
65	64	ancoms 458	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑦 ∈ (𝑋 ∖ {𝑍})) → (𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = (𝑦𝐻𝑥))
66	65	eqeq1d 2731	. . . . . . . . . 10 ⊢ ((𝑥 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑦 ∈ (𝑋 ∖ {𝑍})) → ((𝑦(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑥) = 𝑈 ↔ (𝑦𝐻𝑥) = 𝑈))
67	66	rexbidva 3151	. . . . . . . . 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 3121	. . . . 5 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)
72	8, 71	jca 511	. . . 4 ⊢ ((𝑅 ∈ RingOps ∧ (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) ∈ GrpOp) → (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈))
73	1	fvexi 6840	. . . . . . . 8 ⊢ 𝐺 ∈ V
74	73	rnex 7850	. . . . . . 7 ⊢ ran 𝐺 ∈ V
75	4, 74	eqeltri 2824	. . . . . 6 ⊢ 𝑋 ∈ V
76		difexg 5271	. . . . . 6 ⊢ (𝑋 ∈ V → (𝑋 ∖ {𝑍}) ∈ V)
77	75, 76	mp1i 13	. . . . 5 ⊢ ((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) → (𝑋 ∖ {𝑍}) ∈ V)
78	14	ffnd 6657	. . . . . . . 8 ⊢ (𝑅 ∈ RingOps → 𝐻 Fn (𝑋 × 𝑋))
79	78	adantr 480	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) → 𝐻 Fn (𝑋 × 𝑋))
80		fnssres 6609	. . . . . . 7 ⊢ ((𝐻 Fn (𝑋 × 𝑋) ∧ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})) ⊆ (𝑋 × 𝑋)) → (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) Fn ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))
81	79, 13, 80	sylancl 586	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) → (𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))) Fn ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))
82		ovres 7519	. . . . . . . . 9 ⊢ ((𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍})) → (𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣) = (𝑢𝐻𝑣))
83	82	adantl 481	. . . . . . . 8 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}))) → (𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣) = (𝑢𝐻𝑣))
84		eldifi 4084	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ (𝑋 ∖ {𝑍}) → 𝑢 ∈ 𝑋)
85		eldifi 4084	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ (𝑋 ∖ {𝑍}) → 𝑣 ∈ 𝑋)
86	84, 85	anim12i 613	. . . . . . . . . . 11 ⊢ ((𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍})) → (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋))
87	1, 2, 4	rngocl 37880	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ RingOps ∧ 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋) → (𝑢𝐻𝑣) ∈ 𝑋)
88	87	3expb 1120	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ RingOps ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑢𝐻𝑣) ∈ 𝑋)
89	86, 88	sylan2 593	. . . . . . . . . 10 ⊢ ((𝑅 ∈ RingOps ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}))) → (𝑢𝐻𝑣) ∈ 𝑋)
90	89	adantlr 715	. . . . . . . . 9 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}))) → (𝑢𝐻𝑣) ∈ 𝑋)
91		oveq2 7361	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑢 → (𝑦𝐻𝑥) = (𝑦𝐻𝑢))
92	91	eqeq1d 2731	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑢 → ((𝑦𝐻𝑥) = 𝑈 ↔ (𝑦𝐻𝑢) = 𝑈))
93	92	rexbidv 3153	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑢 → (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈 ↔ ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈))
94	93	rspcv 3575	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ (𝑋 ∖ {𝑍}) → (∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈 → ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈))
95	94	imdistanri 569	. . . . . . . . . . . 12 ⊢ ((∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈 ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈 ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})))
96		eldifsn 4740	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ (𝑋 ∖ {𝑍}) ↔ (𝑣 ∈ 𝑋 ∧ 𝑣 ≠ 𝑍))
97		ssrexv 4007	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑋 ∖ {𝑍}) ⊆ 𝑋 → (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈 → ∃𝑦 ∈ 𝑋 (𝑦𝐻𝑢) = 𝑈))
98	11, 97	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈 → ∃𝑦 ∈ 𝑋 (𝑦𝐻𝑢) = 𝑈)
99	1, 2, 3, 4, 6	zerdivemp1x 37926	. . . . . . . . . . . . . . . . . . . . 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 2946	. . . . . . . . . . . . . . . 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 4740	. . . . . . . . 9 ⊢ ((𝑢𝐻𝑣) ∈ (𝑋 ∖ {𝑍}) ↔ ((𝑢𝐻𝑣) ∈ 𝑋 ∧ (𝑢𝐻𝑣) ≠ 𝑍))
113	90, 111, 112	sylanbrc 583	. . . . . . . 8 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}))) → (𝑢𝐻𝑣) ∈ (𝑋 ∖ {𝑍}))
114	83, 113	eqeltrd 2828	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}))) → (𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣) ∈ (𝑋 ∖ {𝑍}))
115	114	ralrimivva 3172	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) → ∀𝑢 ∈ (𝑋 ∖ {𝑍})∀𝑣 ∈ (𝑋 ∖ {𝑍})(𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣) ∈ (𝑋 ∖ {𝑍}))
116		ffnov 7479	. . . . . 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 7520	. . . . . 6 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → ((𝑢𝐻𝑣)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) = ((𝑢𝐻𝑣)𝐻𝑤))
121	82	3adant3 1132	. . . . . . . 8 ⊢ ((𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍})) → (𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣) = (𝑢𝐻𝑣))
122	121	adantl 481	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → (𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣) = (𝑢𝐻𝑣))
123	122	oveq1d 7368	. . . . . 6 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → ((𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) = ((𝑢𝐻𝑣)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤))
124		ovres 7519	. . . . . . . . . 10 ⊢ ((𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍})) → (𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) = (𝑣𝐻𝑤))
125	124	3adant1 1130	. . . . . . . . 9 ⊢ ((𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍})) → (𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) = (𝑣𝐻𝑤))
126	125	adantl 481	. . . . . . . 8 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → (𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) = (𝑣𝐻𝑤))
127	126	oveq2d 7369	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → (𝑢𝐻(𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤)) = (𝑢𝐻(𝑣𝐻𝑤)))
128		simpr1 1195	. . . . . . . 8 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → 𝑢 ∈ (𝑋 ∖ {𝑍}))
129		fovcdm 7523	. . . . . . . . . 10 ⊢ (((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))):((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))⟶(𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍})) → (𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) ∈ (𝑋 ∖ {𝑍}))
130	129	3adant3r1 1183	. . . . . . . . 9 ⊢ (((𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))):((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍}))⟶(𝑋 ∖ {𝑍}) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → (𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) ∈ (𝑋 ∖ {𝑍}))
131	117, 130	sylan 580	. . . . . . . 8 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → (𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) ∈ (𝑋 ∖ {𝑍}))
132	128, 131	ovresd 7520	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → (𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))(𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤)) = (𝑢𝐻(𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤)))
133		eldifi 4084	. . . . . . . . . 10 ⊢ (𝑤 ∈ (𝑋 ∖ {𝑍}) → 𝑤 ∈ 𝑋)
134	84, 85, 133	3anim123i 1151	. . . . . . . . 9 ⊢ ((𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍})) → (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋))
135	1, 2, 4	rngoass 37885	. . . . . . . . 9 ⊢ ((𝑅 ∈ RingOps ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → ((𝑢𝐻𝑣)𝐻𝑤) = (𝑢𝐻(𝑣𝐻𝑤)))
136	134, 135	sylan2 593	. . . . . . . 8 ⊢ ((𝑅 ∈ RingOps ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → ((𝑢𝐻𝑣)𝐻𝑤) = (𝑢𝐻(𝑣𝐻𝑤)))
137	136	adantlr 715	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → ((𝑢𝐻𝑣)𝐻𝑤) = (𝑢𝐻(𝑣𝐻𝑤)))
138	127, 132, 137	3eqtr4d 2774	. . . . . 6 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → (𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))(𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤)) = ((𝑢𝐻𝑣)𝐻𝑤))
139	120, 123, 138	3eqtr4d 2774	. . . . 5 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ (𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑣 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑤 ∈ (𝑋 ∖ {𝑍}))) → ((𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑣)(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤) = (𝑢(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))(𝑣(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑤)))
140	43	anim1i 615	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → (𝑈 ∈ 𝑋 ∧ 𝑈 ≠ 𝑍))
141	140, 45	sylibr 234	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → 𝑈 ∈ (𝑋 ∖ {𝑍}))
142	141	adantrr 717	. . . . 5 ⊢ ((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) → 𝑈 ∈ (𝑋 ∖ {𝑍}))
143		ovres 7519	. . . . . . . 8 ⊢ ((𝑈 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → (𝑈(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = (𝑈𝐻𝑢))
144	141, 143	sylan 580	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → (𝑈(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = (𝑈𝐻𝑢))
145	2, 42, 6	rngolidm 37916	. . . . . . . . 9 ⊢ ((𝑅 ∈ RingOps ∧ 𝑢 ∈ 𝑋) → (𝑈𝐻𝑢) = 𝑢)
146	84, 145	sylan2 593	. . . . . . . 8 ⊢ ((𝑅 ∈ RingOps ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → (𝑈𝐻𝑢) = 𝑢)
147	146	adantlr 715	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → (𝑈𝐻𝑢) = 𝑢)
148	144, 147	eqtrd 2764	. . . . . 6 ⊢ (((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → (𝑈(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = 𝑢)
149	148	adantlrr 721	. . . . 5 ⊢ (((𝑅 ∈ RingOps ∧ (𝑈 ≠ 𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈)) ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → (𝑈(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = 𝑢)
150	93	rspcva 3577	. . . . . . . . 9 ⊢ ((𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑥) = 𝑈) → ∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈)
151		oveq1 7360	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (𝑦𝐻𝑢) = (𝑧𝐻𝑢))
152	151	eqeq1d 2731	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → ((𝑦𝐻𝑢) = 𝑈 ↔ (𝑧𝐻𝑢) = 𝑈))
153	152	cbvrexvw 3208	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ (𝑋 ∖ {𝑍})(𝑦𝐻𝑢) = 𝑈 ↔ ∃𝑧 ∈ (𝑋 ∖ {𝑍})(𝑧𝐻𝑢) = 𝑈)
154		ovres 7519	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → (𝑧(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = (𝑧𝐻𝑢))
155	154	eqeq1d 2731	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑢 ∈ (𝑋 ∖ {𝑍})) → ((𝑧(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = 𝑈 ↔ (𝑧𝐻𝑢) = 𝑈))
156	155	ancoms 458	. . . . . . . . . . . 12 ⊢ ((𝑢 ∈ (𝑋 ∖ {𝑍}) ∧ 𝑧 ∈ (𝑋 ∖ {𝑍})) → ((𝑧(𝐻 ↾ ((𝑋 ∖ {𝑍}) × (𝑋 ∖ {𝑍})))𝑢) = 𝑈 ↔ (𝑧𝐻𝑢) = 𝑈))
157	156	rexbidva 3151	. . . . . . . . . . 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 37934	. . . 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 1540   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  ∃wrex 3053  Vcvv 3438   ∖ cdif 3902   ∩ cin 3904   ⊆ wss 3905  {csn 4579   × cxp 5621  dom cdm 5623  ran crn 5624   ↾ cres 5625   Fn wfn 6481  ⟶wf 6482  ‘cfv 6486  (class class class)co 7353  1^st c1st 7929  2^nd c2nd 7930  GrpOpcgr 30451  GIdcgi 30452  invcgn 30453   ExId cexid 37823  Magmacmagm 37827  MndOpcmndo 37845  RingOpscrngo 37873  DivRingOpscdrng 37927

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5221  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rmo 3345  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-riota 7310  df-ov 7356  df-1st 7931  df-2nd 7932  df-1o 8395  df-en 8880  df-grpo 30455  df-gid 30456  df-ginv 30457  df-ablo 30507  df-ass 37822  df-exid 37824  df-mgmOLD 37828  df-sgrOLD 37840  df-mndo 37846  df-rngo 37874  df-drngo 37928

This theorem is referenced by:  isdrngo3  37938  divrngidl  38007