caovdir2d

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

	Ref	Expression
Hypotheses	caovdir2d.1	$⊢ (φ \land (x \in S \land y \in S \land z \in S)) \to x G (y F z) = (x G y) F (x G z)$
	caovdir2d.2	$⊢ φ \to A \in S$
	caovdir2d.3	$⊢ φ \to B \in S$
	caovdir2d.4	$⊢ φ \to C \in S$
	caovdir2d.cl	$⊢ (φ \land (x \in S \land y \in S)) \to x F y \in S$
	caovdir2d.com	$⊢ (φ \land (x \in S \land y \in S)) \to x G y = y G x$
Assertion	caovdir2d	$⊢ φ \to (A F B) G C = (A G C) F (B G C)$

Step	Hyp	Ref	Expression
1		caovdir2d.1	$⊢ (φ \land (x \in S \land y \in S \land z \in S)) \to x G (y F z) = (x G y) F (x G z)$
2		caovdir2d.2	$⊢ φ \to A \in S$
3		caovdir2d.3	$⊢ φ \to B \in S$
4		caovdir2d.4	$⊢ φ \to C \in S$
5		caovdir2d.cl	$⊢ (φ \land (x \in S \land y \in S)) \to x F y \in S$
6		caovdir2d.com	$⊢ (φ \land (x \in S \land y \in S)) \to x G y = y G x$
7	1 4 2 3	caovdid	$⊢ φ \to C G (A F B) = (C G A) F (C G B)$
8	5 2 3	caovcld	$⊢ φ \to A F B \in S$
9	6 8 4	caovcomd	$⊢ φ \to (A F B) G C = C G (A F B)$
10	6 2 4	caovcomd	$⊢ φ \to A G C = C G A$
11	6 3 4	caovcomd	$⊢ φ \to B G C = C G B$
12	10 11	oveq12d	$⊢ φ \to (A G C) F (B G C) = (C G A) F (C G B)$
13	7 9 12	3eqtr4d	$⊢ φ \to (A F B) G C = (A G C) F (B G C)$

Metamath Proof Explorer