Metamath Proof Explorer


Theorem caovdilem

Description: Lemma used by 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
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 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 ovex A G C V
10 ovex B G D 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