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 ) ) )