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 |
⊢ ( ( ( ( 𝐴 𝐺 𝐶 ) 𝐹 ( 𝐵 𝐺 𝐷 ) ) 𝐺 𝐻 ) 𝐹 ( ( ( 𝐴 𝐺 𝐷 ) 𝐹 ( 𝐵 𝐺 𝐶 ) ) 𝐺 𝑅 ) ) = ( ( 𝐴 𝐺 ( ( 𝐶 𝐺 𝐻 ) 𝐹 ( 𝐷 𝐺 𝑅 ) ) ) 𝐹 ( 𝐵 𝐺 ( ( 𝐶 𝐺 𝑅 ) 𝐹 ( 𝐷 𝐺 𝐻 ) ) ) ) |