Metamath Proof Explorer

Theorem caovdid

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

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