isass

Description: The predicate "is an associative operation". (Contributed by FL, 1-Nov-2009) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	isass.1	$⊢ X = dom dom G$
	Assertion	isass	$⊢ G \in A \to (G \in Ass \leftrightarrow \forall x \in X \forall y \in X \forall z \in X (x G y) G z = x G (y G z))$

Proof

Step	Hyp	Ref	Expression
1		isass.1	$⊢ X = dom dom G$
2		dmeq	$⊢ g = G \to dom g = dom G$
3	2	dmeqd	$⊢ g = G \to dom dom g = dom dom G$
4	3	eleq2d	$⊢ g = G \to (x \in dom dom g \leftrightarrow x \in dom dom G)$
5	3	eleq2d	$⊢ g = G \to (y \in dom dom g \leftrightarrow y \in dom dom G)$
6	3	eleq2d	$⊢ g = G \to (z \in dom dom g \leftrightarrow z \in dom dom G)$
7	4 5 6	3anbi123d	$⊢ g = G \to ((x \in dom dom g \land y \in dom dom g \land z \in dom dom g) \leftrightarrow (x \in dom dom G \land y \in dom dom G \land z \in dom dom G))$
8		oveq	$⊢ g = G \to x g y = x G y$
9	8	oveq1d	$⊢ g = G \to (x g y) g z = (x G y) g z$
10		oveq	$⊢ g = G \to (x G y) g z = (x G y) G z$
11	9 10	eqtrd	$⊢ g = G \to (x g y) g z = (x G y) G z$
12		oveq	$⊢ g = G \to y g z = y G z$
13	12	oveq2d	$⊢ g = G \to x g (y g z) = x g (y G z)$
14		oveq	$⊢ g = G \to x g (y G z) = x G (y G z)$
15	13 14	eqtrd	$⊢ g = G \to x g (y g z) = x G (y G z)$
16	11 15	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))$
17	7 16	imbi12d	$⊢ g = G \to (((x \in dom dom g \land y \in dom dom g \land z \in dom dom g) \to (x g y) g z = x g (y g z)) \leftrightarrow ((x \in dom dom G \land y \in dom dom G \land z \in dom dom G) \to (x G y) G z = x G (y G z)))$
18	17	albidv	$⊢ g = G \to (\forall z ((x \in dom dom g \land y \in dom dom g \land z \in dom dom g) \to (x g y) g z = x g (y g z)) \leftrightarrow \forall z ((x \in dom dom G \land y \in dom dom G \land z \in dom dom G) \to (x G y) G z = x G (y G z)))$
19	18	2albidv	$⊢ g = G \to (\forall x \forall y \forall z ((x \in dom dom g \land y \in dom dom g \land z \in dom dom g) \to (x g y) g z = x g (y g z)) \leftrightarrow \forall x \forall y \forall z ((x \in dom dom G \land y \in dom dom G \land z \in dom dom G) \to (x G y) G z = x G (y G z)))$
20		r3al	$⊢ \forall x \in dom dom g \forall y \in dom dom g \forall z \in dom dom g (x g y) g z = x g (y g z) \leftrightarrow \forall x \forall y \forall z ((x \in dom dom g \land y \in dom dom g \land z \in dom dom g) \to (x g y) g z = x g (y g z))$
21		r3al	$⊢ \forall x \in dom dom G \forall y \in dom dom G \forall z \in dom dom G (x G y) G z = x G (y G z) \leftrightarrow \forall x \forall y \forall z ((x \in dom dom G \land y \in dom dom G \land z \in dom dom G) \to (x G y) G z = x G (y G z))$
22	19 20 21	3bitr4g	$⊢ g = G \to (\forall x \in dom dom g \forall y \in dom dom g \forall z \in dom dom g (x g y) g z = x g (y g z) \leftrightarrow \forall x \in dom dom G \forall y \in dom dom G \forall z \in dom dom G (x G y) G z = x G (y G z))$
23	1	eqcomi	$⊢ dom dom G = X$
24	23	a1i	$⊢ g = G \to dom dom G = X$
25	24	raleqdv	$⊢ g = G \to (\forall y \in dom dom G \forall z \in dom dom G (x G y) G z = x G (y G z) \leftrightarrow \forall y \in X \forall z \in dom dom G (x G y) G z = x G (y G z))$
26	24 25	raleqbidv	$⊢ g = G \to (\forall x \in dom dom G \forall y \in dom dom G \forall z \in dom dom G (x G y) G z = x G (y G z) \leftrightarrow \forall x \in X \forall y \in X \forall z \in dom dom G (x G y) G z = x G (y G z))$
27	24	raleqdv	$⊢ g = G \to (\forall z \in dom dom 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))$
28	27	2ralbidv	$⊢ g = G \to (\forall x \in X \forall y \in X \forall z \in dom dom 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))$
29	22 26 28	3bitrd	$⊢ g = G \to (\forall x \in dom dom g \forall y \in dom dom g \forall z \in dom dom 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))$
30		df-ass	$⊢ Ass = \{g \| \forall x \in dom dom g \forall y \in dom dom g \forall z \in dom dom g (x g y) g z = x g (y g z)\}$
31	29 30	elab2g	$⊢ G \in A \to (G \in Ass \leftrightarrow \forall x \in X \forall y \in X \forall z \in X (x G y) G z = x G (y G z))$

Metamath Proof Explorer

Theorem isass

Proof