Metamath Proof Explorer

Theorem caovlem2

Description: Lemma used in 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 ) )
caovdl2.6 
|- R e. _V
caovdl2.com 
|- ( x F y ) = ( y F x )
caovdl2.ass 
|- ( ( x F y ) F z ) = ( x F ( y F z ) )
Assertion caovlem2 
|- ( ( ( ( A G C ) F ( B G D ) ) G H ) F ( ( ( A G D ) F ( B G C ) ) G R ) ) = ( ( A G ( ( C G H ) F ( D G R ) ) ) F ( B G ( ( C G R ) F ( 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 caovdl2.6 
 |-  R e. _V
10 caovdl2.com 
 |-  ( x F y ) = ( y F x )
11 caovdl2.ass 
 |-  ( ( x F y ) F z ) = ( x F ( y F z ) )
12 ovex 
 |-  ( A G ( C G H ) ) e. _V
13 ovex 
 |-  ( B G ( D G H ) ) e. _V
14 ovex 
 |-  ( A G ( D G R ) ) e. _V
15 ovex 
 |-  ( B G ( C G R ) ) e. _V
16 12 13 14 10 11 15 caov42 
 |-  ( ( ( A G ( C G H ) ) F ( B G ( D G H ) ) ) F ( ( A G ( D G R ) ) F ( B G ( C G R ) ) ) ) = ( ( ( A G ( C G H ) ) F ( A G ( D G R ) ) ) F ( ( B G ( C G R ) ) F ( B G ( D G H ) ) ) )
17 1 2 3 4 5 6 7 8 caovdilem 
 |-  ( ( ( A G C ) F ( B G D ) ) G H ) = ( ( A G ( C G H ) ) F ( B G ( D G H ) ) )
18 1 2 6 4 5 3 9 8 caovdilem 
 |-  ( ( ( A G D ) F ( B G C ) ) G R ) = ( ( A G ( D G R ) ) F ( B G ( C G R ) ) )
19 17 18 oveq12i 
 |-  ( ( ( ( A G C ) F ( B G D ) ) G H ) F ( ( ( A G D ) F ( B G C ) ) G R ) ) = ( ( ( A G ( C G H ) ) F ( B G ( D G H ) ) ) F ( ( A G ( D G R ) ) F ( B G ( C G R ) ) ) )
20 ovex 
 |-  ( C G H ) e. _V
21 ovex 
 |-  ( D G R ) e. _V
22 1 20 21 5 caovdi 
 |-  ( A G ( ( C G H ) F ( D G R ) ) ) = ( ( A G ( C G H ) ) F ( A G ( D G R ) ) )
23 ovex 
 |-  ( C G R ) e. _V
24 ovex 
 |-  ( D G H ) e. _V
25 2 23 24 5 caovdi 
 |-  ( B G ( ( C G R ) F ( D G H ) ) ) = ( ( B G ( C G R ) ) F ( B G ( D G H ) ) )
26 22 25 oveq12i 
 |-  ( ( A G ( ( C G H ) F ( D G R ) ) ) F ( B G ( ( C G R ) F ( D G H ) ) ) ) = ( ( ( A G ( C G H ) ) F ( A G ( D G R ) ) ) F ( ( B G ( C G R ) ) F ( B G ( D G H ) ) ) )
27 16 19 26 3eqtr4i 
 |-  ( ( ( ( A G C ) F ( B G D ) ) G H ) F ( ( ( A G D ) F ( B G C ) ) G R ) ) = ( ( A G ( ( C G H ) F ( D G R ) ) ) F ( B G ( ( C G R ) F ( D G H ) ) ) )