caovdig

Description: Convert an operation distributive law to class notation. (Contributed by NM, 25-Aug-1995) (Revised by Mario Carneiro, 26-Jul-2014)

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

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

Metamath Proof Explorer