Step | Hyp | Ref
| Expression |
1 | | ishst 30295 |
. . . 4
⊢ (𝑆 ∈ CHStates ↔ (𝑆:
Cℋ ⟶ ℋ ∧
(normℎ‘(𝑆‘ ℋ)) = 1 ∧ ∀𝑥 ∈
Cℋ ∀𝑦 ∈ Cℋ
(𝑥 ⊆
(⊥‘𝑦) →
(((𝑆‘𝑥)
·ih (𝑆‘𝑦)) = 0 ∧ (𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) +ℎ (𝑆‘𝑦)))))) |
2 | 1 | simp3bi 1149 |
. . 3
⊢ (𝑆 ∈ CHStates →
∀𝑥 ∈
Cℋ ∀𝑦 ∈ Cℋ
(𝑥 ⊆
(⊥‘𝑦) →
(((𝑆‘𝑥)
·ih (𝑆‘𝑦)) = 0 ∧ (𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) +ℎ (𝑆‘𝑦))))) |
3 | 2 | ad2antrr 726 |
. 2
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ (𝐵 ∈ Cℋ
∧ 𝐴 ⊆
(⊥‘𝐵))) →
∀𝑥 ∈
Cℋ ∀𝑦 ∈ Cℋ
(𝑥 ⊆
(⊥‘𝑦) →
(((𝑆‘𝑥)
·ih (𝑆‘𝑦)) = 0 ∧ (𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) +ℎ (𝑆‘𝑦))))) |
4 | | sseq1 3926 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑥 ⊆ (⊥‘𝑦) ↔ 𝐴 ⊆ (⊥‘𝑦))) |
5 | | fveq2 6717 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (𝑆‘𝑥) = (𝑆‘𝐴)) |
6 | 5 | oveq1d 7228 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → ((𝑆‘𝑥) ·ih (𝑆‘𝑦)) = ((𝑆‘𝐴) ·ih (𝑆‘𝑦))) |
7 | 6 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (((𝑆‘𝑥) ·ih (𝑆‘𝑦)) = 0 ↔ ((𝑆‘𝐴) ·ih (𝑆‘𝑦)) = 0)) |
8 | | fvoveq1 7236 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → (𝑆‘(𝑥 ∨ℋ 𝑦)) = (𝑆‘(𝐴 ∨ℋ 𝑦))) |
9 | 5 | oveq1d 7228 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → ((𝑆‘𝑥) +ℎ (𝑆‘𝑦)) = ((𝑆‘𝐴) +ℎ (𝑆‘𝑦))) |
10 | 8, 9 | eqeq12d 2753 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → ((𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) +ℎ (𝑆‘𝑦)) ↔ (𝑆‘(𝐴 ∨ℋ 𝑦)) = ((𝑆‘𝐴) +ℎ (𝑆‘𝑦)))) |
11 | 7, 10 | anbi12d 634 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → ((((𝑆‘𝑥) ·ih (𝑆‘𝑦)) = 0 ∧ (𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) +ℎ (𝑆‘𝑦))) ↔ (((𝑆‘𝐴) ·ih (𝑆‘𝑦)) = 0 ∧ (𝑆‘(𝐴 ∨ℋ 𝑦)) = ((𝑆‘𝐴) +ℎ (𝑆‘𝑦))))) |
12 | 4, 11 | imbi12d 348 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((𝑥 ⊆ (⊥‘𝑦) → (((𝑆‘𝑥) ·ih (𝑆‘𝑦)) = 0 ∧ (𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) +ℎ (𝑆‘𝑦)))) ↔ (𝐴 ⊆ (⊥‘𝑦) → (((𝑆‘𝐴) ·ih (𝑆‘𝑦)) = 0 ∧ (𝑆‘(𝐴 ∨ℋ 𝑦)) = ((𝑆‘𝐴) +ℎ (𝑆‘𝑦)))))) |
13 | | fveq2 6717 |
. . . . . . . 8
⊢ (𝑦 = 𝐵 → (⊥‘𝑦) = (⊥‘𝐵)) |
14 | 13 | sseq2d 3933 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (𝐴 ⊆ (⊥‘𝑦) ↔ 𝐴 ⊆ (⊥‘𝐵))) |
15 | | fveq2 6717 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐵 → (𝑆‘𝑦) = (𝑆‘𝐵)) |
16 | 15 | oveq2d 7229 |
. . . . . . . . 9
⊢ (𝑦 = 𝐵 → ((𝑆‘𝐴) ·ih (𝑆‘𝑦)) = ((𝑆‘𝐴) ·ih (𝑆‘𝐵))) |
17 | 16 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑦 = 𝐵 → (((𝑆‘𝐴) ·ih (𝑆‘𝑦)) = 0 ↔ ((𝑆‘𝐴) ·ih (𝑆‘𝐵)) = 0)) |
18 | | oveq2 7221 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐵 → (𝐴 ∨ℋ 𝑦) = (𝐴 ∨ℋ 𝐵)) |
19 | 18 | fveq2d 6721 |
. . . . . . . . 9
⊢ (𝑦 = 𝐵 → (𝑆‘(𝐴 ∨ℋ 𝑦)) = (𝑆‘(𝐴 ∨ℋ 𝐵))) |
20 | 15 | oveq2d 7229 |
. . . . . . . . 9
⊢ (𝑦 = 𝐵 → ((𝑆‘𝐴) +ℎ (𝑆‘𝑦)) = ((𝑆‘𝐴) +ℎ (𝑆‘𝐵))) |
21 | 19, 20 | eqeq12d 2753 |
. . . . . . . 8
⊢ (𝑦 = 𝐵 → ((𝑆‘(𝐴 ∨ℋ 𝑦)) = ((𝑆‘𝐴) +ℎ (𝑆‘𝑦)) ↔ (𝑆‘(𝐴 ∨ℋ 𝐵)) = ((𝑆‘𝐴) +ℎ (𝑆‘𝐵)))) |
22 | 17, 21 | anbi12d 634 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → ((((𝑆‘𝐴) ·ih (𝑆‘𝑦)) = 0 ∧ (𝑆‘(𝐴 ∨ℋ 𝑦)) = ((𝑆‘𝐴) +ℎ (𝑆‘𝑦))) ↔ (((𝑆‘𝐴) ·ih (𝑆‘𝐵)) = 0 ∧ (𝑆‘(𝐴 ∨ℋ 𝐵)) = ((𝑆‘𝐴) +ℎ (𝑆‘𝐵))))) |
23 | 14, 22 | imbi12d 348 |
. . . . . 6
⊢ (𝑦 = 𝐵 → ((𝐴 ⊆ (⊥‘𝑦) → (((𝑆‘𝐴) ·ih (𝑆‘𝑦)) = 0 ∧ (𝑆‘(𝐴 ∨ℋ 𝑦)) = ((𝑆‘𝐴) +ℎ (𝑆‘𝑦)))) ↔ (𝐴 ⊆ (⊥‘𝐵) → (((𝑆‘𝐴) ·ih (𝑆‘𝐵)) = 0 ∧ (𝑆‘(𝐴 ∨ℋ 𝐵)) = ((𝑆‘𝐴) +ℎ (𝑆‘𝐵)))))) |
24 | 12, 23 | rspc2v 3547 |
. . . . 5
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (∀𝑥 ∈
Cℋ ∀𝑦 ∈ Cℋ
(𝑥 ⊆
(⊥‘𝑦) →
(((𝑆‘𝑥)
·ih (𝑆‘𝑦)) = 0 ∧ (𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) +ℎ (𝑆‘𝑦)))) → (𝐴 ⊆ (⊥‘𝐵) → (((𝑆‘𝐴) ·ih (𝑆‘𝐵)) = 0 ∧ (𝑆‘(𝐴 ∨ℋ 𝐵)) = ((𝑆‘𝐴) +ℎ (𝑆‘𝐵)))))) |
25 | 24 | com23 86 |
. . . 4
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝐴 ⊆
(⊥‘𝐵) →
(∀𝑥 ∈
Cℋ ∀𝑦 ∈ Cℋ
(𝑥 ⊆
(⊥‘𝑦) →
(((𝑆‘𝑥)
·ih (𝑆‘𝑦)) = 0 ∧ (𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) +ℎ (𝑆‘𝑦)))) → (((𝑆‘𝐴) ·ih (𝑆‘𝐵)) = 0 ∧ (𝑆‘(𝐴 ∨ℋ 𝐵)) = ((𝑆‘𝐴) +ℎ (𝑆‘𝐵)))))) |
26 | 25 | impr 458 |
. . 3
⊢ ((𝐴 ∈
Cℋ ∧ (𝐵 ∈ Cℋ
∧ 𝐴 ⊆
(⊥‘𝐵))) →
(∀𝑥 ∈
Cℋ ∀𝑦 ∈ Cℋ
(𝑥 ⊆
(⊥‘𝑦) →
(((𝑆‘𝑥)
·ih (𝑆‘𝑦)) = 0 ∧ (𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) +ℎ (𝑆‘𝑦)))) → (((𝑆‘𝐴) ·ih (𝑆‘𝐵)) = 0 ∧ (𝑆‘(𝐴 ∨ℋ 𝐵)) = ((𝑆‘𝐴) +ℎ (𝑆‘𝐵))))) |
27 | 26 | adantll 714 |
. 2
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ (𝐵 ∈ Cℋ
∧ 𝐴 ⊆
(⊥‘𝐵))) →
(∀𝑥 ∈
Cℋ ∀𝑦 ∈ Cℋ
(𝑥 ⊆
(⊥‘𝑦) →
(((𝑆‘𝑥)
·ih (𝑆‘𝑦)) = 0 ∧ (𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) +ℎ (𝑆‘𝑦)))) → (((𝑆‘𝐴) ·ih (𝑆‘𝐵)) = 0 ∧ (𝑆‘(𝐴 ∨ℋ 𝐵)) = ((𝑆‘𝐴) +ℎ (𝑆‘𝐵))))) |
28 | 3, 27 | mpd 15 |
1
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ (𝐵 ∈ Cℋ
∧ 𝐴 ⊆
(⊥‘𝐵))) →
(((𝑆‘𝐴)
·ih (𝑆‘𝐵)) = 0 ∧ (𝑆‘(𝐴 ∨ℋ 𝐵)) = ((𝑆‘𝐴) +ℎ (𝑆‘𝐵)))) |