Metamath Proof Explorer

Theorem caovlem2

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

Ref Expression
Hypotheses caovdir.1 ⊢ 𝐴 ∈ V
caovdir.2 ⊢ 𝐵 ∈ V
caovdir.3 ⊢ 𝐶 ∈ V
caovdir.com ⊢ ( 𝑥 𝐺 𝑦 ) = ( 𝑦 𝐺 𝑥 )
caovdir.distr ⊢ ( 𝑥 𝐺 ( 𝑦 𝐹 𝑧 ) ) = ( ( 𝑥 𝐺 𝑦 ) 𝐹 ( 𝑥 𝐺 𝑧 ) )
caovdl.4 ⊢ 𝐷 ∈ V
caovdl.5 ⊢ 𝐻 ∈ V
caovdl.ass ⊢ ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) )
caovdl2.6 ⊢ 𝑅 ∈ V
caovdl2.com ⊢ ( 𝑥 𝐹 𝑦 ) = ( 𝑦 𝐹 𝑥 )
caovdl2.ass ⊢ ( ( 𝑥 𝐹 𝑦 ) 𝐹 𝑧 ) = ( 𝑥 𝐹 ( 𝑦 𝐹 𝑧 ) )
Assertion caovlem2 ( ( ( ( 𝐴 𝐺 𝐶 ) 𝐹 ( 𝐵 𝐺 𝐷 ) ) 𝐺 𝐻 ) 𝐹 ( ( ( 𝐴 𝐺 𝐷 ) 𝐹 ( 𝐵 𝐺 𝐶 ) ) 𝐺 𝑅 ) ) = ( ( 𝐴 𝐺 ( ( 𝐶 𝐺 𝐻 ) 𝐹 ( 𝐷 𝐺 𝑅 ) ) ) 𝐹 ( 𝐵 𝐺 ( ( 𝐶 𝐺 𝑅 ) 𝐹 ( 𝐷 𝐺 𝐻 ) ) ) )

Proof

