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

Metamath Proof Explorer

Theorem caovdilem

Description: Lemma used by real number construction. (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 ) )
caovdl.4 
|- D e. _V
caovdl.5 
|- H e. _V
caovdl.ass 
|- ( ( x G y ) G z ) = ( x G ( y G z ) )
Assertion caovdilem 
|- ( ( ( A G C ) F ( B G D ) ) G H ) = ( ( A G ( C G H ) ) F ( B G ( D G H ) ) )

Proof

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 caovdl.4 
 |-  D e. _V
7 caovdl.5 
 |-  H e. _V
8 caovdl.ass 
 |-  ( ( x G y ) G z ) = ( x G ( y G z ) )
9 ovex 
 |-  ( A G C ) e. _V
10 ovex 
 |-  ( B G D ) e. _V
11 9 10 7 4 5 caovdir 
 |-  ( ( ( A G C ) F ( B G D ) ) G H ) = ( ( ( A G C ) G H ) F ( ( B G D ) G H ) )
12 1 3 7 8 caovass 
 |-  ( ( A G C ) G H ) = ( A G ( C G H ) )
13 2 6 7 8 caovass 
 |-  ( ( B G D ) G H ) = ( B G ( D G H ) )
14 12 13 oveq12i 
 |-  ( ( ( A G C ) G H ) F ( ( B G D ) G H ) ) = ( ( A G ( C G H ) ) F ( B G ( D G H ) ) )
15 11 14 eqtri 
 |-  ( ( ( A G C ) F ( B G D ) ) G H ) = ( ( A G ( C G H ) ) F ( B G ( D G H ) ) )