Description: Reverse distributive law. (Contributed by NM, 26-Aug-1995)
Ref | Expression | ||
---|---|---|---|
Hypotheses | caovdir.1 | |- A e. _V |
|
caovdir.2 | |- B e. _V |
||
caovdir.3 | |- C e. _V |
||
caovdir.com | |- ( x G y ) = ( y G x ) |
||
caovdir.distr | |- ( x G ( y F z ) ) = ( ( x G y ) F ( x G z ) ) |
||
Assertion | caovdir | |- ( ( A F B ) G C ) = ( ( A G C ) F ( B G C ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | caovdir.1 | |- A e. _V |
|
2 | caovdir.2 | |- B e. _V |
|
3 | caovdir.3 | |- C e. _V |
|
4 | caovdir.com | |- ( x G y ) = ( y G x ) |
|
5 | caovdir.distr | |- ( x G ( y F z ) ) = ( ( x G y ) F ( x G z ) ) |
|
6 | 3 1 2 5 | caovdi | |- ( C G ( A F B ) ) = ( ( C G A ) F ( C G B ) ) |
7 | ovex | |- ( A F B ) e. _V |
|
8 | 3 7 4 | caovcom | |- ( C G ( A F B ) ) = ( ( A F B ) G C ) |
9 | 3 1 4 | caovcom | |- ( C G A ) = ( A G C ) |
10 | 3 2 4 | caovcom | |- ( C G B ) = ( B G C ) |
11 | 9 10 | oveq12i | |- ( ( C G A ) F ( C G B ) ) = ( ( A G C ) F ( B G C ) ) |
12 | 6 8 11 | 3eqtr3i | |- ( ( A F B ) G C ) = ( ( A G C ) F ( B G C ) ) |