Metamath Proof Explorer


Theorem caovlem2

Description: Lemma used in real number construction. (Contributed by NM, 26-Aug-1995)

Ref Expression
Hypotheses caovdir.1 A V
caovdir.2 B V
caovdir.3 C 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 V
caovdl.5 H V
caovdl.ass x G y G z = x G y G z
caovdl2.6 R 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 V
2 caovdir.2 B V
3 caovdir.3 C 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 V
7 caovdl.5 H V
8 caovdl.ass x G y G z = x G y G z
9 caovdl2.6 R 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 V
13 ovex B G D G H V
14 ovex A G D G R V
15 ovex B G C G R 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 V
21 ovex D G R 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 V
24 ovex D G H 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