caovdirg

Description: Convert an operation reverse distributive law to class notation. (Contributed by Mario Carneiro, 19-Oct-2014)

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

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

Metamath Proof Explorer