Step | Hyp | Ref
| Expression |
1 | | ax-hilex 27240 |
. . . 4
⊢ ℋ
∈ V |
2 | | chex 27467 |
. . . 4
⊢
Cℋ ∈ V |
3 | 1, 2 | elmap 7772 |
. . 3
⊢ (𝑆 ∈ ( ℋ
↑𝑚 Cℋ ) ↔ 𝑆:
Cℋ ⟶ ℋ) |
4 | 3 | anbi1i 727 |
. 2
⊢ ((𝑆 ∈ ( ℋ
↑𝑚 Cℋ ) ∧
((normℎ‘(𝑆‘ ℋ)) = 1 ∧ ∀𝑥 ∈
Cℋ ∀𝑦 ∈ Cℋ
(𝑥 ⊆
(⊥‘𝑦) →
(((𝑆‘𝑥)
·ih (𝑆‘𝑦)) = 0 ∧ (𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) +ℎ (𝑆‘𝑦)))))) ↔ (𝑆: Cℋ ⟶
ℋ ∧ ((normℎ‘(𝑆‘ ℋ)) = 1 ∧ ∀𝑥 ∈
Cℋ ∀𝑦 ∈ Cℋ
(𝑥 ⊆
(⊥‘𝑦) →
(((𝑆‘𝑥)
·ih (𝑆‘𝑦)) = 0 ∧ (𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) +ℎ (𝑆‘𝑦))))))) |
5 | | fveq1 6102 |
. . . . . 6
⊢ (𝑓 = 𝑆 → (𝑓‘ ℋ) = (𝑆‘ ℋ)) |
6 | 5 | fveq2d 6107 |
. . . . 5
⊢ (𝑓 = 𝑆 →
(normℎ‘(𝑓‘ ℋ)) =
(normℎ‘(𝑆‘ ℋ))) |
7 | 6 | eqeq1d 2612 |
. . . 4
⊢ (𝑓 = 𝑆 →
((normℎ‘(𝑓‘ ℋ)) = 1 ↔
(normℎ‘(𝑆‘ ℋ)) = 1)) |
8 | | fveq1 6102 |
. . . . . . . . 9
⊢ (𝑓 = 𝑆 → (𝑓‘𝑥) = (𝑆‘𝑥)) |
9 | | fveq1 6102 |
. . . . . . . . 9
⊢ (𝑓 = 𝑆 → (𝑓‘𝑦) = (𝑆‘𝑦)) |
10 | 8, 9 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑓 = 𝑆 → ((𝑓‘𝑥) ·ih (𝑓‘𝑦)) = ((𝑆‘𝑥) ·ih (𝑆‘𝑦))) |
11 | 10 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑓 = 𝑆 → (((𝑓‘𝑥) ·ih (𝑓‘𝑦)) = 0 ↔ ((𝑆‘𝑥) ·ih (𝑆‘𝑦)) = 0)) |
12 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑓 = 𝑆 → (𝑓‘(𝑥 ∨ℋ 𝑦)) = (𝑆‘(𝑥 ∨ℋ 𝑦))) |
13 | 8, 9 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑓 = 𝑆 → ((𝑓‘𝑥) +ℎ (𝑓‘𝑦)) = ((𝑆‘𝑥) +ℎ (𝑆‘𝑦))) |
14 | 12, 13 | eqeq12d 2625 |
. . . . . . 7
⊢ (𝑓 = 𝑆 → ((𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) +ℎ (𝑓‘𝑦)) ↔ (𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) +ℎ (𝑆‘𝑦)))) |
15 | 11, 14 | anbi12d 743 |
. . . . . 6
⊢ (𝑓 = 𝑆 → ((((𝑓‘𝑥) ·ih (𝑓‘𝑦)) = 0 ∧ (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) +ℎ (𝑓‘𝑦))) ↔ (((𝑆‘𝑥) ·ih (𝑆‘𝑦)) = 0 ∧ (𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) +ℎ (𝑆‘𝑦))))) |
16 | 15 | imbi2d 329 |
. . . . 5
⊢ (𝑓 = 𝑆 → ((𝑥 ⊆ (⊥‘𝑦) → (((𝑓‘𝑥) ·ih (𝑓‘𝑦)) = 0 ∧ (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) +ℎ (𝑓‘𝑦)))) ↔ (𝑥 ⊆ (⊥‘𝑦) → (((𝑆‘𝑥) ·ih (𝑆‘𝑦)) = 0 ∧ (𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) +ℎ (𝑆‘𝑦)))))) |
17 | 16 | 2ralbidv 2972 |
. . . 4
⊢ (𝑓 = 𝑆 → (∀𝑥 ∈ Cℋ
∀𝑦 ∈
Cℋ (𝑥 ⊆ (⊥‘𝑦) → (((𝑓‘𝑥) ·ih (𝑓‘𝑦)) = 0 ∧ (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) +ℎ (𝑓‘𝑦)))) ↔ ∀𝑥 ∈ Cℋ
∀𝑦 ∈
Cℋ (𝑥 ⊆ (⊥‘𝑦) → (((𝑆‘𝑥) ·ih (𝑆‘𝑦)) = 0 ∧ (𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) +ℎ (𝑆‘𝑦)))))) |
18 | 7, 17 | anbi12d 743 |
. . 3
⊢ (𝑓 = 𝑆 →
(((normℎ‘(𝑓‘ ℋ)) = 1 ∧ ∀𝑥 ∈
Cℋ ∀𝑦 ∈ Cℋ
(𝑥 ⊆
(⊥‘𝑦) →
(((𝑓‘𝑥)
·ih (𝑓‘𝑦)) = 0 ∧ (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) +ℎ (𝑓‘𝑦))))) ↔
((normℎ‘(𝑆‘ ℋ)) = 1 ∧ ∀𝑥 ∈
Cℋ ∀𝑦 ∈ Cℋ
(𝑥 ⊆
(⊥‘𝑦) →
(((𝑆‘𝑥)
·ih (𝑆‘𝑦)) = 0 ∧ (𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) +ℎ (𝑆‘𝑦))))))) |
19 | | df-hst 28455 |
. . 3
⊢ CHStates
= {𝑓 ∈ ( ℋ
↑𝑚 Cℋ ) ∣
((normℎ‘(𝑓‘ ℋ)) = 1 ∧ ∀𝑥 ∈
Cℋ ∀𝑦 ∈ Cℋ
(𝑥 ⊆
(⊥‘𝑦) →
(((𝑓‘𝑥)
·ih (𝑓‘𝑦)) = 0 ∧ (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) +ℎ (𝑓‘𝑦)))))} |
20 | 18, 19 | elrab2 3333 |
. 2
⊢ (𝑆 ∈ CHStates ↔ (𝑆 ∈ ( ℋ
↑𝑚 Cℋ ) ∧
((normℎ‘(𝑆‘ ℋ)) = 1 ∧ ∀𝑥 ∈
Cℋ ∀𝑦 ∈ Cℋ
(𝑥 ⊆
(⊥‘𝑦) →
(((𝑆‘𝑥)
·ih (𝑆‘𝑦)) = 0 ∧ (𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) +ℎ (𝑆‘𝑦))))))) |
21 | | 3anass 1035 |
. 2
⊢ ((𝑆:
Cℋ ⟶ ℋ ∧
(normℎ‘(𝑆‘ ℋ)) = 1 ∧ ∀𝑥 ∈
Cℋ ∀𝑦 ∈ Cℋ
(𝑥 ⊆
(⊥‘𝑦) →
(((𝑆‘𝑥)
·ih (𝑆‘𝑦)) = 0 ∧ (𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) +ℎ (𝑆‘𝑦))))) ↔ (𝑆: Cℋ ⟶
ℋ ∧ ((normℎ‘(𝑆‘ ℋ)) = 1 ∧ ∀𝑥 ∈
Cℋ ∀𝑦 ∈ Cℋ
(𝑥 ⊆
(⊥‘𝑦) →
(((𝑆‘𝑥)
·ih (𝑆‘𝑦)) = 0 ∧ (𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) +ℎ (𝑆‘𝑦))))))) |
22 | 4, 20, 21 | 3bitr4i 291 |
1
⊢ (𝑆 ∈ CHStates ↔ (𝑆:
Cℋ ⟶ ℋ ∧
(normℎ‘(𝑆‘ ℋ)) = 1 ∧ ∀𝑥 ∈
Cℋ ∀𝑦 ∈ Cℋ
(𝑥 ⊆
(⊥‘𝑦) →
(((𝑆‘𝑥)
·ih (𝑆‘𝑦)) = 0 ∧ (𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) +ℎ (𝑆‘𝑦)))))) |