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