isgrpo

Description: The predicate "is a group operation." Note that X is the base set of the group. (Contributed by NM, 10-Oct-2006) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	isgrp.1	$⊢ X = ran G$
	Assertion	isgrpo	$⊢ G \in A \to (G \in GrpOp \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)))$

Proof

Step	Hyp	Ref	Expression
1		isgrp.1	$⊢ X = ran G$
2		feq1	$⊢ g = G \to (g : t \times t ⟶ t \leftrightarrow G : t \times t ⟶ t)$
3		oveq	$⊢ g = G \to (x g y) g z = (x g y) G z$
4		oveq	$⊢ g = G \to x g y = x G y$
5	4	oveq1d	$⊢ g = G \to (x g y) G z = (x G y) G z$
6	3 5	eqtrd	$⊢ g = G \to (x g y) g z = (x G y) G z$
7		oveq	$⊢ g = G \to x g (y g z) = x G (y g z)$
8		oveq	$⊢ g = G \to y g z = y G z$
9	8	oveq2d	$⊢ g = G \to x G (y g z) = x G (y G z)$
10	7 9	eqtrd	$⊢ g = G \to x g (y g z) = x G (y G z)$
11	6 10	eqeq12d	$⊢ g = G \to ((x g y) g z = x g (y g z) \leftrightarrow (x G y) G z = x G (y G z))$
12	11	ralbidv	$⊢ g = G \to (\forall z \in t (x g y) g z = x g (y g z) \leftrightarrow \forall z \in t (x G y) G z = x G (y G z))$
13	12	2ralbidv	$⊢ g = G \to (\forall x \in t \forall y \in t \forall z \in t (x g y) g z = x g (y g z) \leftrightarrow \forall x \in t \forall y \in t \forall z \in t (x G y) G z = x G (y G z))$
14		oveq	$⊢ g = G \to u g x = u G x$
15	14	eqeq1d	$⊢ g = G \to (u g x = x \leftrightarrow u G x = x)$
16		oveq	$⊢ g = G \to y g x = y G x$
17	16	eqeq1d	$⊢ g = G \to (y g x = u \leftrightarrow y G x = u)$
18	17	rexbidv	$⊢ g = G \to (\exists y \in t y g x = u \leftrightarrow \exists y \in t y G x = u)$
19	15 18	anbi12d	$⊢ g = G \to ((u g x = x \land \exists y \in t y g x = u) \leftrightarrow (u G x = x \land \exists y \in t y G x = u))$
20	19	rexralbidv	$⊢ g = G \to (\exists u \in t \forall x \in t (u g x = x \land \exists y \in t y g x = u) \leftrightarrow \exists u \in t \forall x \in t (u G x = x \land \exists y \in t y G x = u))$
21	2 13 20	3anbi123d	$⊢ g = G \to ((g : t \times t ⟶ t \land \forall x \in t \forall y \in t \forall z \in t (x g y) g z = x g (y g z) \land \exists u \in t \forall x \in t (u g x = x \land \exists y \in t y g x = u)) \leftrightarrow (G : t \times t ⟶ t \land \forall x \in t \forall y \in t \forall z \in t (x G y) G z = x G (y G z) \land \exists u \in t \forall x \in t (u G x = x \land \exists y \in t y G x = u)))$
22	21	exbidv	$⊢ g = G \to (\exists t (g : t \times t ⟶ t \land \forall x \in t \forall y \in t \forall z \in t (x g y) g z = x g (y g z) \land \exists u \in t \forall x \in t (u g x = x \land \exists y \in t y g x = u)) \leftrightarrow \exists t (G : t \times t ⟶ t \land \forall x \in t \forall y \in t \forall z \in t (x G y) G z = x G (y G z) \land \exists u \in t \forall x \in t (u G x = x \land \exists y \in t y G x = u)))$
23		df-grpo	$⊢ GrpOp = \{g \| \exists t (g : t \times t ⟶ t \land \forall x \in t \forall y \in t \forall z \in t (x g y) g z = x g (y g z) \land \exists u \in t \forall x \in t (u g x = x \land \exists y \in t y g x = u))\}$
24	22 23	elab2g	$⊢ G \in A \to (G \in GrpOp \leftrightarrow \exists t (G : t \times t ⟶ t \land \forall x \in t \forall y \in t \forall z \in t (x G y) G z = x G (y G z) \land \exists u \in t \forall x \in t (u G x = x \land \exists y \in t y G x = u)))$
25		simpl	$⊢ (u G x = x \land \exists y \in t y G x = u) \to u G x = x$
26	25	ralimi	$⊢ \forall x \in t (u G x = x \land \exists y \in t y G x = u) \to \forall x \in t u G x = x$
27		oveq2	$⊢ x = z \to u G x = u G z$
28		id	$⊢ x = z \to x = z$
29	27 28	eqeq12d	$⊢ x = z \to (u G x = x \leftrightarrow u G z = z)$
30		eqcom	$⊢ u G z = z \leftrightarrow z = u G z$
31	29 30	syl6bb	$⊢ x = z \to (u G x = x \leftrightarrow z = u G z)$
32	31	rspcv	$⊢ z \in t \to (\forall x \in t u G x = x \to z = u G z)$
33		oveq2	$⊢ y = z \to u G y = u G z$
34	33	rspceeqv	$⊢ (z \in t \land z = u G z) \to \exists y \in t z = u G y$
35	34	ex	$⊢ z \in t \to (z = u G z \to \exists y \in t z = u G y)$
36	32 35	syld	$⊢ z \in t \to (\forall x \in t u G x = x \to \exists y \in t z = u G y)$
37	26 36	syl5	$⊢ z \in t \to (\forall x \in t (u G x = x \land \exists y \in t y G x = u) \to \exists y \in t z = u G y)$
38	37	reximdv	$⊢ z \in t \to (\exists u \in t \forall x \in t (u G x = x \land \exists y \in t y G x = u) \to \exists u \in t \exists y \in t z = u G y)$
39	38	impcom	$⊢ (\exists u \in t \forall x \in t (u G x = x \land \exists y \in t y G x = u) \land z \in t) \to \exists u \in t \exists y \in t z = u G y$
40	39	ralrimiva	$⊢ \exists u \in t \forall x \in t (u G x = x \land \exists y \in t y G x = u) \to \forall z \in t \exists u \in t \exists y \in t z = u G y$
41	40	anim2i	$⊢ (G : t \times t ⟶ t \land \exists u \in t \forall x \in t (u G x = x \land \exists y \in t y G x = u)) \to (G : t \times t ⟶ t \land \forall z \in t \exists u \in t \exists y \in t z = u G y)$
42		foov	$⊢ G : t \times t \underset{onto}{⟶} t \leftrightarrow (G : t \times t ⟶ t \land \forall z \in t \exists u \in t \exists y \in t z = u G y)$
43	41 42	sylibr	$⊢ (G : t \times t ⟶ t \land \exists u \in t \forall x \in t (u G x = x \land \exists y \in t y G x = u)) \to G : t \times t \underset{onto}{⟶} t$
44		forn	$⊢ G : t \times t \underset{onto}{⟶} t \to ran G = t$
45	44	eqcomd	$⊢ G : t \times t \underset{onto}{⟶} t \to t = ran G$
46	43 45	syl	$⊢ (G : t \times t ⟶ t \land \exists u \in t \forall x \in t (u G x = x \land \exists y \in t y G x = u)) \to t = ran G$
47	46	3adant2	$⊢ (G : t \times t ⟶ t \land \forall x \in t \forall y \in t \forall z \in t (x G y) G z = x G (y G z) \land \exists u \in t \forall x \in t (u G x = x \land \exists y \in t y G x = u)) \to t = ran G$
48	47	pm4.71ri	$⊢ (G : t \times t ⟶ t \land \forall x \in t \forall y \in t \forall z \in t (x G y) G z = x G (y G z) \land \exists u \in t \forall x \in t (u G x = x \land \exists y \in t y G x = u)) \leftrightarrow (t = ran G \land (G : t \times t ⟶ t \land \forall x \in t \forall y \in t \forall z \in t (x G y) G z = x G (y G z) \land \exists u \in t \forall x \in t (u G x = x \land \exists y \in t y G x = u)))$
49	48	exbii	$⊢ \exists t (G : t \times t ⟶ t \land \forall x \in t \forall y \in t \forall z \in t (x G y) G z = x G (y G z) \land \exists u \in t \forall x \in t (u G x = x \land \exists y \in t y G x = u)) \leftrightarrow \exists t (t = ran G \land (G : t \times t ⟶ t \land \forall x \in t \forall y \in t \forall z \in t (x G y) G z = x G (y G z) \land \exists u \in t \forall x \in t (u G x = x \land \exists y \in t y G x = u)))$
50	24 49	syl6bb	$⊢ G \in A \to (G \in GrpOp \leftrightarrow \exists t (t = ran G \land (G : t \times t ⟶ t \land \forall x \in t \forall y \in t \forall z \in t (x G y) G z = x G (y G z) \land \exists u \in t \forall x \in t (u G x = x \land \exists y \in t y G x = u))))$
51		rnexg	$⊢ G \in A \to ran G \in V$
52	1	eqeq2i	$⊢ t = X \leftrightarrow t = ran G$
53		xpeq1	$⊢ t = X \to t \times t = X \times t$
54		xpeq2	$⊢ t = X \to X \times t = X \times X$
55	53 54	eqtrd	$⊢ t = X \to t \times t = X \times X$
56	55	feq2d	$⊢ t = X \to (G : t \times t ⟶ t \leftrightarrow G : X \times X ⟶ t)$
57		feq3	$⊢ t = X \to (G : X \times X ⟶ t \leftrightarrow G : X \times X ⟶ X)$
58	56 57	bitrd	$⊢ t = X \to (G : t \times t ⟶ t \leftrightarrow G : X \times X ⟶ X)$
59		raleq	$⊢ t = X \to (\forall z \in t (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))$
60	59	raleqbi1dv	$⊢ t = X \to (\forall y \in t \forall z \in t (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))$
61	60	raleqbi1dv	$⊢ t = X \to (\forall x \in t \forall y \in t \forall z \in t (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))$
62		rexeq	$⊢ t = X \to (\exists y \in t y G x = u \leftrightarrow \exists y \in X y G x = u)$
63	62	anbi2d	$⊢ t = X \to ((u G x = x \land \exists y \in t y G x = u) \leftrightarrow (u G x = x \land \exists y \in X y G x = u))$
64	63	raleqbi1dv	$⊢ t = X \to (\forall x \in t (u G x = x \land \exists y \in t y G x = u) \leftrightarrow \forall x \in X (u G x = x \land \exists y \in X y G x = u))$
65	64	rexeqbi1dv	$⊢ t = X \to (\exists u \in t \forall x \in t (u G x = x \land \exists y \in t 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))$
66	58 61 65	3anbi123d	$⊢ t = X \to ((G : t \times t ⟶ t \land \forall x \in t \forall y \in t \forall z \in t (x G y) G z = x G (y G z) \land \exists u \in t \forall x \in t (u G x = x \land \exists y \in t 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)))$
67	52 66	sylbir	$⊢ t = ran G \to ((G : t \times t ⟶ t \land \forall x \in t \forall y \in t \forall z \in t (x G y) G z = x G (y G z) \land \exists u \in t \forall x \in t (u G x = x \land \exists y \in t 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)))$
68	67	ceqsexgv	$⊢ ran G \in V \to (\exists t (t = ran G \land (G : t \times t ⟶ t \land \forall x \in t \forall y \in t \forall z \in t (x G y) G z = x G (y G z) \land \exists u \in t \forall x \in t (u G x = x \land \exists y \in t 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)))$
69	51 68	syl	$⊢ G \in A \to (\exists t (t = ran G \land (G : t \times t ⟶ t \land \forall x \in t \forall y \in t \forall z \in t (x G y) G z = x G (y G z) \land \exists u \in t \forall x \in t (u G x = x \land \exists y \in t 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)))$
70	50 69	bitrd	$⊢ G \in A \to (G \in GrpOp \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)))$

Metamath Proof Explorer

Theorem isgrpo

Proof