isrngo

Description: The predicate "is a (unital) ring." Definition of "ring with unit" in Schechter p. 187. (Contributed by Jeff Hankins, 21-Nov-2006) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	isring.1	$⊢ X = ran G$
	Assertion	isrngo	$⊢ H \in A \to (⟨G, H⟩ \in RingOps \leftrightarrow ((G \in AbelOp \land H : X \times X ⟶ X) \land (\forall x \in X \forall y \in X \forall z \in X ((x H y) H z = x H (y H z) \land x H (y G z) = (x H y) G (x H z) \land (x G y) H z = (x H z) G (y H z)) \land \exists x \in X \forall y \in X (x H y = y \land y H x = y))))$

Proof

Step	Hyp	Ref	Expression
1		isring.1	$⊢ X = ran G$
2		df-br	$⊢ G RingOps H \leftrightarrow ⟨G, H⟩ \in RingOps$
3		relrngo	$⊢ Rel RingOps$
4	3	brrelex1i	$⊢ G RingOps H \to G \in V$
5	2 4	sylbir	$⊢ ⟨G, H⟩ \in RingOps \to G \in V$
6	5	a1i	$⊢ H \in A \to (⟨G, H⟩ \in RingOps \to G \in V)$
7		elex	$⊢ G \in AbelOp \to G \in V$
8	7	ad2antrr	$⊢ ((G \in AbelOp \land H : X \times X ⟶ X) \land (\forall x \in X \forall y \in X \forall z \in X ((x H y) H z = x H (y H z) \land x H (y G z) = (x H y) G (x H z) \land (x G y) H z = (x H z) G (y H z)) \land \exists x \in X \forall y \in X (x H y = y \land y H x = y))) \to G \in V$
9	8	a1i	$⊢ H \in A \to (((G \in AbelOp \land H : X \times X ⟶ X) \land (\forall x \in X \forall y \in X \forall z \in X ((x H y) H z = x H (y H z) \land x H (y G z) = (x H y) G (x H z) \land (x G y) H z = (x H z) G (y H z)) \land \exists x \in X \forall y \in X (x H y = y \land y H x = y))) \to G \in V)$
10		df-rngo	$⊢ RingOps = \{⟨g, h⟩ \| ((g \in AbelOp \land h : ran g \times ran g ⟶ ran g) \land (\forall x \in ran g \forall y \in ran g \forall z \in ran g ((x h y) h z = x h (y h z) \land x h (y g z) = (x h y) g (x h z) \land (x g y) h z = (x h z) g (y h z)) \land \exists x \in ran g \forall y \in ran g (x h y = y \land y h x = y)))\}$
11	10	eleq2i	$⊢ ⟨G, H⟩ \in RingOps \leftrightarrow ⟨G, H⟩ \in \{⟨g, h⟩ \| ((g \in AbelOp \land h : ran g \times ran g ⟶ ran g) \land (\forall x \in ran g \forall y \in ran g \forall z \in ran g ((x h y) h z = x h (y h z) \land x h (y g z) = (x h y) g (x h z) \land (x g y) h z = (x h z) g (y h z)) \land \exists x \in ran g \forall y \in ran g (x h y = y \land y h x = y)))\}$
12		simpl	$⊢ (g = G \land h = H) \to g = G$
13	12	eleq1d	$⊢ (g = G \land h = H) \to (g \in AbelOp \leftrightarrow G \in AbelOp)$
14		simpr	$⊢ (g = G \land h = H) \to h = H$
15	12	rneqd	$⊢ (g = G \land h = H) \to ran g = ran G$
16	15 1	eqtr4di	$⊢ (g = G \land h = H) \to ran g = X$
17	16	sqxpeqd	$⊢ (g = G \land h = H) \to ran g \times ran g = X \times X$
18	14 17 16	feq123d	$⊢ (g = G \land h = H) \to (h : ran g \times ran g ⟶ ran g \leftrightarrow H : X \times X ⟶ X)$
19	13 18	anbi12d	$⊢ (g = G \land h = H) \to ((g \in AbelOp \land h : ran g \times ran g ⟶ ran g) \leftrightarrow (G \in AbelOp \land H : X \times X ⟶ X))$
20	14	oveqd	$⊢ (g = G \land h = H) \to x h y = x H y$
21		eqidd	$⊢ (g = G \land h = H) \to z = z$
22	14 20 21	oveq123d	$⊢ (g = G \land h = H) \to (x h y) h z = (x H y) H z$
23		eqidd	$⊢ (g = G \land h = H) \to x = x$
24	14	oveqd	$⊢ (g = G \land h = H) \to y h z = y H z$
25	14 23 24	oveq123d	$⊢ (g = G \land h = H) \to x h (y h z) = x H (y H z)$
26	22 25	eqeq12d	$⊢ (g = G \land h = H) \to ((x h y) h z = x h (y h z) \leftrightarrow (x H y) H z = x H (y H z))$
27	12	oveqd	$⊢ (g = G \land h = H) \to y g z = y G z$
28	14 23 27	oveq123d	$⊢ (g = G \land h = H) \to x h (y g z) = x H (y G z)$
29	14	oveqd	$⊢ (g = G \land h = H) \to x h z = x H z$
30	12 20 29	oveq123d	$⊢ (g = G \land h = H) \to (x h y) g (x h z) = (x H y) G (x H z)$
31	28 30	eqeq12d	$⊢ (g = G \land h = H) \to (x h (y g z) = (x h y) g (x h z) \leftrightarrow x H (y G z) = (x H y) G (x H z))$
32	12	oveqd	$⊢ (g = G \land h = H) \to x g y = x G y$
33	14 32 21	oveq123d	$⊢ (g = G \land h = H) \to (x g y) h z = (x G y) H z$
34	12 29 24	oveq123d	$⊢ (g = G \land h = H) \to (x h z) g (y h z) = (x H z) G (y H z)$
35	33 34	eqeq12d	$⊢ (g = G \land h = H) \to ((x g y) h z = (x h z) g (y h z) \leftrightarrow (x G y) H z = (x H z) G (y H z))$
36	26 31 35	3anbi123d	$⊢ (g = G \land h = H) \to (((x h y) h z = x h (y h z) \land x h (y g z) = (x h y) g (x h z) \land (x g y) h z = (x h z) g (y h z)) \leftrightarrow ((x H y) H z = x H (y H z) \land x H (y G z) = (x H y) G (x H z) \land (x G y) H z = (x H z) G (y H z)))$
37	16 36	raleqbidv	$⊢ (g = G \land h = H) \to (\forall z \in ran g ((x h y) h z = x h (y h z) \land x h (y g z) = (x h y) g (x h z) \land (x g y) h z = (x h z) g (y h z)) \leftrightarrow \forall z \in X ((x H y) H z = x H (y H z) \land x H (y G z) = (x H y) G (x H z) \land (x G y) H z = (x H z) G (y H z)))$
38	16 37	raleqbidv	$⊢ (g = G \land h = H) \to (\forall y \in ran g \forall z \in ran g ((x h y) h z = x h (y h z) \land x h (y g z) = (x h y) g (x h z) \land (x g y) h z = (x h z) g (y h z)) \leftrightarrow \forall y \in X \forall z \in X ((x H y) H z = x H (y H z) \land x H (y G z) = (x H y) G (x H z) \land (x G y) H z = (x H z) G (y H z)))$
39	16 38	raleqbidv	$⊢ (g = G \land h = H) \to (\forall x \in ran g \forall y \in ran g \forall z \in ran g ((x h y) h z = x h (y h z) \land x h (y g z) = (x h y) g (x h z) \land (x g y) h z = (x h z) g (y h z)) \leftrightarrow \forall x \in X \forall y \in X \forall z \in X ((x H y) H z = x H (y H z) \land x H (y G z) = (x H y) G (x H z) \land (x G y) H z = (x H z) G (y H z)))$
40	20	eqeq1d	$⊢ (g = G \land h = H) \to (x h y = y \leftrightarrow x H y = y)$
41	14	oveqd	$⊢ (g = G \land h = H) \to y h x = y H x$
42	41	eqeq1d	$⊢ (g = G \land h = H) \to (y h x = y \leftrightarrow y H x = y)$
43	40 42	anbi12d	$⊢ (g = G \land h = H) \to ((x h y = y \land y h x = y) \leftrightarrow (x H y = y \land y H x = y))$
44	16 43	raleqbidv	$⊢ (g = G \land h = H) \to (\forall y \in ran g (x h y = y \land y h x = y) \leftrightarrow \forall y \in X (x H y = y \land y H x = y))$
45	16 44	rexeqbidv	$⊢ (g = G \land h = H) \to (\exists x \in ran g \forall y \in ran g (x h y = y \land y h x = y) \leftrightarrow \exists x \in X \forall y \in X (x H y = y \land y H x = y))$
46	39 45	anbi12d	$⊢ (g = G \land h = H) \to ((\forall x \in ran g \forall y \in ran g \forall z \in ran g ((x h y) h z = x h (y h z) \land x h (y g z) = (x h y) g (x h z) \land (x g y) h z = (x h z) g (y h z)) \land \exists x \in ran g \forall y \in ran g (x h y = y \land y h x = y)) \leftrightarrow (\forall x \in X \forall y \in X \forall z \in X ((x H y) H z = x H (y H z) \land x H (y G z) = (x H y) G (x H z) \land (x G y) H z = (x H z) G (y H z)) \land \exists x \in X \forall y \in X (x H y = y \land y H x = y)))$
47	19 46	anbi12d	$⊢ (g = G \land h = H) \to (((g \in AbelOp \land h : ran g \times ran g ⟶ ran g) \land (\forall x \in ran g \forall y \in ran g \forall z \in ran g ((x h y) h z = x h (y h z) \land x h (y g z) = (x h y) g (x h z) \land (x g y) h z = (x h z) g (y h z)) \land \exists x \in ran g \forall y \in ran g (x h y = y \land y h x = y))) \leftrightarrow ((G \in AbelOp \land H : X \times X ⟶ X) \land (\forall x \in X \forall y \in X \forall z \in X ((x H y) H z = x H (y H z) \land x H (y G z) = (x H y) G (x H z) \land (x G y) H z = (x H z) G (y H z)) \land \exists x \in X \forall y \in X (x H y = y \land y H x = y))))$
48	47	opelopabga	$⊢ (G \in V \land H \in A) \to (⟨G, H⟩ \in \{⟨g, h⟩ \| ((g \in AbelOp \land h : ran g \times ran g ⟶ ran g) \land (\forall x \in ran g \forall y \in ran g \forall z \in ran g ((x h y) h z = x h (y h z) \land x h (y g z) = (x h y) g (x h z) \land (x g y) h z = (x h z) g (y h z)) \land \exists x \in ran g \forall y \in ran g (x h y = y \land y h x = y)))\} \leftrightarrow ((G \in AbelOp \land H : X \times X ⟶ X) \land (\forall x \in X \forall y \in X \forall z \in X ((x H y) H z = x H (y H z) \land x H (y G z) = (x H y) G (x H z) \land (x G y) H z = (x H z) G (y H z)) \land \exists x \in X \forall y \in X (x H y = y \land y H x = y))))$
49	11 48	bitrid	$⊢ (G \in V \land H \in A) \to (⟨G, H⟩ \in RingOps \leftrightarrow ((G \in AbelOp \land H : X \times X ⟶ X) \land (\forall x \in X \forall y \in X \forall z \in X ((x H y) H z = x H (y H z) \land x H (y G z) = (x H y) G (x H z) \land (x G y) H z = (x H z) G (y H z)) \land \exists x \in X \forall y \in X (x H y = y \land y H x = y))))$
50	49	expcom	$⊢ H \in A \to (G \in V \to (⟨G, H⟩ \in RingOps \leftrightarrow ((G \in AbelOp \land H : X \times X ⟶ X) \land (\forall x \in X \forall y \in X \forall z \in X ((x H y) H z = x H (y H z) \land x H (y G z) = (x H y) G (x H z) \land (x G y) H z = (x H z) G (y H z)) \land \exists x \in X \forall y \in X (x H y = y \land y H x = y)))))$
51	6 9 50	pm5.21ndd	$⊢ H \in A \to (⟨G, H⟩ \in RingOps \leftrightarrow ((G \in AbelOp \land H : X \times X ⟶ X) \land (\forall x \in X \forall y \in X \forall z \in X ((x H y) H z = x H (y H z) \land x H (y G z) = (x H y) G (x H z) \land (x G y) H z = (x H z) G (y H z)) \land \exists x \in X \forall y \in X (x H y = y \land y H x = y))))$

Metamath Proof Explorer

Theorem isrngo

Proof