isgrpda

Description: Properties that determine a group operation. (Contributed by Jeff Madsen, 1-Dec-2009) (New usage is discouraged.)

	Ref	Expression
Hypotheses	isgrpda.1	$⊢ φ \to X \in V$
	isgrpda.2	$⊢ φ \to G : X \times X ⟶ X$
	isgrpda.3	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to (x G y) G z = x G (y G z)$
	isgrpda.4	$⊢ φ \to U \in X$
	isgrpda.5	$⊢ (φ \land x \in X) \to U G x = x$
	isgrpda.6	$⊢ (φ \land x \in X) \to \exists n \in X n G x = U$
Assertion	isgrpda	$⊢ φ \to G \in GrpOp$

Proof

Step	Hyp	Ref	Expression
1		isgrpda.1	$⊢ φ \to X \in V$
2		isgrpda.2	$⊢ φ \to G : X \times X ⟶ X$
3		isgrpda.3	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to (x G y) G z = x G (y G z)$
4		isgrpda.4	$⊢ φ \to U \in X$
5		isgrpda.5	$⊢ (φ \land x \in X) \to U G x = x$
6		isgrpda.6	$⊢ (φ \land x \in X) \to \exists n \in X n G x = U$
7	3	ralrimivvva	$⊢ φ \to \forall x \in X \forall y \in X \forall z \in X (x G y) G z = x G (y G z)$
8		oveq1	$⊢ y = n \to y G x = n G x$
9	8	eqeq1d	$⊢ y = n \to (y G x = U \leftrightarrow n G x = U)$
10	9	cbvrexvw	$⊢ \exists y \in X y G x = U \leftrightarrow \exists n \in X n G x = U$
11	6 10	sylibr	$⊢ (φ \land x \in X) \to \exists y \in X y G x = U$
12	5 11	jca	$⊢ (φ \land x \in X) \to (U G x = x \land \exists y \in X y G x = U)$
13	12	ralrimiva	$⊢ φ \to \forall x \in X (U G x = x \land \exists y \in X y G x = U)$
14		oveq1	$⊢ u = U \to u G x = U G x$
15	14	eqeq1d	$⊢ u = U \to (u G x = x \leftrightarrow U G x = x)$
16		eqeq2	$⊢ u = U \to (y G x = u \leftrightarrow y G x = U)$
17	16	rexbidv	$⊢ u = U \to (\exists y \in X y G x = u \leftrightarrow \exists y \in X y G x = U)$
18	15 17	anbi12d	$⊢ u = U \to ((u G x = x \land \exists y \in X y G x = u) \leftrightarrow (U G x = x \land \exists y \in X y G x = U))$
19	18	ralbidv	$⊢ u = U \to (\forall x \in X (u G x = x \land \exists y \in X y G x = u) \leftrightarrow \forall x \in X (U G x = x \land \exists y \in X y G x = U))$
20	19	rspcev	$⊢ (U \in X \land \forall x \in X (U G x = x \land \exists y \in X y G x = U)) \to \exists u \in X \forall x \in X (u G x = x \land \exists y \in X y G x = u)$
21	4 13 20	syl2anc	$⊢ φ \to \exists u \in X \forall x \in X (u G x = x \land \exists y \in X y G x = u)$
22	4	adantr	$⊢ (φ \land x \in X) \to U \in X$
23		simpr	$⊢ (φ \land x \in X) \to x \in X$
24	5	eqcomd	$⊢ (φ \land x \in X) \to x = U G x$
25		rspceov	$⊢ (U \in X \land x \in X \land x = U G x) \to \exists y \in X \exists z \in X x = y G z$
26	22 23 24 25	syl3anc	$⊢ (φ \land x \in X) \to \exists y \in X \exists z \in X x = y G z$
27	26	ralrimiva	$⊢ φ \to \forall x \in X \exists y \in X \exists z \in X x = y G z$
28		foov	$⊢ G : X \times X \underset{onto}{⟶} X \leftrightarrow (G : X \times X ⟶ X \land \forall x \in X \exists y \in X \exists z \in X x = y G z)$
29	2 27 28	sylanbrc	$⊢ φ \to G : X \times X \underset{onto}{⟶} X$
30		forn	$⊢ G : X \times X \underset{onto}{⟶} X \to ran G = X$
31	29 30	syl	$⊢ φ \to ran G = X$
32	31	sqxpeqd	$⊢ φ \to ran G \times ran G = X \times X$
33	32 31	feq23d	$⊢ φ \to (G : ran G \times ran G ⟶ ran G \leftrightarrow G : X \times X ⟶ X)$
34	31	raleqdv	$⊢ φ \to (\forall z \in ran G (x G y) G z = x G (y G z) \leftrightarrow \forall z \in X (x G y) G z = x G (y G z))$
35	31 34	raleqbidv	$⊢ φ \to (\forall y \in ran G \forall z \in ran G (x G y) G z = x G (y G z) \leftrightarrow \forall y \in X \forall z \in X (x G y) G z = x G (y G z))$
36	31 35	raleqbidv	$⊢ φ \to (\forall x \in ran G \forall y \in ran G \forall z \in ran G (x G y) G z = x G (y G z) \leftrightarrow \forall x \in X \forall y \in X \forall z \in X (x G y) G z = x G (y G z))$
37	31	rexeqdv	$⊢ φ \to (\exists y \in ran G y G x = u \leftrightarrow \exists y \in X y G x = u)$
38	37	anbi2d	$⊢ φ \to ((u G x = x \land \exists y \in ran G y G x = u) \leftrightarrow (u G x = x \land \exists y \in X y G x = u))$
39	31 38	raleqbidv	$⊢ φ \to (\forall x \in ran G (u G x = x \land \exists y \in ran G y G x = u) \leftrightarrow \forall x \in X (u G x = x \land \exists y \in X y G x = u))$
40	31 39	rexeqbidv	$⊢ φ \to (\exists u \in ran G \forall x \in ran G (u G x = x \land \exists y \in ran G y G x = u) \leftrightarrow \exists u \in X \forall x \in X (u G x = x \land \exists y \in X y G x = u))$
41	33 36 40	3anbi123d	$⊢ φ \to ((G : ran G \times ran G ⟶ ran G \land \forall x \in ran G \forall y \in ran G \forall z \in ran G (x G y) G z = x G (y G z) \land \exists u \in ran G \forall x \in ran G (u G x = x \land \exists y \in ran G y G x = u)) \leftrightarrow (G : X \times X ⟶ X \land \forall x \in X \forall y \in X \forall z \in X (x G y) G z = x G (y G z) \land \exists u \in X \forall x \in X (u G x = x \land \exists y \in X y G x = u)))$
42	2 7 21 41	mpbir3and	$⊢ φ \to (G : ran G \times ran G ⟶ ran G \land \forall x \in ran G \forall y \in ran G \forall z \in ran G (x G y) G z = x G (y G z) \land \exists u \in ran G \forall x \in ran G (u G x = x \land \exists y \in ran G y G x = u))$
43	1 1	xpexd	$⊢ φ \to X \times X \in V$
44	2 43	fexd	$⊢ φ \to G \in V$
45		eqid	$⊢ ran G = ran G$
46	45	isgrpo	$⊢ G \in V \to (G \in GrpOp \leftrightarrow (G : ran G \times ran G ⟶ ran G \land \forall x \in ran G \forall y \in ran G \forall z \in ran G (x G y) G z = x G (y G z) \land \exists u \in ran G \forall x \in ran G (u G x = x \land \exists y \in ran G y G x = u)))$
47	44 46	syl	$⊢ φ \to (G \in GrpOp \leftrightarrow (G : ran G \times ran G ⟶ ran G \land \forall x \in ran G \forall y \in ran G \forall z \in ran G (x G y) G z = x G (y G z) \land \exists u \in ran G \forall x \in ran G (u G x = x \land \exists y \in ran G y G x = u)))$
48	42 47	mpbird	$⊢ φ \to G \in GrpOp$

Metamath Proof Explorer

Theorem isgrpda

Proof