isrngod

Description: Conditions that determine a ring. (Changed label from isringd to isrngod -NM 2-Aug-2013.) (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	isringod.1	$⊢ φ \to G \in AbelOp$
	isringod.2	$⊢ φ \to X = ran G$
	isringod.3	$⊢ φ \to H : X \times X ⟶ X$
	isringod.4	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to (x H y) H z = x H (y H z)$
	isringod.5	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to x H (y G z) = (x H y) G (x H z)$
	isringod.6	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to (x G y) H z = (x H z) G (y H z)$
	isringod.7	$⊢ φ \to U \in X$
	isringod.8	$⊢ (φ \land y \in X) \to U H y = y$
	isringod.9	$⊢ (φ \land y \in X) \to y H U = y$
Assertion	isrngod	$⊢ φ \to ⟨G, H⟩ \in RingOps$

Proof

Step	Hyp	Ref	Expression
1		isringod.1	$⊢ φ \to G \in AbelOp$
2		isringod.2	$⊢ φ \to X = ran G$
3		isringod.3	$⊢ φ \to H : X \times X ⟶ X$
4		isringod.4	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to (x H y) H z = x H (y H z)$
5		isringod.5	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to x H (y G z) = (x H y) G (x H z)$
6		isringod.6	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to (x G y) H z = (x H z) G (y H z)$
7		isringod.7	$⊢ φ \to U \in X$
8		isringod.8	$⊢ (φ \land y \in X) \to U H y = y$
9		isringod.9	$⊢ (φ \land y \in X) \to y H U = y$
10	2	sqxpeqd	$⊢ φ \to X \times X = ran G \times ran G$
11	10 2	feq23d	$⊢ φ \to (H : X \times X ⟶ X \leftrightarrow H : ran G \times ran G ⟶ ran G)$
12	3 11	mpbid	$⊢ φ \to H : ran G \times ran G ⟶ ran G$
13	4 5 6	3jca	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \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))$
14	13	ralrimivvva	$⊢ φ \to \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))$
15	2	raleqdv	$⊢ φ \to (\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)) \leftrightarrow \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)))$
16	2 15	raleqbidv	$⊢ φ \to (\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)) \leftrightarrow \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)))$
17	2 16	raleqbidv	$⊢ φ \to (\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)) \leftrightarrow \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)))$
18	14 17	mpbid	$⊢ φ \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))$
19	8 9	jca	$⊢ (φ \land y \in X) \to (U H y = y \land y H U = y)$
20	19	ralrimiva	$⊢ φ \to \forall y \in X (U H y = y \land y H U = y)$
21		oveq1	$⊢ x = U \to x H y = U H y$
22	21	eqeq1d	$⊢ x = U \to (x H y = y \leftrightarrow U H y = y)$
23	22	ovanraleqv	$⊢ x = U \to (\forall y \in X (x H y = y \land y H x = y) \leftrightarrow \forall y \in X (U H y = y \land y H U = y))$
24	23	rspcev	$⊢ (U \in X \land \forall y \in X (U H y = y \land y H U = y)) \to \exists x \in X \forall y \in X (x H y = y \land y H x = y)$
25	7 20 24	syl2anc	$⊢ φ \to \exists x \in X \forall y \in X (x H y = y \land y H x = y)$
26	2	raleqdv	$⊢ φ \to (\forall y \in X (x H y = y \land y H x = y) \leftrightarrow \forall y \in ran G (x H y = y \land y H x = y))$
27	2 26	rexeqbidv	$⊢ φ \to (\exists x \in X \forall y \in X (x H y = y \land y H x = y) \leftrightarrow \exists x \in ran G \forall y \in ran G (x H y = y \land y H x = y))$
28	25 27	mpbid	$⊢ φ \to \exists x \in ran G \forall y \in ran G (x H y = y \land y H x = y)$
29	18 28	jca	$⊢ φ \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))$
30	1 12 29	jca31	$⊢ φ \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)))$
31		rnexg	$⊢ G \in AbelOp \to ran G \in V$
32	1 31	syl	$⊢ φ \to ran G \in V$
33	32 32	xpexd	$⊢ φ \to ran G \times ran G \in V$
34		fex	$⊢ (H : ran G \times ran G ⟶ ran G \land ran G \times ran G \in V) \to H \in V$
35	12 33 34	syl2anc	$⊢ φ \to H \in V$
36		eqid	$⊢ ran G = ran G$
37	36	isrngo	$⊢ H \in V \to (⟨G, H⟩ \in RingOps \leftrightarrow ((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))))$
38	35 37	syl	$⊢ φ \to (⟨G, H⟩ \in RingOps \leftrightarrow ((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))))$
39	30 38	mpbird	$⊢ φ \to ⟨G, H⟩ \in RingOps$

Metamath Proof Explorer

Theorem isrngod

Proof