Metamath Proof Explorer


Theorem caovdilem

Description: Lemma used by 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 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) )
Assertion caovdilem ( ( ( 𝐴 𝐺 𝐶 ) 𝐹 ( 𝐵 𝐺 𝐷 ) ) 𝐺 𝐻 ) = ( ( 𝐴 𝐺 ( 𝐶 𝐺 𝐻 ) ) 𝐹 ( 𝐵 𝐺 ( 𝐷 𝐺 𝐻 ) ) )

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 ovex ( 𝐴 𝐺 𝐶 ) ∈ V
10 ovex ( 𝐵 𝐺 𝐷 ) ∈ V
11 9 10 7 4 5 caovdir ( ( ( 𝐴 𝐺 𝐶 ) 𝐹 ( 𝐵 𝐺 𝐷 ) ) 𝐺 𝐻 ) = ( ( ( 𝐴 𝐺 𝐶 ) 𝐺 𝐻 ) 𝐹 ( ( 𝐵 𝐺 𝐷 ) 𝐺 𝐻 ) )
12 1 3 7 8 caovass ( ( 𝐴 𝐺 𝐶 ) 𝐺 𝐻 ) = ( 𝐴 𝐺 ( 𝐶 𝐺 𝐻 ) )
13 2 6 7 8 caovass ( ( 𝐵 𝐺 𝐷 ) 𝐺 𝐻 ) = ( 𝐵 𝐺 ( 𝐷 𝐺 𝐻 ) )
14 12 13 oveq12i ( ( ( 𝐴 𝐺 𝐶 ) 𝐺 𝐻 ) 𝐹 ( ( 𝐵 𝐺 𝐷 ) 𝐺 𝐻 ) ) = ( ( 𝐴 𝐺 ( 𝐶 𝐺 𝐻 ) ) 𝐹 ( 𝐵 𝐺 ( 𝐷 𝐺 𝐻 ) ) )
15 11 14 eqtri ( ( ( 𝐴 𝐺 𝐶 ) 𝐹 ( 𝐵 𝐺 𝐷 ) ) 𝐺 𝐻 ) = ( ( 𝐴 𝐺 ( 𝐶 𝐺 𝐻 ) ) 𝐹 ( 𝐵 𝐺 ( 𝐷 𝐺 𝐻 ) ) )