Metamath Proof Explorer

Theorem ishst

Description: Property of a complex Hilbert-space-valued state. Definition of CH-states in Mayet3 p. 9. (Contributed by NM, 25-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion ishst ( 𝑆 ∈ CHStates ↔ ( 𝑆 : Cℋ ⟶ ℋ ∧ ( normℎ ‘ ( 𝑆 ‘ ℋ ) ) = 1 ∧ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( ( ( 𝑆 ‘ 𝑥 ) ·ih ( 𝑆 ‘ 𝑦 ) ) = 0 ∧ ( 𝑆 ‘ ( 𝑥 ∨ℋ 𝑦 ) ) = ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑆 ‘ 𝑦 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ax-hilex ⊢ ℋ ∈ V
2 chex ⊢ Cℋ ∈ V
3 1 2 elmap ⊢ ( 𝑆 ∈ ( ℋ ↑m Cℋ ) ↔ 𝑆 : Cℋ ⟶ ℋ )
4 3 anbi1i ⊢ ( ( 𝑆 ∈ ( ℋ ↑m Cℋ ) ∧ ( ( normℎ ‘ ( 𝑆 ‘ ℋ ) ) = 1 ∧ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( ( ( 𝑆 ‘ 𝑥 ) ·ih ( 𝑆 ‘ 𝑦 ) ) = 0 ∧ ( 𝑆 ‘ ( 𝑥 ∨ℋ 𝑦 ) ) = ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑆 ‘ 𝑦 ) ) ) ) ) ) ↔ ( 𝑆 : Cℋ ⟶ ℋ ∧ ( ( normℎ ‘ ( 𝑆 ‘ ℋ ) ) = 1 ∧ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( ( ( 𝑆 ‘ 𝑥 ) ·ih ( 𝑆 ‘ 𝑦 ) ) = 0 ∧ ( 𝑆 ‘ ( 𝑥 ∨ℋ 𝑦 ) ) = ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑆 ‘ 𝑦 ) ) ) ) ) ) )
5 fveq1 ⊢ ( 𝑓 = 𝑆 → ( 𝑓 ‘ ℋ ) = ( 𝑆 ‘ ℋ ) )
6 5 fveqeq2d ⊢ ( 𝑓 = 𝑆 → ( ( normℎ ‘ ( 𝑓 ‘ ℋ ) ) = 1 ↔ ( normℎ ‘ ( 𝑆 ‘ ℋ ) ) = 1 ) )
7 fveq1 ⊢ ( 𝑓 = 𝑆 → ( 𝑓 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
8 fveq1 ⊢ ( 𝑓 = 𝑆 → ( 𝑓 ‘ 𝑦 ) = ( 𝑆 ‘ 𝑦 ) )
9 7 8 oveq12d ⊢ ( 𝑓 = 𝑆 → ( ( 𝑓 ‘ 𝑥 ) ·ih ( 𝑓 ‘ 𝑦 ) ) = ( ( 𝑆 ‘ 𝑥 ) ·ih ( 𝑆 ‘ 𝑦 ) ) )
10 9 eqeq1d ⊢ ( 𝑓 = 𝑆 → ( ( ( 𝑓 ‘ 𝑥 ) ·ih ( 𝑓 ‘ 𝑦 ) ) = 0 ↔ ( ( 𝑆 ‘ 𝑥 ) ·ih ( 𝑆 ‘ 𝑦 ) ) = 0 ) )
11 fveq1 ⊢ ( 𝑓 = 𝑆 → ( 𝑓 ‘ ( 𝑥 ∨ℋ 𝑦 ) ) = ( 𝑆 ‘ ( 𝑥 ∨ℋ 𝑦 ) ) )
12 7 8 oveq12d ⊢ ( 𝑓 = 𝑆 → ( ( 𝑓 ‘ 𝑥 ) +ℎ ( 𝑓 ‘ 𝑦 ) ) = ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑆 ‘ 𝑦 ) ) )
13 11 12 eqeq12d ⊢ ( 𝑓 = 𝑆 → ( ( 𝑓 ‘ ( 𝑥 ∨ℋ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) +ℎ ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑆 ‘ ( 𝑥 ∨ℋ 𝑦 ) ) = ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑆 ‘ 𝑦 ) ) ) )
14 10 13 anbi12d ⊢ ( 𝑓 = 𝑆 → ( ( ( ( 𝑓 ‘ 𝑥 ) ·ih ( 𝑓 ‘ 𝑦 ) ) = 0 ∧ ( 𝑓 ‘ ( 𝑥 ∨ℋ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) +ℎ ( 𝑓 ‘ 𝑦 ) ) ) ↔ ( ( ( 𝑆 ‘ 𝑥 ) ·ih ( 𝑆 ‘ 𝑦 ) ) = 0 ∧ ( 𝑆 ‘ ( 𝑥 ∨ℋ 𝑦 ) ) = ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑆 ‘ 𝑦 ) ) ) ) )
15 14 imbi2d ⊢ ( 𝑓 = 𝑆 → ( ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( ( ( 𝑓 ‘ 𝑥 ) ·ih ( 𝑓 ‘ 𝑦 ) ) = 0 ∧ ( 𝑓 ‘ ( 𝑥 ∨ℋ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) +ℎ ( 𝑓 ‘ 𝑦 ) ) ) ) ↔ ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( ( ( 𝑆 ‘ 𝑥 ) ·ih ( 𝑆 ‘ 𝑦 ) ) = 0 ∧ ( 𝑆 ‘ ( 𝑥 ∨ℋ 𝑦 ) ) = ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑆 ‘ 𝑦 ) ) ) ) ) )
16 15 2ralbidv ⊢ ( 𝑓 = 𝑆 → ( ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( ( ( 𝑓 ‘ 𝑥 ) ·ih ( 𝑓 ‘ 𝑦 ) ) = 0 ∧ ( 𝑓 ‘ ( 𝑥 ∨ℋ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) +ℎ ( 𝑓 ‘ 𝑦 ) ) ) ) ↔ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( ( ( 𝑆 ‘ 𝑥 ) ·ih ( 𝑆 ‘ 𝑦 ) ) = 0 ∧ ( 𝑆 ‘ ( 𝑥 ∨ℋ 𝑦 ) ) = ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑆 ‘ 𝑦 ) ) ) ) ) )
17 6 16 anbi12d ⊢ ( 𝑓 = 𝑆 → ( ( ( normℎ ‘ ( 𝑓 ‘ ℋ ) ) = 1 ∧ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( ( ( 𝑓 ‘ 𝑥 ) ·ih ( 𝑓 ‘ 𝑦 ) ) = 0 ∧ ( 𝑓 ‘ ( 𝑥 ∨ℋ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) +ℎ ( 𝑓 ‘ 𝑦 ) ) ) ) ) ↔ ( ( normℎ ‘ ( 𝑆 ‘ ℋ ) ) = 1 ∧ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( ( ( 𝑆 ‘ 𝑥 ) ·ih ( 𝑆 ‘ 𝑦 ) ) = 0 ∧ ( 𝑆 ‘ ( 𝑥 ∨ℋ 𝑦 ) ) = ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑆 ‘ 𝑦 ) ) ) ) ) ) )
18 df-hst ⊢ CHStates = { 𝑓 ∈ ( ℋ ↑m Cℋ ) ∣ ( ( normℎ ‘ ( 𝑓 ‘ ℋ ) ) = 1 ∧ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( ( ( 𝑓 ‘ 𝑥 ) ·ih ( 𝑓 ‘ 𝑦 ) ) = 0 ∧ ( 𝑓 ‘ ( 𝑥 ∨ℋ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) +ℎ ( 𝑓 ‘ 𝑦 ) ) ) ) ) }
19 17 18 elrab2 ⊢ ( 𝑆 ∈ CHStates ↔ ( 𝑆 ∈ ( ℋ ↑m Cℋ ) ∧ ( ( normℎ ‘ ( 𝑆 ‘ ℋ ) ) = 1 ∧ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( ( ( 𝑆 ‘ 𝑥 ) ·ih ( 𝑆 ‘ 𝑦 ) ) = 0 ∧ ( 𝑆 ‘ ( 𝑥 ∨ℋ 𝑦 ) ) = ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑆 ‘ 𝑦 ) ) ) ) ) ) )
20 3anass ⊢ ( ( 𝑆 : Cℋ ⟶ ℋ ∧ ( normℎ ‘ ( 𝑆 ‘ ℋ ) ) = 1 ∧ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( ( ( 𝑆 ‘ 𝑥 ) ·ih ( 𝑆 ‘ 𝑦 ) ) = 0 ∧ ( 𝑆 ‘ ( 𝑥 ∨ℋ 𝑦 ) ) = ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑆 ‘ 𝑦 ) ) ) ) ) ↔ ( 𝑆 : Cℋ ⟶ ℋ ∧ ( ( normℎ ‘ ( 𝑆 ‘ ℋ ) ) = 1 ∧ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( ( ( 𝑆 ‘ 𝑥 ) ·ih ( 𝑆 ‘ 𝑦 ) ) = 0 ∧ ( 𝑆 ‘ ( 𝑥 ∨ℋ 𝑦 ) ) = ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑆 ‘ 𝑦 ) ) ) ) ) ) )
21 4 19 20 3bitr4i ⊢ ( 𝑆 ∈ CHStates ↔ ( 𝑆 : Cℋ ⟶ ℋ ∧ ( normℎ ‘ ( 𝑆 ‘ ℋ ) ) = 1 ∧ ∀ 𝑥 ∈ Cℋ ∀ 𝑦 ∈ Cℋ ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( ( ( 𝑆 ‘ 𝑥 ) ·ih ( 𝑆 ‘ 𝑦 ) ) = 0 ∧ ( 𝑆 ‘ ( 𝑥 ∨ℋ 𝑦 ) ) = ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑆 ‘ 𝑦 ) ) ) ) ) )