Step | Hyp | Ref
| Expression |
1 | | caovdilemd.cl |
. . . 4
⊢ ((φ ∧
(x ∈
𝑆 ∧ y ∈ 𝑆)) → (x𝐺y) ∈ 𝑆) |
2 | | caovdilemd.a |
. . . 4
⊢ (φ → A ∈ 𝑆) |
3 | | caovdilemd.c |
. . . . 5
⊢ (φ → 𝐶 ∈ 𝑆) |
4 | | caovdilemd.h |
. . . . 5
⊢ (φ → 𝐻 ∈ 𝑆) |
5 | 1, 3, 4 | caovcld 5596 |
. . . 4
⊢ (φ → (𝐶𝐺𝐻) ∈ 𝑆) |
6 | 1, 2, 5 | caovcld 5596 |
. . 3
⊢ (φ → (A𝐺(𝐶𝐺𝐻)) ∈ 𝑆) |
7 | | caovdilemd.b |
. . . 4
⊢ (φ → B ∈ 𝑆) |
8 | | caovdilemd.d |
. . . . 5
⊢ (φ → 𝐷 ∈ 𝑆) |
9 | 1, 8, 4 | caovcld 5596 |
. . . 4
⊢ (φ → (𝐷𝐺𝐻) ∈ 𝑆) |
10 | 1, 7, 9 | caovcld 5596 |
. . 3
⊢ (φ → (B𝐺(𝐷𝐺𝐻)) ∈ 𝑆) |
11 | | caovdl2.6 |
. . . . 5
⊢ (φ → 𝑅 ∈ 𝑆) |
12 | 1, 8, 11 | caovcld 5596 |
. . . 4
⊢ (φ → (𝐷𝐺𝑅) ∈ 𝑆) |
13 | 1, 2, 12 | caovcld 5596 |
. . 3
⊢ (φ → (A𝐺(𝐷𝐺𝑅)) ∈ 𝑆) |
14 | | caovdl2.com |
. . 3
⊢ ((φ ∧
(x ∈
𝑆 ∧ y ∈ 𝑆)) → (x𝐹y) =
(y𝐹x)) |
15 | | caovdl2.ass |
. . 3
⊢ ((φ ∧
(x ∈
𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → ((x𝐹y)𝐹z) = (x𝐹(y𝐹z))) |
16 | 1, 3, 11 | caovcld 5596 |
. . . 4
⊢ (φ → (𝐶𝐺𝑅) ∈ 𝑆) |
17 | 1, 7, 16 | caovcld 5596 |
. . 3
⊢ (φ → (B𝐺(𝐶𝐺𝑅)) ∈ 𝑆) |
18 | | caovdl2.cl |
. . 3
⊢ ((φ ∧
(x ∈
𝑆 ∧ y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆) |
19 | 6, 10, 13, 14, 15, 17, 18 | caov42d 5629 |
. 2
⊢ (φ → (((A𝐺(𝐶𝐺𝐻))𝐹(B𝐺(𝐷𝐺𝐻)))𝐹((A𝐺(𝐷𝐺𝑅))𝐹(B𝐺(𝐶𝐺𝑅)))) = (((A𝐺(𝐶𝐺𝐻))𝐹(A𝐺(𝐷𝐺𝑅)))𝐹((B𝐺(𝐶𝐺𝑅))𝐹(B𝐺(𝐷𝐺𝐻))))) |
20 | | caovdilemd.com |
. . . 4
⊢ ((φ ∧
(x ∈
𝑆 ∧ y ∈ 𝑆)) → (x𝐺y) =
(y𝐺x)) |
21 | | caovdilemd.distr |
. . . 4
⊢ ((φ ∧
(x ∈
𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → ((x𝐹y)𝐺z) = ((x𝐺z)𝐹(y𝐺z))) |
22 | | caovdilemd.ass |
. . . 4
⊢ ((φ ∧
(x ∈
𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → ((x𝐺y)𝐺z) = (x𝐺(y𝐺z))) |
23 | 20, 21, 22, 1, 2, 7,
3, 8, 4 | caovdilemd 5634 |
. . 3
⊢ (φ → (((A𝐺𝐶)𝐹(B𝐺𝐷))𝐺𝐻) = ((A𝐺(𝐶𝐺𝐻))𝐹(B𝐺(𝐷𝐺𝐻)))) |
24 | 20, 21, 22, 1, 2, 7,
8, 3, 11 | caovdilemd 5634 |
. . 3
⊢ (φ → (((A𝐺𝐷)𝐹(B𝐺𝐶))𝐺𝑅) = ((A𝐺(𝐷𝐺𝑅))𝐹(B𝐺(𝐶𝐺𝑅)))) |
25 | 23, 24 | oveq12d 5473 |
. 2
⊢ (φ → ((((A𝐺𝐶)𝐹(B𝐺𝐷))𝐺𝐻)𝐹(((A𝐺𝐷)𝐹(B𝐺𝐶))𝐺𝑅)) = (((A𝐺(𝐶𝐺𝐻))𝐹(B𝐺(𝐷𝐺𝐻)))𝐹((A𝐺(𝐷𝐺𝑅))𝐹(B𝐺(𝐶𝐺𝑅))))) |
26 | | simpr1 909 |
. . . . . . 7
⊢ ((φ ∧
(x ∈
𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → x ∈ 𝑆) |
27 | 18 | caovclg 5595 |
. . . . . . . . 9
⊢ ((φ ∧ (𝑟 ∈ 𝑆 ∧ 𝑠 ∈ 𝑆)) → (𝑟𝐹𝑠) ∈ 𝑆) |
28 | 27 | caovclg 5595 |
. . . . . . . 8
⊢ ((φ ∧
(y ∈
𝑆 ∧ z ∈ 𝑆)) → (y𝐹z) ∈ 𝑆) |
29 | 28 | 3adantr1 1062 |
. . . . . . 7
⊢ ((φ ∧
(x ∈
𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → (y𝐹z) ∈ 𝑆) |
30 | 26, 29 | jca 290 |
. . . . . 6
⊢ ((φ ∧
(x ∈
𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → (x ∈ 𝑆 ∧ (y𝐹z) ∈ 𝑆)) |
31 | 20 | caovcomg 5598 |
. . . . . . 7
⊢ ((φ ∧ (𝑟 ∈ 𝑆 ∧ 𝑠 ∈ 𝑆)) → (𝑟𝐺𝑠) = (𝑠𝐺𝑟)) |
32 | 31 | caovcomg 5598 |
. . . . . 6
⊢ ((φ ∧
(x ∈
𝑆 ∧ (y𝐹z) ∈ 𝑆)) → (x𝐺(y𝐹z)) = ((y𝐹z)𝐺x)) |
33 | 30, 32 | syldan 266 |
. . . . 5
⊢ ((φ ∧
(x ∈
𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → (x𝐺(y𝐹z)) = ((y𝐹z)𝐺x)) |
34 | | 3anrot 889 |
. . . . . 6
⊢
((x ∈ 𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆) ↔ (y ∈ 𝑆 ∧ z ∈ 𝑆 ∧ x ∈ 𝑆)) |
35 | 21 | caovdirg 5620 |
. . . . . . 7
⊢ ((φ ∧ (𝑟 ∈ 𝑆 ∧ 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑆)) → ((𝑟𝐹𝑠)𝐺𝑡) = ((𝑟𝐺𝑡)𝐹(𝑠𝐺𝑡))) |
36 | 35 | caovdirg 5620 |
. . . . . 6
⊢ ((φ ∧
(y ∈
𝑆 ∧ z ∈ 𝑆 ∧ x ∈ 𝑆)) → ((y𝐹z)𝐺x) = ((y𝐺x)𝐹(z𝐺x))) |
37 | 34, 36 | sylan2b 271 |
. . . . 5
⊢ ((φ ∧
(x ∈
𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → ((y𝐹z)𝐺x) = ((y𝐺x)𝐹(z𝐺x))) |
38 | 20 | eqcomd 2042 |
. . . . . . 7
⊢ ((φ ∧
(x ∈
𝑆 ∧ y ∈ 𝑆)) → (y𝐺x) =
(x𝐺y)) |
39 | 38 | 3adantr3 1064 |
. . . . . 6
⊢ ((φ ∧
(x ∈
𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → (y𝐺x) =
(x𝐺y)) |
40 | 31 | caovcomg 5598 |
. . . . . . . 8
⊢ ((φ ∧
(z ∈
𝑆 ∧ x ∈ 𝑆)) → (z𝐺x) =
(x𝐺z)) |
41 | 40 | ancom2s 500 |
. . . . . . 7
⊢ ((φ ∧
(x ∈
𝑆 ∧ z ∈ 𝑆)) → (z𝐺x) =
(x𝐺z)) |
42 | 41 | 3adantr2 1063 |
. . . . . 6
⊢ ((φ ∧
(x ∈
𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → (z𝐺x) =
(x𝐺z)) |
43 | 39, 42 | oveq12d 5473 |
. . . . 5
⊢ ((φ ∧
(x ∈
𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → ((y𝐺x)𝐹(z𝐺x)) =
((x𝐺y)𝐹(x𝐺z))) |
44 | 33, 37, 43 | 3eqtrd 2073 |
. . . 4
⊢ ((φ ∧
(x ∈
𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → (x𝐺(y𝐹z)) = ((x𝐺y)𝐹(x𝐺z))) |
45 | 44, 2, 5, 12 | caovdid 5618 |
. . 3
⊢ (φ → (A𝐺((𝐶𝐺𝐻)𝐹(𝐷𝐺𝑅))) = ((A𝐺(𝐶𝐺𝐻))𝐹(A𝐺(𝐷𝐺𝑅)))) |
46 | 44, 7, 16, 9 | caovdid 5618 |
. . 3
⊢ (φ → (B𝐺((𝐶𝐺𝑅)𝐹(𝐷𝐺𝐻))) = ((B𝐺(𝐶𝐺𝑅))𝐹(B𝐺(𝐷𝐺𝐻)))) |
47 | 45, 46 | oveq12d 5473 |
. 2
⊢ (φ → ((A𝐺((𝐶𝐺𝐻)𝐹(𝐷𝐺𝑅)))𝐹(B𝐺((𝐶𝐺𝑅)𝐹(𝐷𝐺𝐻)))) = (((A𝐺(𝐶𝐺𝐻))𝐹(A𝐺(𝐷𝐺𝑅)))𝐹((B𝐺(𝐶𝐺𝑅))𝐹(B𝐺(𝐷𝐺𝐻))))) |
48 | 19, 25, 47 | 3eqtr4d 2079 |
1
⊢ (φ → ((((A𝐺𝐶)𝐹(B𝐺𝐷))𝐺𝐻)𝐹(((A𝐺𝐷)𝐹(B𝐺𝐶))𝐺𝑅)) = ((A𝐺((𝐶𝐺𝐻)𝐹(𝐷𝐺𝑅)))𝐹(B𝐺((𝐶𝐺𝑅)𝐹(𝐷𝐺𝐻))))) |