Proof of Theorem golem1
Step | Hyp | Ref
| Expression |
1 | | golem1.1 |
. . . . . . . . . . 11
⊢ 𝐴 ∈
Cℋ |
2 | 1 | choccli 29388 |
. . . . . . . . . 10
⊢
(⊥‘𝐴)
∈ Cℋ |
3 | | stcl 30297 |
. . . . . . . . . 10
⊢ (𝑓 ∈ States →
((⊥‘𝐴) ∈
Cℋ → (𝑓‘(⊥‘𝐴)) ∈ ℝ)) |
4 | 2, 3 | mpi 20 |
. . . . . . . . 9
⊢ (𝑓 ∈ States → (𝑓‘(⊥‘𝐴)) ∈
ℝ) |
5 | 4 | recnd 10861 |
. . . . . . . 8
⊢ (𝑓 ∈ States → (𝑓‘(⊥‘𝐴)) ∈
ℂ) |
6 | | golem1.2 |
. . . . . . . . . . 11
⊢ 𝐵 ∈
Cℋ |
7 | 6 | choccli 29388 |
. . . . . . . . . 10
⊢
(⊥‘𝐵)
∈ Cℋ |
8 | | stcl 30297 |
. . . . . . . . . 10
⊢ (𝑓 ∈ States →
((⊥‘𝐵) ∈
Cℋ → (𝑓‘(⊥‘𝐵)) ∈ ℝ)) |
9 | 7, 8 | mpi 20 |
. . . . . . . . 9
⊢ (𝑓 ∈ States → (𝑓‘(⊥‘𝐵)) ∈
ℝ) |
10 | 9 | recnd 10861 |
. . . . . . . 8
⊢ (𝑓 ∈ States → (𝑓‘(⊥‘𝐵)) ∈
ℂ) |
11 | | golem1.3 |
. . . . . . . . . . 11
⊢ 𝐶 ∈
Cℋ |
12 | 11 | choccli 29388 |
. . . . . . . . . 10
⊢
(⊥‘𝐶)
∈ Cℋ |
13 | | stcl 30297 |
. . . . . . . . . 10
⊢ (𝑓 ∈ States →
((⊥‘𝐶) ∈
Cℋ → (𝑓‘(⊥‘𝐶)) ∈ ℝ)) |
14 | 12, 13 | mpi 20 |
. . . . . . . . 9
⊢ (𝑓 ∈ States → (𝑓‘(⊥‘𝐶)) ∈
ℝ) |
15 | 14 | recnd 10861 |
. . . . . . . 8
⊢ (𝑓 ∈ States → (𝑓‘(⊥‘𝐶)) ∈
ℂ) |
16 | 5, 10, 15 | addassd 10855 |
. . . . . . 7
⊢ (𝑓 ∈ States → (((𝑓‘(⊥‘𝐴)) + (𝑓‘(⊥‘𝐵))) + (𝑓‘(⊥‘𝐶))) = ((𝑓‘(⊥‘𝐴)) + ((𝑓‘(⊥‘𝐵)) + (𝑓‘(⊥‘𝐶))))) |
17 | 10, 15 | addcld 10852 |
. . . . . . . 8
⊢ (𝑓 ∈ States → ((𝑓‘(⊥‘𝐵)) + (𝑓‘(⊥‘𝐶))) ∈ ℂ) |
18 | 5, 17 | addcomd 11034 |
. . . . . . 7
⊢ (𝑓 ∈ States → ((𝑓‘(⊥‘𝐴)) + ((𝑓‘(⊥‘𝐵)) + (𝑓‘(⊥‘𝐶)))) = (((𝑓‘(⊥‘𝐵)) + (𝑓‘(⊥‘𝐶))) + (𝑓‘(⊥‘𝐴)))) |
19 | 16, 18 | eqtrd 2777 |
. . . . . 6
⊢ (𝑓 ∈ States → (((𝑓‘(⊥‘𝐴)) + (𝑓‘(⊥‘𝐵))) + (𝑓‘(⊥‘𝐶))) = (((𝑓‘(⊥‘𝐵)) + (𝑓‘(⊥‘𝐶))) + (𝑓‘(⊥‘𝐴)))) |
20 | 19 | oveq1d 7228 |
. . . . 5
⊢ (𝑓 ∈ States → ((((𝑓‘(⊥‘𝐴)) + (𝑓‘(⊥‘𝐵))) + (𝑓‘(⊥‘𝐶))) + (((𝑓‘(𝐴 ∩ 𝐵)) + (𝑓‘(𝐵 ∩ 𝐶))) + (𝑓‘(𝐶 ∩ 𝐴)))) = ((((𝑓‘(⊥‘𝐵)) + (𝑓‘(⊥‘𝐶))) + (𝑓‘(⊥‘𝐴))) + (((𝑓‘(𝐴 ∩ 𝐵)) + (𝑓‘(𝐵 ∩ 𝐶))) + (𝑓‘(𝐶 ∩ 𝐴))))) |
21 | 5, 10 | addcld 10852 |
. . . . . 6
⊢ (𝑓 ∈ States → ((𝑓‘(⊥‘𝐴)) + (𝑓‘(⊥‘𝐵))) ∈ ℂ) |
22 | 1, 6 | chincli 29541 |
. . . . . . . . 9
⊢ (𝐴 ∩ 𝐵) ∈
Cℋ |
23 | | stcl 30297 |
. . . . . . . . 9
⊢ (𝑓 ∈ States → ((𝐴 ∩ 𝐵) ∈ Cℋ
→ (𝑓‘(𝐴 ∩ 𝐵)) ∈ ℝ)) |
24 | 22, 23 | mpi 20 |
. . . . . . . 8
⊢ (𝑓 ∈ States → (𝑓‘(𝐴 ∩ 𝐵)) ∈ ℝ) |
25 | 24 | recnd 10861 |
. . . . . . 7
⊢ (𝑓 ∈ States → (𝑓‘(𝐴 ∩ 𝐵)) ∈ ℂ) |
26 | 6, 11 | chincli 29541 |
. . . . . . . . 9
⊢ (𝐵 ∩ 𝐶) ∈
Cℋ |
27 | | stcl 30297 |
. . . . . . . . 9
⊢ (𝑓 ∈ States → ((𝐵 ∩ 𝐶) ∈ Cℋ
→ (𝑓‘(𝐵 ∩ 𝐶)) ∈ ℝ)) |
28 | 26, 27 | mpi 20 |
. . . . . . . 8
⊢ (𝑓 ∈ States → (𝑓‘(𝐵 ∩ 𝐶)) ∈ ℝ) |
29 | 28 | recnd 10861 |
. . . . . . 7
⊢ (𝑓 ∈ States → (𝑓‘(𝐵 ∩ 𝐶)) ∈ ℂ) |
30 | 25, 29 | addcld 10852 |
. . . . . 6
⊢ (𝑓 ∈ States → ((𝑓‘(𝐴 ∩ 𝐵)) + (𝑓‘(𝐵 ∩ 𝐶))) ∈ ℂ) |
31 | 11, 1 | chincli 29541 |
. . . . . . . 8
⊢ (𝐶 ∩ 𝐴) ∈
Cℋ |
32 | | stcl 30297 |
. . . . . . . 8
⊢ (𝑓 ∈ States → ((𝐶 ∩ 𝐴) ∈ Cℋ
→ (𝑓‘(𝐶 ∩ 𝐴)) ∈ ℝ)) |
33 | 31, 32 | mpi 20 |
. . . . . . 7
⊢ (𝑓 ∈ States → (𝑓‘(𝐶 ∩ 𝐴)) ∈ ℝ) |
34 | 33 | recnd 10861 |
. . . . . 6
⊢ (𝑓 ∈ States → (𝑓‘(𝐶 ∩ 𝐴)) ∈ ℂ) |
35 | 21, 30, 15, 34 | add4d 11060 |
. . . . 5
⊢ (𝑓 ∈ States → ((((𝑓‘(⊥‘𝐴)) + (𝑓‘(⊥‘𝐵))) + ((𝑓‘(𝐴 ∩ 𝐵)) + (𝑓‘(𝐵 ∩ 𝐶)))) + ((𝑓‘(⊥‘𝐶)) + (𝑓‘(𝐶 ∩ 𝐴)))) = ((((𝑓‘(⊥‘𝐴)) + (𝑓‘(⊥‘𝐵))) + (𝑓‘(⊥‘𝐶))) + (((𝑓‘(𝐴 ∩ 𝐵)) + (𝑓‘(𝐵 ∩ 𝐶))) + (𝑓‘(𝐶 ∩ 𝐴))))) |
36 | 17, 30, 5, 34 | add4d 11060 |
. . . . 5
⊢ (𝑓 ∈ States → ((((𝑓‘(⊥‘𝐵)) + (𝑓‘(⊥‘𝐶))) + ((𝑓‘(𝐴 ∩ 𝐵)) + (𝑓‘(𝐵 ∩ 𝐶)))) + ((𝑓‘(⊥‘𝐴)) + (𝑓‘(𝐶 ∩ 𝐴)))) = ((((𝑓‘(⊥‘𝐵)) + (𝑓‘(⊥‘𝐶))) + (𝑓‘(⊥‘𝐴))) + (((𝑓‘(𝐴 ∩ 𝐵)) + (𝑓‘(𝐵 ∩ 𝐶))) + (𝑓‘(𝐶 ∩ 𝐴))))) |
37 | 20, 35, 36 | 3eqtr4d 2787 |
. . . 4
⊢ (𝑓 ∈ States → ((((𝑓‘(⊥‘𝐴)) + (𝑓‘(⊥‘𝐵))) + ((𝑓‘(𝐴 ∩ 𝐵)) + (𝑓‘(𝐵 ∩ 𝐶)))) + ((𝑓‘(⊥‘𝐶)) + (𝑓‘(𝐶 ∩ 𝐴)))) = ((((𝑓‘(⊥‘𝐵)) + (𝑓‘(⊥‘𝐶))) + ((𝑓‘(𝐴 ∩ 𝐵)) + (𝑓‘(𝐵 ∩ 𝐶)))) + ((𝑓‘(⊥‘𝐴)) + (𝑓‘(𝐶 ∩ 𝐴))))) |
38 | 5, 25, 10, 29 | add4d 11060 |
. . . . 5
⊢ (𝑓 ∈ States → (((𝑓‘(⊥‘𝐴)) + (𝑓‘(𝐴 ∩ 𝐵))) + ((𝑓‘(⊥‘𝐵)) + (𝑓‘(𝐵 ∩ 𝐶)))) = (((𝑓‘(⊥‘𝐴)) + (𝑓‘(⊥‘𝐵))) + ((𝑓‘(𝐴 ∩ 𝐵)) + (𝑓‘(𝐵 ∩ 𝐶))))) |
39 | 38 | oveq1d 7228 |
. . . 4
⊢ (𝑓 ∈ States → ((((𝑓‘(⊥‘𝐴)) + (𝑓‘(𝐴 ∩ 𝐵))) + ((𝑓‘(⊥‘𝐵)) + (𝑓‘(𝐵 ∩ 𝐶)))) + ((𝑓‘(⊥‘𝐶)) + (𝑓‘(𝐶 ∩ 𝐴)))) = ((((𝑓‘(⊥‘𝐴)) + (𝑓‘(⊥‘𝐵))) + ((𝑓‘(𝐴 ∩ 𝐵)) + (𝑓‘(𝐵 ∩ 𝐶)))) + ((𝑓‘(⊥‘𝐶)) + (𝑓‘(𝐶 ∩ 𝐴))))) |
40 | 10, 25, 15, 29 | add4d 11060 |
. . . . 5
⊢ (𝑓 ∈ States → (((𝑓‘(⊥‘𝐵)) + (𝑓‘(𝐴 ∩ 𝐵))) + ((𝑓‘(⊥‘𝐶)) + (𝑓‘(𝐵 ∩ 𝐶)))) = (((𝑓‘(⊥‘𝐵)) + (𝑓‘(⊥‘𝐶))) + ((𝑓‘(𝐴 ∩ 𝐵)) + (𝑓‘(𝐵 ∩ 𝐶))))) |
41 | 40 | oveq1d 7228 |
. . . 4
⊢ (𝑓 ∈ States → ((((𝑓‘(⊥‘𝐵)) + (𝑓‘(𝐴 ∩ 𝐵))) + ((𝑓‘(⊥‘𝐶)) + (𝑓‘(𝐵 ∩ 𝐶)))) + ((𝑓‘(⊥‘𝐴)) + (𝑓‘(𝐶 ∩ 𝐴)))) = ((((𝑓‘(⊥‘𝐵)) + (𝑓‘(⊥‘𝐶))) + ((𝑓‘(𝐴 ∩ 𝐵)) + (𝑓‘(𝐵 ∩ 𝐶)))) + ((𝑓‘(⊥‘𝐴)) + (𝑓‘(𝐶 ∩ 𝐴))))) |
42 | 37, 39, 41 | 3eqtr4d 2787 |
. . 3
⊢ (𝑓 ∈ States → ((((𝑓‘(⊥‘𝐴)) + (𝑓‘(𝐴 ∩ 𝐵))) + ((𝑓‘(⊥‘𝐵)) + (𝑓‘(𝐵 ∩ 𝐶)))) + ((𝑓‘(⊥‘𝐶)) + (𝑓‘(𝐶 ∩ 𝐴)))) = ((((𝑓‘(⊥‘𝐵)) + (𝑓‘(𝐴 ∩ 𝐵))) + ((𝑓‘(⊥‘𝐶)) + (𝑓‘(𝐵 ∩ 𝐶)))) + ((𝑓‘(⊥‘𝐴)) + (𝑓‘(𝐶 ∩ 𝐴))))) |
43 | 1, 6 | stji1i 30323 |
. . . . 5
⊢ (𝑓 ∈ States → (𝑓‘((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐵))) = ((𝑓‘(⊥‘𝐴)) + (𝑓‘(𝐴 ∩ 𝐵)))) |
44 | 6, 11 | stji1i 30323 |
. . . . 5
⊢ (𝑓 ∈ States → (𝑓‘((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐶))) = ((𝑓‘(⊥‘𝐵)) + (𝑓‘(𝐵 ∩ 𝐶)))) |
45 | 43, 44 | oveq12d 7231 |
. . . 4
⊢ (𝑓 ∈ States → ((𝑓‘((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐵))) + (𝑓‘((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐶)))) = (((𝑓‘(⊥‘𝐴)) + (𝑓‘(𝐴 ∩ 𝐵))) + ((𝑓‘(⊥‘𝐵)) + (𝑓‘(𝐵 ∩ 𝐶))))) |
46 | 11, 1 | stji1i 30323 |
. . . 4
⊢ (𝑓 ∈ States → (𝑓‘((⊥‘𝐶) ∨ℋ (𝐶 ∩ 𝐴))) = ((𝑓‘(⊥‘𝐶)) + (𝑓‘(𝐶 ∩ 𝐴)))) |
47 | 45, 46 | oveq12d 7231 |
. . 3
⊢ (𝑓 ∈ States → (((𝑓‘((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐵))) + (𝑓‘((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐶)))) + (𝑓‘((⊥‘𝐶) ∨ℋ (𝐶 ∩ 𝐴)))) = ((((𝑓‘(⊥‘𝐴)) + (𝑓‘(𝐴 ∩ 𝐵))) + ((𝑓‘(⊥‘𝐵)) + (𝑓‘(𝐵 ∩ 𝐶)))) + ((𝑓‘(⊥‘𝐶)) + (𝑓‘(𝐶 ∩ 𝐴))))) |
48 | 6, 1 | stji1i 30323 |
. . . . . 6
⊢ (𝑓 ∈ States → (𝑓‘((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐴))) = ((𝑓‘(⊥‘𝐵)) + (𝑓‘(𝐵 ∩ 𝐴)))) |
49 | | incom 4115 |
. . . . . . . 8
⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵) |
50 | 49 | fveq2i 6720 |
. . . . . . 7
⊢ (𝑓‘(𝐵 ∩ 𝐴)) = (𝑓‘(𝐴 ∩ 𝐵)) |
51 | 50 | oveq2i 7224 |
. . . . . 6
⊢ ((𝑓‘(⊥‘𝐵)) + (𝑓‘(𝐵 ∩ 𝐴))) = ((𝑓‘(⊥‘𝐵)) + (𝑓‘(𝐴 ∩ 𝐵))) |
52 | 48, 51 | eqtrdi 2794 |
. . . . 5
⊢ (𝑓 ∈ States → (𝑓‘((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐴))) = ((𝑓‘(⊥‘𝐵)) + (𝑓‘(𝐴 ∩ 𝐵)))) |
53 | 11, 6 | stji1i 30323 |
. . . . . 6
⊢ (𝑓 ∈ States → (𝑓‘((⊥‘𝐶) ∨ℋ (𝐶 ∩ 𝐵))) = ((𝑓‘(⊥‘𝐶)) + (𝑓‘(𝐶 ∩ 𝐵)))) |
54 | | incom 4115 |
. . . . . . . 8
⊢ (𝐶 ∩ 𝐵) = (𝐵 ∩ 𝐶) |
55 | 54 | fveq2i 6720 |
. . . . . . 7
⊢ (𝑓‘(𝐶 ∩ 𝐵)) = (𝑓‘(𝐵 ∩ 𝐶)) |
56 | 55 | oveq2i 7224 |
. . . . . 6
⊢ ((𝑓‘(⊥‘𝐶)) + (𝑓‘(𝐶 ∩ 𝐵))) = ((𝑓‘(⊥‘𝐶)) + (𝑓‘(𝐵 ∩ 𝐶))) |
57 | 53, 56 | eqtrdi 2794 |
. . . . 5
⊢ (𝑓 ∈ States → (𝑓‘((⊥‘𝐶) ∨ℋ (𝐶 ∩ 𝐵))) = ((𝑓‘(⊥‘𝐶)) + (𝑓‘(𝐵 ∩ 𝐶)))) |
58 | 52, 57 | oveq12d 7231 |
. . . 4
⊢ (𝑓 ∈ States → ((𝑓‘((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐴))) + (𝑓‘((⊥‘𝐶) ∨ℋ (𝐶 ∩ 𝐵)))) = (((𝑓‘(⊥‘𝐵)) + (𝑓‘(𝐴 ∩ 𝐵))) + ((𝑓‘(⊥‘𝐶)) + (𝑓‘(𝐵 ∩ 𝐶))))) |
59 | 1, 11 | stji1i 30323 |
. . . . 5
⊢ (𝑓 ∈ States → (𝑓‘((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐶))) = ((𝑓‘(⊥‘𝐴)) + (𝑓‘(𝐴 ∩ 𝐶)))) |
60 | | incom 4115 |
. . . . . . 7
⊢ (𝐴 ∩ 𝐶) = (𝐶 ∩ 𝐴) |
61 | 60 | fveq2i 6720 |
. . . . . 6
⊢ (𝑓‘(𝐴 ∩ 𝐶)) = (𝑓‘(𝐶 ∩ 𝐴)) |
62 | 61 | oveq2i 7224 |
. . . . 5
⊢ ((𝑓‘(⊥‘𝐴)) + (𝑓‘(𝐴 ∩ 𝐶))) = ((𝑓‘(⊥‘𝐴)) + (𝑓‘(𝐶 ∩ 𝐴))) |
63 | 59, 62 | eqtrdi 2794 |
. . . 4
⊢ (𝑓 ∈ States → (𝑓‘((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐶))) = ((𝑓‘(⊥‘𝐴)) + (𝑓‘(𝐶 ∩ 𝐴)))) |
64 | 58, 63 | oveq12d 7231 |
. . 3
⊢ (𝑓 ∈ States → (((𝑓‘((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐴))) + (𝑓‘((⊥‘𝐶) ∨ℋ (𝐶 ∩ 𝐵)))) + (𝑓‘((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐶)))) = ((((𝑓‘(⊥‘𝐵)) + (𝑓‘(𝐴 ∩ 𝐵))) + ((𝑓‘(⊥‘𝐶)) + (𝑓‘(𝐵 ∩ 𝐶)))) + ((𝑓‘(⊥‘𝐴)) + (𝑓‘(𝐶 ∩ 𝐴))))) |
65 | 42, 47, 64 | 3eqtr4d 2787 |
. 2
⊢ (𝑓 ∈ States → (((𝑓‘((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐵))) + (𝑓‘((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐶)))) + (𝑓‘((⊥‘𝐶) ∨ℋ (𝐶 ∩ 𝐴)))) = (((𝑓‘((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐴))) + (𝑓‘((⊥‘𝐶) ∨ℋ (𝐶 ∩ 𝐵)))) + (𝑓‘((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐶))))) |
66 | | golem1.4 |
. . . . 5
⊢ 𝐹 = ((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐵)) |
67 | 66 | fveq2i 6720 |
. . . 4
⊢ (𝑓‘𝐹) = (𝑓‘((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐵))) |
68 | | golem1.5 |
. . . . 5
⊢ 𝐺 = ((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐶)) |
69 | 68 | fveq2i 6720 |
. . . 4
⊢ (𝑓‘𝐺) = (𝑓‘((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐶))) |
70 | 67, 69 | oveq12i 7225 |
. . 3
⊢ ((𝑓‘𝐹) + (𝑓‘𝐺)) = ((𝑓‘((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐵))) + (𝑓‘((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐶)))) |
71 | | golem1.6 |
. . . 4
⊢ 𝐻 = ((⊥‘𝐶) ∨ℋ (𝐶 ∩ 𝐴)) |
72 | 71 | fveq2i 6720 |
. . 3
⊢ (𝑓‘𝐻) = (𝑓‘((⊥‘𝐶) ∨ℋ (𝐶 ∩ 𝐴))) |
73 | 70, 72 | oveq12i 7225 |
. 2
⊢ (((𝑓‘𝐹) + (𝑓‘𝐺)) + (𝑓‘𝐻)) = (((𝑓‘((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐵))) + (𝑓‘((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐶)))) + (𝑓‘((⊥‘𝐶) ∨ℋ (𝐶 ∩ 𝐴)))) |
74 | | golem1.7 |
. . . . 5
⊢ 𝐷 = ((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐴)) |
75 | 74 | fveq2i 6720 |
. . . 4
⊢ (𝑓‘𝐷) = (𝑓‘((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐴))) |
76 | | golem1.8 |
. . . . 5
⊢ 𝑅 = ((⊥‘𝐶) ∨ℋ (𝐶 ∩ 𝐵)) |
77 | 76 | fveq2i 6720 |
. . . 4
⊢ (𝑓‘𝑅) = (𝑓‘((⊥‘𝐶) ∨ℋ (𝐶 ∩ 𝐵))) |
78 | 75, 77 | oveq12i 7225 |
. . 3
⊢ ((𝑓‘𝐷) + (𝑓‘𝑅)) = ((𝑓‘((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐴))) + (𝑓‘((⊥‘𝐶) ∨ℋ (𝐶 ∩ 𝐵)))) |
79 | | golem1.9 |
. . . 4
⊢ 𝑆 = ((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐶)) |
80 | 79 | fveq2i 6720 |
. . 3
⊢ (𝑓‘𝑆) = (𝑓‘((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐶))) |
81 | 78, 80 | oveq12i 7225 |
. 2
⊢ (((𝑓‘𝐷) + (𝑓‘𝑅)) + (𝑓‘𝑆)) = (((𝑓‘((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐴))) + (𝑓‘((⊥‘𝐶) ∨ℋ (𝐶 ∩ 𝐵)))) + (𝑓‘((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐶)))) |
82 | 65, 73, 81 | 3eqtr4g 2803 |
1
⊢ (𝑓 ∈ States → (((𝑓‘𝐹) + (𝑓‘𝐺)) + (𝑓‘𝐻)) = (((𝑓‘𝐷) + (𝑓‘𝑅)) + (𝑓‘𝑆))) |