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 ⊢xGy=yGx
caovdir.distr ⊢xGyFz=xGyFxGz
caovdl.4 ⊢D∈V
caovdl.5 ⊢H∈V
caovdl.ass ⊢xGyGz=xGyGz
caovdl2.6 ⊢R∈V
caovdl2.com ⊢xFy=yFx
caovdl2.ass ⊢xFyFz=xFyFz
Assertion caovlem2 ⊢AGCFBGDGHFAGDFBGCGR=AGCGHFDGRFBGCGRFDGH

Proof

Step Hyp Ref Expression
1 caovdir.1 ⊢A∈V
2 caovdir.2 ⊢B∈V
3 caovdir.3 ⊢C∈V
4 caovdir.com ⊢xGy=yGx
5 caovdir.distr ⊢xGyFz=xGyFxGz
6 caovdl.4 ⊢D∈V
7 caovdl.5 ⊢H∈V
8 caovdl.ass ⊢xGyGz=xGyGz
9 caovdl2.6 ⊢R∈V
10 caovdl2.com ⊢xFy=yFx
11 caovdl2.ass ⊢xFyFz=xFyFz
12 ovex ⊢AGCGH∈V
13 ovex ⊢BGDGH∈V
14 ovex ⊢AGDGR∈V
15 ovex ⊢BGCGR∈V
16 12 13 14 10 11 15 caov42 ⊢AGCGHFBGDGHFAGDGRFBGCGR=AGCGHFAGDGRFBGCGRFBGDGH
17 1 2 3 4 5 6 7 8 caovdilem ⊢AGCFBGDGH=AGCGHFBGDGH
18 1 2 6 4 5 3 9 8 caovdilem ⊢AGDFBGCGR=AGDGRFBGCGR
19 17 18 oveq12i ⊢AGCFBGDGHFAGDFBGCGR=AGCGHFBGDGHFAGDGRFBGCGR
20 ovex ⊢CGH∈V
21 ovex ⊢DGR∈V
22 1 20 21 5 caovdi ⊢AGCGHFDGR=AGCGHFAGDGR
23 ovex ⊢CGR∈V
24 ovex ⊢DGH∈V
25 2 23 24 5 caovdi ⊢BGCGRFDGH=BGCGRFBGDGH
26 22 25 oveq12i ⊢AGCGHFDGRFBGCGRFDGH=AGCGHFAGDGRFBGCGRFBGDGH
27 16 19 26 3eqtr4i ⊢AGCFBGDGHFAGDFBGCGR=AGCGHFDGRFBGCGRFDGH