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