isdrngo2

Description: Obsolete theorem, use isdrng3 instead. A division ring is a ring in which 1 =/= 0 and every nonzero element is invertible. (Contributed by Jeff Madsen, 8-Jun-2010) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	isdivrng1.1	$⊢ G = 1^{st} (R)$
	isdivrng1.2	$⊢ H = 2^{nd} (R)$
	isdivrng1.3	$⊢ Z = GId (G)$
	isdivrng1.4	$⊢ X = ran G$
	isdivrng2.5	$⊢ U = GId (H)$
Assertion	isdrngo2	$⊢ R \in DivRingOps \leftrightarrow (R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U))$

Proof

Step	Hyp	Ref	Expression
1		isdivrng1.1	$⊢ G = 1^{st} (R)$
2		isdivrng1.2	$⊢ H = 2^{nd} (R)$
3		isdivrng1.3	$⊢ Z = GId (G)$
4		isdivrng1.4	$⊢ X = ran G$
5		isdivrng2.5	$⊢ U = GId (H)$
6	1 2 3 4	isdrngo1	$⊢ R \in DivRingOps \leftrightarrow (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp)$
7	1 2 4 3 5	dvrunz	$⊢ R \in DivRingOps \to U \neq Z$
8	6 7	sylbir	$⊢ (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \to U \neq Z$
9		grporndm	$⊢ {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp \to ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) = dom dom ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))})$
10	9	adantl	$⊢ (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \to ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) = dom dom ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))})$
11		difss	$⊢ X ∖ \{Z\} \subseteq X$
12		xpss12	$⊢ (X ∖ \{Z\} \subseteq X \land X ∖ \{Z\} \subseteq X) \to (X ∖ \{Z\}) \times (X ∖ \{Z\}) \subseteq X \times X$
13	11 11 12	mp2an	$⊢ (X ∖ \{Z\}) \times (X ∖ \{Z\}) \subseteq X \times X$
14	1 2 4	rngosm	$⊢ R \in RingOps \to H : X \times X ⟶ X$
15	14	fdmd	$⊢ R \in RingOps \to dom H = X \times X$
16	13 15	sseqtrrid	$⊢ R \in RingOps \to (X ∖ \{Z\}) \times (X ∖ \{Z\}) \subseteq dom H$
17	16	adantr	$⊢ (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \to (X ∖ \{Z\}) \times (X ∖ \{Z\}) \subseteq dom H$
18		ssdmres	$⊢ (X ∖ \{Z\}) \times (X ∖ \{Z\}) \subseteq dom H \leftrightarrow dom ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) = (X ∖ \{Z\}) \times (X ∖ \{Z\})$
19	17 18	sylib	$⊢ (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \to dom ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) = (X ∖ \{Z\}) \times (X ∖ \{Z\})$
20	19	dmeqd	$⊢ (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \to dom dom ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) = dom ((X ∖ \{Z\}) \times (X ∖ \{Z\}))$
21		dmxpid	$⊢ dom ((X ∖ \{Z\}) \times (X ∖ \{Z\})) = X ∖ \{Z\}$
22	20 21	eqtrdi	$⊢ (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \to dom dom ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) = X ∖ \{Z\}$
23	10 22	eqtrd	$⊢ (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \to ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) = X ∖ \{Z\}$
24	23	eleq2d	$⊢ (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \to (x \in ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) \leftrightarrow x \in (X ∖ \{Z\}))$
25	24	biimpar	$⊢ ((R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \land x \in (X ∖ \{Z\})) \to x \in ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))})$
26		eqid	$⊢ ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) = ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))})$
27		eqid	$⊢ inv ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) = inv ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))})$
28	26 27	grpoinvcl	$⊢ ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp \land x \in ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))})) \to inv ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) (x) \in ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))})$
29	28	adantll	$⊢ ((R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \land x \in ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))})) \to inv ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) (x) \in ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))})$
30		eqid	$⊢ GId ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) = GId ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))})$
31	26 30 27	grpolinv	$⊢ ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp \land x \in ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))})) \to inv ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) (x) ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) x = GId ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))})$
32	31	adantll	$⊢ ((R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \land x \in ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))})) \to inv ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) (x) ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) x = GId ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))})$
33	2	rngomndo	$⊢ R \in RingOps \to H \in MndOp$
34		mndomgmid	$⊢ H \in MndOp \to H \in (Magma \cap ExId)$
35	33 34	syl	$⊢ R \in RingOps \to H \in (Magma \cap ExId)$
36	35	adantr	$⊢ (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \to H \in (Magma \cap ExId)$
37	11 4	sseqtri	$⊢ X ∖ \{Z\} \subseteq ran G$
38	2 1	rngorn1eq	$⊢ R \in RingOps \to ran G = ran H$
39	37 38	sseqtrid	$⊢ R \in RingOps \to X ∖ \{Z\} \subseteq ran H$
40	39	adantr	$⊢ (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \to X ∖ \{Z\} \subseteq ran H$
41	1	rneqi	$⊢ ran G = ran 1^{st} (R)$
42	4 41	eqtri	$⊢ X = ran 1^{st} (R)$
43	42 2 5	rngo1cl	$⊢ R \in RingOps \to U \in X$
44	43	adantr	$⊢ (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \to U \in X$
45		eldifsn	$⊢ U \in (X ∖ \{Z\}) \leftrightarrow (U \in X \land U \neq Z)$
46	44 8 45	sylanbrc	$⊢ (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \to U \in (X ∖ \{Z\})$
47		grpomndo	$⊢ {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp \to {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in MndOp$
48		mndoismgmOLD	$⊢ {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in MndOp \to {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in Magma$
49	47 48	syl	$⊢ {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp \to {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in Magma$
50	49	adantl	$⊢ (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \to {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in Magma$
51		eqid	$⊢ ran H = ran H$
52		eqid	$⊢ {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} = {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}$
53	51 5 52	exidresid	$⊢ ((H \in (Magma \cap ExId) \land X ∖ \{Z\} \subseteq ran H \land U \in (X ∖ \{Z\})) \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in Magma) \to GId ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) = U$
54	36 40 46 50 53	syl31anc	$⊢ (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \to GId ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) = U$
55	54	adantr	$⊢ ((R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \land x \in ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))})) \to GId ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) = U$
56	32 55	eqtrd	$⊢ ((R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \land x \in ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))})) \to inv ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) (x) ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) x = U$
57		oveq1	$⊢ y = inv ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) (x) \to y ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) x = inv ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) (x) ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) x$
58	57	eqeq1d	$⊢ y = inv ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) (x) \to (y ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) x = U \leftrightarrow inv ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) (x) ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) x = U)$
59	58	rspcev	$⊢ (inv ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) (x) \in ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) \land inv ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) (x) ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) x = U) \to \exists y \in ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) y ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) x = U$
60	29 56 59	syl2anc	$⊢ ((R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \land x \in ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))})) \to \exists y \in ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) y ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) x = U$
61	25 60	syldan	$⊢ ((R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \land x \in (X ∖ \{Z\})) \to \exists y \in ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) y ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) x = U$
62	23	adantr	$⊢ ((R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \land x \in (X ∖ \{Z\})) \to ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) = X ∖ \{Z\}$
63	62	rexeqdv	$⊢ ((R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \land x \in (X ∖ \{Z\})) \to (\exists y \in ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) y ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) x = U \leftrightarrow \exists y \in (X ∖ \{Z\}) y ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) x = U)$
64		ovres	$⊢ (y \in (X ∖ \{Z\}) \land x \in (X ∖ \{Z\})) \to y ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) x = y H x$
65	64	ancoms	$⊢ (x \in (X ∖ \{Z\}) \land y \in (X ∖ \{Z\})) \to y ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) x = y H x$
66	65	eqeq1d	$⊢ (x \in (X ∖ \{Z\}) \land y \in (X ∖ \{Z\})) \to (y ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) x = U \leftrightarrow y H x = U)$
67	66	rexbidva	$⊢ x \in (X ∖ \{Z\}) \to (\exists y \in (X ∖ \{Z\}) y ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) x = U \leftrightarrow \exists y \in (X ∖ \{Z\}) y H x = U)$
68	67	adantl	$⊢ ((R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \land x \in (X ∖ \{Z\})) \to (\exists y \in (X ∖ \{Z\}) y ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) x = U \leftrightarrow \exists y \in (X ∖ \{Z\}) y H x = U)$
69	63 68	bitrd	$⊢ ((R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \land x \in (X ∖ \{Z\})) \to (\exists y \in ran ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) y ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) x = U \leftrightarrow \exists y \in (X ∖ \{Z\}) y H x = U)$
70	61 69	mpbid	$⊢ ((R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \land x \in (X ∖ \{Z\})) \to \exists y \in (X ∖ \{Z\}) y H x = U$
71	70	ralrimiva	$⊢ (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \to \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U$
72	8 71	jca	$⊢ (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \to (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U)$
73	1	fvexi	$⊢ G \in V$
74	73	rnex	$⊢ ran G \in V$
75	4 74	eqeltri	$⊢ X \in V$
76		difexg	$⊢ X \in V \to X ∖ \{Z\} \in V$
77	75 76	mp1i	$⊢ (R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U)) \to X ∖ \{Z\} \in V$
78	14	ffnd	$⊢ R \in RingOps \to H Fn (X \times X)$
79	78	adantr	$⊢ (R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U)) \to H Fn (X \times X)$
80		fnssres	$⊢ (H Fn (X \times X) \land (X ∖ \{Z\}) \times (X ∖ \{Z\}) \subseteq X \times X) \to ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) Fn ((X ∖ \{Z\}) \times (X ∖ \{Z\}))$
81	79 13 80	sylancl	$⊢ (R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U)) \to ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) Fn ((X ∖ \{Z\}) \times (X ∖ \{Z\}))$
82		ovres	$⊢ (u \in (X ∖ \{Z\}) \land v \in (X ∖ \{Z\})) \to u ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) v = u H v$
83	82	adantl	$⊢ ((R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U)) \land (u \in (X ∖ \{Z\}) \land v \in (X ∖ \{Z\}))) \to u ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) v = u H v$
84		eldifi	$⊢ u \in (X ∖ \{Z\}) \to u \in X$
85		eldifi	$⊢ v \in (X ∖ \{Z\}) \to v \in X$
86	84 85	anim12i	$⊢ (u \in (X ∖ \{Z\}) \land v \in (X ∖ \{Z\})) \to (u \in X \land v \in X)$
87	1 2 4	rngocl	$⊢ (R \in RingOps \land u \in X \land v \in X) \to u H v \in X$
88	87	3expb	$⊢ (R \in RingOps \land (u \in X \land v \in X)) \to u H v \in X$
89	86 88	sylan2	$⊢ (R \in RingOps \land (u \in (X ∖ \{Z\}) \land v \in (X ∖ \{Z\}))) \to u H v \in X$
90	89	adantlr	$⊢ ((R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U)) \land (u \in (X ∖ \{Z\}) \land v \in (X ∖ \{Z\}))) \to u H v \in X$
91		oveq2	$⊢ x = u \to y H x = y H u$
92	91	eqeq1d	$⊢ x = u \to (y H x = U \leftrightarrow y H u = U)$
93	92	rexbidv	$⊢ x = u \to (\exists y \in (X ∖ \{Z\}) y H x = U \leftrightarrow \exists y \in (X ∖ \{Z\}) y H u = U)$
94	93	rspcv	$⊢ u \in (X ∖ \{Z\}) \to (\forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U \to \exists y \in (X ∖ \{Z\}) y H u = U)$
95	94	imdistanri	$⊢ (\forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U \land u \in (X ∖ \{Z\})) \to (\exists y \in (X ∖ \{Z\}) y H u = U \land u \in (X ∖ \{Z\}))$
96		eldifsn	$⊢ v \in (X ∖ \{Z\}) \leftrightarrow (v \in X \land v \neq Z)$
97		ssrexv	$⊢ X ∖ \{Z\} \subseteq X \to (\exists y \in (X ∖ \{Z\}) y H u = U \to \exists y \in X y H u = U)$
98	11 97	ax-mp	$⊢ \exists y \in (X ∖ \{Z\}) y H u = U \to \exists y \in X y H u = U$
99	1 2 3 4 5	zerdivemp1x	$⊢ (R \in RingOps \land u \in X \land \exists y \in X y H u = U) \to (v \in X \to (u H v = Z \to v = Z))$
100	98 99	syl3an3	$⊢ (R \in RingOps \land u \in X \land \exists y \in (X ∖ \{Z\}) y H u = U) \to (v \in X \to (u H v = Z \to v = Z))$
101	84 100	syl3an2	$⊢ (R \in RingOps \land u \in (X ∖ \{Z\}) \land \exists y \in (X ∖ \{Z\}) y H u = U) \to (v \in X \to (u H v = Z \to v = Z))$
102	101	3expb	$⊢ (R \in RingOps \land (u \in (X ∖ \{Z\}) \land \exists y \in (X ∖ \{Z\}) y H u = U)) \to (v \in X \to (u H v = Z \to v = Z))$
103	102	imp	$⊢ ((R \in RingOps \land (u \in (X ∖ \{Z\}) \land \exists y \in (X ∖ \{Z\}) y H u = U)) \land v \in X) \to (u H v = Z \to v = Z)$
104	103	necon3d	$⊢ ((R \in RingOps \land (u \in (X ∖ \{Z\}) \land \exists y \in (X ∖ \{Z\}) y H u = U)) \land v \in X) \to (v \neq Z \to u H v \neq Z)$
105	104	impr	$⊢ ((R \in RingOps \land (u \in (X ∖ \{Z\}) \land \exists y \in (X ∖ \{Z\}) y H u = U)) \land (v \in X \land v \neq Z)) \to u H v \neq Z$
106	96 105	sylan2b	$⊢ ((R \in RingOps \land (u \in (X ∖ \{Z\}) \land \exists y \in (X ∖ \{Z\}) y H u = U)) \land v \in (X ∖ \{Z\})) \to u H v \neq Z$
107	106	an32s	$⊢ ((R \in RingOps \land v \in (X ∖ \{Z\})) \land (u \in (X ∖ \{Z\}) \land \exists y \in (X ∖ \{Z\}) y H u = U)) \to u H v \neq Z$
108	107	ancom2s	$⊢ ((R \in RingOps \land v \in (X ∖ \{Z\})) \land (\exists y \in (X ∖ \{Z\}) y H u = U \land u \in (X ∖ \{Z\}))) \to u H v \neq Z$
109	95 108	sylan2	$⊢ ((R \in RingOps \land v \in (X ∖ \{Z\})) \land (\forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U \land u \in (X ∖ \{Z\}))) \to u H v \neq Z$
110	109	an42s	$⊢ ((R \in RingOps \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U) \land (u \in (X ∖ \{Z\}) \land v \in (X ∖ \{Z\}))) \to u H v \neq Z$
111	110	adantlrl	$⊢ ((R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U)) \land (u \in (X ∖ \{Z\}) \land v \in (X ∖ \{Z\}))) \to u H v \neq Z$
112		eldifsn	$⊢ u H v \in (X ∖ \{Z\}) \leftrightarrow (u H v \in X \land u H v \neq Z)$
113	90 111 112	sylanbrc	$⊢ ((R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U)) \land (u \in (X ∖ \{Z\}) \land v \in (X ∖ \{Z\}))) \to u H v \in (X ∖ \{Z\})$
114	83 113	eqeltrd	$⊢ ((R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U)) \land (u \in (X ∖ \{Z\}) \land v \in (X ∖ \{Z\}))) \to u ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) v \in (X ∖ \{Z\})$
115	114	ralrimivva	$⊢ (R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U)) \to \forall u \in (X ∖ \{Z\}) \forall v \in (X ∖ \{Z\}) u ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) v \in (X ∖ \{Z\})$
116		ffnov	$⊢ ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) : (X ∖ \{Z\}) \times (X ∖ \{Z\}) ⟶ X ∖ \{Z\} \leftrightarrow (({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) Fn ((X ∖ \{Z\}) \times (X ∖ \{Z\})) \land \forall u \in (X ∖ \{Z\}) \forall v \in (X ∖ \{Z\}) u ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) v \in (X ∖ \{Z\}))$
117	81 115 116	sylanbrc	$⊢ (R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U)) \to ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) : (X ∖ \{Z\}) \times (X ∖ \{Z\}) ⟶ X ∖ \{Z\}$
118	113	3adantr3	$⊢ ((R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U)) \land (u \in (X ∖ \{Z\}) \land v \in (X ∖ \{Z\}) \land w \in (X ∖ \{Z\}))) \to u H v \in (X ∖ \{Z\})$
119		simpr3	$⊢ ((R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U)) \land (u \in (X ∖ \{Z\}) \land v \in (X ∖ \{Z\}) \land w \in (X ∖ \{Z\}))) \to w \in (X ∖ \{Z\})$
120	118 119	ovresd	$⊢ ((R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U)) \land (u \in (X ∖ \{Z\}) \land v \in (X ∖ \{Z\}) \land w \in (X ∖ \{Z\}))) \to (u H v) ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) w = (u H v) H w$
121	82	3adant3	$⊢ (u \in (X ∖ \{Z\}) \land v \in (X ∖ \{Z\}) \land w \in (X ∖ \{Z\})) \to u ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) v = u H v$
122	121	adantl	$⊢ ((R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U)) \land (u \in (X ∖ \{Z\}) \land v \in (X ∖ \{Z\}) \land w \in (X ∖ \{Z\}))) \to u ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) v = u H v$
123	122	oveq1d	$⊢ ((R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U)) \land (u \in (X ∖ \{Z\}) \land v \in (X ∖ \{Z\}) \land w \in (X ∖ \{Z\}))) \to (u ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) v) ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) w = (u H v) ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) w$
124		ovres	$⊢ (v \in (X ∖ \{Z\}) \land w \in (X ∖ \{Z\})) \to v ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) w = v H w$
125	124	3adant1	$⊢ (u \in (X ∖ \{Z\}) \land v \in (X ∖ \{Z\}) \land w \in (X ∖ \{Z\})) \to v ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) w = v H w$
126	125	adantl	$⊢ ((R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U)) \land (u \in (X ∖ \{Z\}) \land v \in (X ∖ \{Z\}) \land w \in (X ∖ \{Z\}))) \to v ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) w = v H w$
127	126	oveq2d	$⊢ ((R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U)) \land (u \in (X ∖ \{Z\}) \land v \in (X ∖ \{Z\}) \land w \in (X ∖ \{Z\}))) \to u H (v ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) w) = u H (v H w)$
128		simpr1	$⊢ ((R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U)) \land (u \in (X ∖ \{Z\}) \land v \in (X ∖ \{Z\}) \land w \in (X ∖ \{Z\}))) \to u \in (X ∖ \{Z\})$
129		fovcdm	$⊢ (({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) : (X ∖ \{Z\}) \times (X ∖ \{Z\}) ⟶ X ∖ \{Z\} \land v \in (X ∖ \{Z\}) \land w \in (X ∖ \{Z\})) \to v ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) w \in (X ∖ \{Z\})$
130	129	3adant3r1	$⊢ (({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) : (X ∖ \{Z\}) \times (X ∖ \{Z\}) ⟶ X ∖ \{Z\} \land (u \in (X ∖ \{Z\}) \land v \in (X ∖ \{Z\}) \land w \in (X ∖ \{Z\}))) \to v ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) w \in (X ∖ \{Z\})$
131	117 130	sylan	$⊢ ((R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U)) \land (u \in (X ∖ \{Z\}) \land v \in (X ∖ \{Z\}) \land w \in (X ∖ \{Z\}))) \to v ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) w \in (X ∖ \{Z\})$
132	128 131	ovresd	$⊢ ((R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U)) \land (u \in (X ∖ \{Z\}) \land v \in (X ∖ \{Z\}) \land w \in (X ∖ \{Z\}))) \to u ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) (v ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) w) = u H (v ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) w)$
133		eldifi	$⊢ w \in (X ∖ \{Z\}) \to w \in X$
134	84 85 133	3anim123i	$⊢ (u \in (X ∖ \{Z\}) \land v \in (X ∖ \{Z\}) \land w \in (X ∖ \{Z\})) \to (u \in X \land v \in X \land w \in X)$
135	1 2 4	rngoass	$⊢ (R \in RingOps \land (u \in X \land v \in X \land w \in X)) \to (u H v) H w = u H (v H w)$
136	134 135	sylan2	$⊢ (R \in RingOps \land (u \in (X ∖ \{Z\}) \land v \in (X ∖ \{Z\}) \land w \in (X ∖ \{Z\}))) \to (u H v) H w = u H (v H w)$
137	136	adantlr	$⊢ ((R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U)) \land (u \in (X ∖ \{Z\}) \land v \in (X ∖ \{Z\}) \land w \in (X ∖ \{Z\}))) \to (u H v) H w = u H (v H w)$
138	127 132 137	3eqtr4d	$⊢ ((R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U)) \land (u \in (X ∖ \{Z\}) \land v \in (X ∖ \{Z\}) \land w \in (X ∖ \{Z\}))) \to u ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) (v ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) w) = (u H v) H w$
139	120 123 138	3eqtr4d	$⊢ ((R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U)) \land (u \in (X ∖ \{Z\}) \land v \in (X ∖ \{Z\}) \land w \in (X ∖ \{Z\}))) \to (u ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) v) ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) w = u ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) (v ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) w)$
140	43	anim1i	$⊢ (R \in RingOps \land U \neq Z) \to (U \in X \land U \neq Z)$
141	140 45	sylibr	$⊢ (R \in RingOps \land U \neq Z) \to U \in (X ∖ \{Z\})$
142	141	adantrr	$⊢ (R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U)) \to U \in (X ∖ \{Z\})$
143		ovres	$⊢ (U \in (X ∖ \{Z\}) \land u \in (X ∖ \{Z\})) \to U ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) u = U H u$
144	141 143	sylan	$⊢ ((R \in RingOps \land U \neq Z) \land u \in (X ∖ \{Z\})) \to U ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) u = U H u$
145	2 42 5	rngolidm	$⊢ (R \in RingOps \land u \in X) \to U H u = u$
146	84 145	sylan2	$⊢ (R \in RingOps \land u \in (X ∖ \{Z\})) \to U H u = u$
147	146	adantlr	$⊢ ((R \in RingOps \land U \neq Z) \land u \in (X ∖ \{Z\})) \to U H u = u$
148	144 147	eqtrd	$⊢ ((R \in RingOps \land U \neq Z) \land u \in (X ∖ \{Z\})) \to U ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) u = u$
149	148	adantlrr	$⊢ ((R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U)) \land u \in (X ∖ \{Z\})) \to U ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) u = u$
150	93	rspcva	$⊢ (u \in (X ∖ \{Z\}) \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U) \to \exists y \in (X ∖ \{Z\}) y H u = U$
151		oveq1	$⊢ y = z \to y H u = z H u$
152	151	eqeq1d	$⊢ y = z \to (y H u = U \leftrightarrow z H u = U)$
153	152	cbvrexvw	$⊢ \exists y \in (X ∖ \{Z\}) y H u = U \leftrightarrow \exists z \in (X ∖ \{Z\}) z H u = U$
154		ovres	$⊢ (z \in (X ∖ \{Z\}) \land u \in (X ∖ \{Z\})) \to z ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) u = z H u$
155	154	eqeq1d	$⊢ (z \in (X ∖ \{Z\}) \land u \in (X ∖ \{Z\})) \to (z ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) u = U \leftrightarrow z H u = U)$
156	155	ancoms	$⊢ (u \in (X ∖ \{Z\}) \land z \in (X ∖ \{Z\})) \to (z ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) u = U \leftrightarrow z H u = U)$
157	156	rexbidva	$⊢ u \in (X ∖ \{Z\}) \to (\exists z \in (X ∖ \{Z\}) z ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) u = U \leftrightarrow \exists z \in (X ∖ \{Z\}) z H u = U)$
158	157	biimpar	$⊢ (u \in (X ∖ \{Z\}) \land \exists z \in (X ∖ \{Z\}) z H u = U) \to \exists z \in (X ∖ \{Z\}) z ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) u = U$
159	153 158	sylan2b	$⊢ (u \in (X ∖ \{Z\}) \land \exists y \in (X ∖ \{Z\}) y H u = U) \to \exists z \in (X ∖ \{Z\}) z ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) u = U$
160	150 159	syldan	$⊢ (u \in (X ∖ \{Z\}) \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U) \to \exists z \in (X ∖ \{Z\}) z ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) u = U$
161	160	ancoms	$⊢ (\forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U \land u \in (X ∖ \{Z\})) \to \exists z \in (X ∖ \{Z\}) z ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) u = U$
162	161	adantll	$⊢ ((R \in RingOps \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U) \land u \in (X ∖ \{Z\})) \to \exists z \in (X ∖ \{Z\}) z ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) u = U$
163	162	adantlrl	$⊢ ((R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U)) \land u \in (X ∖ \{Z\})) \to \exists z \in (X ∖ \{Z\}) z ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))}) u = U$
164	77 117 139 142 149 163	isgrpda	$⊢ (R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U)) \to {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp$
165	72 164	impbida	$⊢ R \in RingOps \to ({H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp \leftrightarrow (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U))$
166	165	pm5.32i	$⊢ (R \in RingOps \land {H ↾}_{((X ∖ \{Z\}) \times (X ∖ \{Z\}))} \in GrpOp) \leftrightarrow (R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U))$
167	6 166	bitri	$⊢ R \in DivRingOps \leftrightarrow (R \in RingOps \land (U \neq Z \land \forall x \in (X ∖ \{Z\}) \exists y \in (X ∖ \{Z\}) y H x = U))$

Metamath Proof Explorer

Theorem isdrngo2

Proof