This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem caovdir2d

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

Ref Expression
Hypotheses caovdir2d.1 
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( x G ( y F z ) ) = ( ( x G y ) F ( x G z ) ) )
caovdir2d.2 
|- ( ph -> A e. S )
caovdir2d.3 
|- ( ph -> B e. S )
caovdir2d.4 
|- ( ph -> C e. S )
caovdir2d.cl 
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) e. S )
caovdir2d.com 
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x G y ) = ( y G x ) )
Assertion caovdir2d 
|- ( ph -> ( ( A F B ) G C ) = ( ( A G C ) F ( B G C ) ) )

Proof

Step Hyp Ref Expression
1 caovdir2d.1 
 |-  ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( x G ( y F z ) ) = ( ( x G y ) F ( x G z ) ) )
2 caovdir2d.2 
 |-  ( ph -> A e. S )
3 caovdir2d.3 
 |-  ( ph -> B e. S )
4 caovdir2d.4 
 |-  ( ph -> C e. S )
5 caovdir2d.cl 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) e. S )
6 caovdir2d.com 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x G y ) = ( y G x ) )
7 1 4 2 3 caovdid 
 |-  ( ph -> ( C G ( A F B ) ) = ( ( C G A ) F ( C G B ) ) )
8 5 2 3 caovcld 
 |-  ( ph -> ( A F B ) e. S )
9 6 8 4 caovcomd 
 |-  ( ph -> ( ( A F B ) G C ) = ( C G ( A F B ) ) )
10 6 2 4 caovcomd 
 |-  ( ph -> ( A G C ) = ( C G A ) )
11 6 3 4 caovcomd 
 |-  ( ph -> ( B G C ) = ( C G B ) )
12 10 11 oveq12d 
 |-  ( ph -> ( ( A G C ) F ( B G C ) ) = ( ( C G A ) F ( C G B ) ) )
13 7 9 12 3eqtr4d 
 |-  ( ph -> ( ( A F B ) G C ) = ( ( A G C ) F ( B G C ) ) )