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