Step | Hyp | Ref
| Expression |
1 | | isst 29072 |
. . . 4
⊢ (𝑆 ∈ States ↔ (𝑆:
Cℋ ⟶(0[,]1) ∧ (𝑆‘ ℋ) = 1 ∧ ∀𝑥 ∈
Cℋ ∀𝑦 ∈ Cℋ
(𝑥 ⊆
(⊥‘𝑦) →
(𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) + (𝑆‘𝑦))))) |
2 | 1 | simp3bi 1078 |
. . 3
⊢ (𝑆 ∈ States →
∀𝑥 ∈
Cℋ ∀𝑦 ∈ Cℋ
(𝑥 ⊆
(⊥‘𝑦) →
(𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) + (𝑆‘𝑦)))) |
3 | | sseq1 3626 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝑥 ⊆ (⊥‘𝑦) ↔ 𝐴 ⊆ (⊥‘𝑦))) |
4 | | oveq1 6657 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑥 ∨ℋ 𝑦) = (𝐴 ∨ℋ 𝑦)) |
5 | 4 | fveq2d 6195 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝑆‘(𝑥 ∨ℋ 𝑦)) = (𝑆‘(𝐴 ∨ℋ 𝑦))) |
6 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑆‘𝑥) = (𝑆‘𝐴)) |
7 | 6 | oveq1d 6665 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((𝑆‘𝑥) + (𝑆‘𝑦)) = ((𝑆‘𝐴) + (𝑆‘𝑦))) |
8 | 5, 7 | eqeq12d 2637 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) + (𝑆‘𝑦)) ↔ (𝑆‘(𝐴 ∨ℋ 𝑦)) = ((𝑆‘𝐴) + (𝑆‘𝑦)))) |
9 | 3, 8 | imbi12d 334 |
. . . 4
⊢ (𝑥 = 𝐴 → ((𝑥 ⊆ (⊥‘𝑦) → (𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) + (𝑆‘𝑦))) ↔ (𝐴 ⊆ (⊥‘𝑦) → (𝑆‘(𝐴 ∨ℋ 𝑦)) = ((𝑆‘𝐴) + (𝑆‘𝑦))))) |
10 | | fveq2 6191 |
. . . . . 6
⊢ (𝑦 = 𝐵 → (⊥‘𝑦) = (⊥‘𝐵)) |
11 | 10 | sseq2d 3633 |
. . . . 5
⊢ (𝑦 = 𝐵 → (𝐴 ⊆ (⊥‘𝑦) ↔ 𝐴 ⊆ (⊥‘𝐵))) |
12 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (𝐴 ∨ℋ 𝑦) = (𝐴 ∨ℋ 𝐵)) |
13 | 12 | fveq2d 6195 |
. . . . . 6
⊢ (𝑦 = 𝐵 → (𝑆‘(𝐴 ∨ℋ 𝑦)) = (𝑆‘(𝐴 ∨ℋ 𝐵))) |
14 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (𝑆‘𝑦) = (𝑆‘𝐵)) |
15 | 14 | oveq2d 6666 |
. . . . . 6
⊢ (𝑦 = 𝐵 → ((𝑆‘𝐴) + (𝑆‘𝑦)) = ((𝑆‘𝐴) + (𝑆‘𝐵))) |
16 | 13, 15 | eqeq12d 2637 |
. . . . 5
⊢ (𝑦 = 𝐵 → ((𝑆‘(𝐴 ∨ℋ 𝑦)) = ((𝑆‘𝐴) + (𝑆‘𝑦)) ↔ (𝑆‘(𝐴 ∨ℋ 𝐵)) = ((𝑆‘𝐴) + (𝑆‘𝐵)))) |
17 | 11, 16 | imbi12d 334 |
. . . 4
⊢ (𝑦 = 𝐵 → ((𝐴 ⊆ (⊥‘𝑦) → (𝑆‘(𝐴 ∨ℋ 𝑦)) = ((𝑆‘𝐴) + (𝑆‘𝑦))) ↔ (𝐴 ⊆ (⊥‘𝐵) → (𝑆‘(𝐴 ∨ℋ 𝐵)) = ((𝑆‘𝐴) + (𝑆‘𝐵))))) |
18 | 9, 17 | rspc2v 3322 |
. . 3
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (∀𝑥 ∈
Cℋ ∀𝑦 ∈ Cℋ
(𝑥 ⊆
(⊥‘𝑦) →
(𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) + (𝑆‘𝑦))) → (𝐴 ⊆ (⊥‘𝐵) → (𝑆‘(𝐴 ∨ℋ 𝐵)) = ((𝑆‘𝐴) + (𝑆‘𝐵))))) |
19 | 2, 18 | syl5com 31 |
. 2
⊢ (𝑆 ∈ States → ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝐴 ⊆
(⊥‘𝐵) →
(𝑆‘(𝐴 ∨ℋ 𝐵)) = ((𝑆‘𝐴) + (𝑆‘𝐵))))) |
20 | 19 | impd 447 |
1
⊢ (𝑆 ∈ States → (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ 𝐴 ⊆
(⊥‘𝐵)) →
(𝑆‘(𝐴 ∨ℋ 𝐵)) = ((𝑆‘𝐴) + (𝑆‘𝐵)))) |