Metamath Proof Explorer

Theorem caovdird

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

	Ref	Expression
Hypotheses	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)$
	caovdird.2	$⊢ φ \to A \in S$
	caovdird.3	$⊢ φ \to B \in S$
	caovdird.4	$⊢ φ \to C \in K$
Assertion	caovdird	$⊢ φ \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		caovdird.2	$⊢ φ \to A \in S$
3		caovdird.3	$⊢ φ \to B \in S$
4		caovdird.4	$⊢ φ \to C \in K$
5		id	$⊢ φ \to φ$
6	1	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)$
7	5 2 3 4 6	syl13anc	$⊢ φ \to (A F B) G C = (A G C) H (B G C)$