Metamath Proof Explorer

Theorem caovassg

Description: Convert an operation associative law to class notation. (Contributed by Mario Carneiro, 1-Jun-2013) (Revised by Mario Carneiro, 26-May-2014)

		Ref	Expression
	Hypothesis	caovassg.1	$⊢ (φ \land (x \in S \land y \in S \land z \in S)) \to (x F y) F z = x F (y F z)$
	Assertion	caovassg	$⊢ (φ \land (A \in S \land B \in S \land C \in S)) \to (A F B) F C = A F (B F C)$

Proof

Step	Hyp	Ref	Expression
1		caovassg.1	$⊢ (φ \land (x \in S \land y \in S \land z \in S)) \to (x F y) F z = x F (y F z)$
2	1	ralrimivvva	$⊢ φ \to \forall x \in S \forall y \in S \forall z \in S (x F y) F z = x F (y F z)$
3		oveq1	$⊢ x = A \to x F y = A F y$
4	3	oveq1d	$⊢ x = A \to (x F y) F z = (A F y) F z$
5		oveq1	$⊢ x = A \to x F (y F z) = A F (y F z)$
6	4 5	eqeq12d	$⊢ x = A \to ((x F y) F z = x F (y F z) \leftrightarrow (A F y) F z = A F (y F z))$
7		oveq2	$⊢ y = B \to A F y = A F B$
8	7	oveq1d	$⊢ y = B \to (A F y) F z = (A F B) F z$
9		oveq1	$⊢ y = B \to y F z = B F z$
10	9	oveq2d	$⊢ y = B \to A F (y F z) = A F (B F z)$
11	8 10	eqeq12d	$⊢ y = B \to ((A F y) F z = A F (y F z) \leftrightarrow (A F B) F z = A F (B F z))$
12		oveq2	$⊢ z = C \to (A F B) F z = (A F B) F C$
13		oveq2	$⊢ z = C \to B F z = B F C$
14	13	oveq2d	$⊢ z = C \to A F (B F z) = A F (B F C)$
15	12 14	eqeq12d	$⊢ z = C \to ((A F B) F z = A F (B F z) \leftrightarrow (A F B) F C = A F (B F C))$
16	6 11 15	rspc3v	$⊢ (A \in S \land B \in S \land C \in S) \to (\forall x \in S \forall y \in S \forall z \in S (x F y) F z = x F (y F z) \to (A F B) F C = A F (B F C))$
17	2 16	mpan9	$⊢ (φ \land (A \in S \land B \in S \land C \in S)) \to (A F B) F C = A F (B F C)$