Theorem caovdir2d

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

	Ref	Expression
Hypotheses	caovdir2d.1	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\wedge z\in S\right)\right)\to xG\left(yFz\right)=\left(xGy\right)F\left(xGz\right)$$
	caovdir2d.2	$$⊢\phi \to A\in S$$
	caovdir2d.3	$$⊢\phi \to B\in S$$
	caovdir2d.4	$$⊢\phi \to C\in S$$
	caovdir2d.cl	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\right)\right)\to xFy\in S$$
	caovdir2d.com	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\right)\right)\to xGy=yGx$$
Assertion	caovdir2d	$$⊢\phi \to \left(AFB\right)GC=\left(AGC\right)F\left(BGC\right)$$

Proof

Step	Hyp	Ref	Expression
1		caovdir2d.1	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\wedge z\in S\right)\right)\to xG\left(yFz\right)=\left(xGy\right)F\left(xGz\right)$$
2		caovdir2d.2	$$⊢\phi \to A\in S$$
3		caovdir2d.3	$$⊢\phi \to B\in S$$
4		caovdir2d.4	$$⊢\phi \to C\in S$$
5		caovdir2d.cl	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\right)\right)\to xFy\in S$$
6		caovdir2d.com	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\right)\right)\to xGy=yGx$$
7	1 4 2 3	caovdid	$$⊢\phi \to CG\left(AFB\right)=\left(CGA\right)F\left(CGB\right)$$
8	5 2 3	caovcld	$$⊢\phi \to AFB\in S$$
9	6 8 4	caovcomd	$$⊢\phi \to \left(AFB\right)GC=CG\left(AFB\right)$$
10	6 2 4	caovcomd	$$⊢\phi \to AGC=CGA$$
11	6 3 4	caovcomd	$$⊢\phi \to BGC=CGB$$
12	10 11	oveq12d	$$⊢\phi \to \left(AGC\right)F\left(BGC\right)=\left(CGA\right)F\left(CGB\right)$$
13	7 9 12	3eqtr4d	$$⊢\phi \to \left(AFB\right)GC=\left(AGC\right)F\left(BGC\right)$$