Step Hyp Ref Expression
1 caovdir.1 ⊢ 𝐴 ∈ V
2 caovdir.2 ⊢ 𝐵 ∈ V
3 caovdir.3 ⊢ 𝐶 ∈ V
4 caovdir.com ⊢ ( 𝑥 𝐺 𝑦 ) = ( 𝑦 𝐺 𝑥 )
5 caovdir.distr ⊢ ( 𝑥 𝐺 ( 𝑦 𝐹 𝑧 ) ) = ( ( 𝑥 𝐺 𝑦 ) 𝐹 ( 𝑥 𝐺 𝑧 ) )
6 caovdl.4 ⊢ 𝐷 ∈ V
7 caovdl.5 ⊢ 𝐻 ∈ V
8 caovdl.ass ⊢ ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) )
9 caovdl2.6 ⊢ 𝑅 ∈ V
10 caovdl2.com ⊢ ( 𝑥 𝐹 𝑦 ) = ( 𝑦 𝐹 𝑥 )
11 caovdl2.ass ⊢ ( ( 𝑥 𝐹 𝑦 ) 𝐹 𝑧 ) = ( 𝑥 𝐹 ( 𝑦 𝐹 𝑧 ) )
12 ovex ⊢ ( 𝐴 𝐺 ( 𝐶 𝐺 𝐻 ) ) ∈ V
13 ovex ⊢ ( 𝐵 𝐺 ( 𝐷 𝐺 𝐻 ) ) ∈ V
14 ovex ⊢ ( 𝐴 𝐺 ( 𝐷 𝐺 𝑅 ) ) ∈ V
15 ovex ⊢ ( 𝐵 𝐺 ( 𝐶 𝐺 𝑅 ) ) ∈ V
16 12 13 14 10 11 15 caov42 ⊢ ( ( ( 𝐴 𝐺 ( 𝐶 𝐺 𝐻 ) ) 𝐹 ( 𝐵 𝐺 ( 𝐷 𝐺 𝐻 ) ) ) 𝐹 ( ( 𝐴 𝐺 ( 𝐷 𝐺 𝑅 ) ) 𝐹 ( 𝐵 𝐺 ( 𝐶 𝐺 𝑅 ) ) ) ) = ( ( ( 𝐴 𝐺 ( 𝐶 𝐺 𝐻 ) ) 𝐹 ( 𝐴 𝐺 ( 𝐷 𝐺 𝑅 ) ) ) 𝐹 ( ( 𝐵 𝐺 ( 𝐶 𝐺 𝑅 ) ) 𝐹 ( 𝐵 𝐺 ( 𝐷 𝐺 𝐻 ) ) ) )
17 1 2 3 4 5 6 7 8 caovdilem ⊢ ( ( ( 𝐴 𝐺 𝐶 ) 𝐹 ( 𝐵 𝐺 𝐷 ) ) 𝐺 𝐻 ) = ( ( 𝐴 𝐺 ( 𝐶 𝐺 𝐻 ) ) 𝐹 ( 𝐵 𝐺 ( 𝐷 𝐺 𝐻 ) ) )
18 1 2 6 4 5 3 9 8 caovdilem ⊢ ( ( ( 𝐴 𝐺 𝐷 ) 𝐹 ( 𝐵 𝐺 𝐶 ) ) 𝐺 𝑅 ) = ( ( 𝐴 𝐺 ( 𝐷 𝐺 𝑅 ) ) 𝐹 ( 𝐵 𝐺 ( 𝐶 𝐺 𝑅 ) ) )
19 17 18 oveq12i ⊢ ( ( ( ( 𝐴 𝐺 𝐶 ) 𝐹 ( 𝐵 𝐺 𝐷 ) ) 𝐺 𝐻 ) 𝐹 ( ( ( 𝐴 𝐺 𝐷 ) 𝐹 ( 𝐵 𝐺 𝐶 ) ) 𝐺 𝑅 ) ) = ( ( ( 𝐴 𝐺 ( 𝐶 𝐺 𝐻 ) ) 𝐹 ( 𝐵 𝐺 ( 𝐷 𝐺 𝐻 ) ) ) 𝐹 ( ( 𝐴 𝐺 ( 𝐷 𝐺 𝑅 ) ) 𝐹 ( 𝐵 𝐺 ( 𝐶 𝐺 𝑅 ) ) ) )
20 ovex ⊢ ( 𝐶 𝐺 𝐻 ) ∈ V
21 ovex ⊢ ( 𝐷 𝐺 𝑅 ) ∈ V
22 1 20 21 5 caovdi ⊢ ( 𝐴 𝐺 ( ( 𝐶 𝐺 𝐻 ) 𝐹 ( 𝐷 𝐺 𝑅 ) ) ) = ( ( 𝐴 𝐺 ( 𝐶 𝐺 𝐻 ) ) 𝐹 ( 𝐴 𝐺 ( 𝐷 𝐺 𝑅 ) ) )
23 ovex ⊢ ( 𝐶 𝐺 𝑅 ) ∈ V
24 ovex ⊢ ( 𝐷 𝐺 𝐻 ) ∈ V
25 2 23 24 5 caovdi ⊢ ( 𝐵 𝐺 ( ( 𝐶 𝐺 𝑅 ) 𝐹 ( 𝐷 𝐺 𝐻 ) ) ) = ( ( 𝐵 𝐺 ( 𝐶 𝐺 𝑅 ) ) 𝐹 ( 𝐵 𝐺 ( 𝐷 𝐺 𝐻 ) ) )
26 22 25 oveq12i ⊢ ( ( 𝐴 𝐺 ( ( 𝐶 𝐺 𝐻 ) 𝐹 ( 𝐷 𝐺 𝑅 ) ) ) 𝐹 ( 𝐵 𝐺 ( ( 𝐶 𝐺 𝑅 ) 𝐹 ( 𝐷 𝐺 𝐻 ) ) ) ) = ( ( ( 𝐴 𝐺 ( 𝐶 𝐺 𝐻 ) ) 𝐹 ( 𝐴 𝐺 ( 𝐷 𝐺 𝑅 ) ) ) 𝐹 ( ( 𝐵 𝐺 ( 𝐶 𝐺 𝑅 ) ) 𝐹 ( 𝐵 𝐺 ( 𝐷 𝐺 𝐻 ) ) ) )
27 16 19 26 3eqtr4i ⊢ ( ( ( ( 𝐴 𝐺 𝐶 ) 𝐹 ( 𝐵 𝐺 𝐷 ) ) 𝐺 𝐻 ) 𝐹 ( ( ( 𝐴 𝐺 𝐷 ) 𝐹 ( 𝐵 𝐺 𝐶 ) ) 𝐺 𝑅 ) ) = ( ( 𝐴 𝐺 ( ( 𝐶 𝐺 𝐻 ) 𝐹 ( 𝐷 𝐺 𝑅 ) ) ) 𝐹 ( 𝐵 𝐺 ( ( 𝐶 𝐺 𝑅 ) 𝐹 ( 𝐷 𝐺 𝐻 ) ) ) )