# 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 ∧ ( 𝑆 ‘ ( 𝑥 𝑦 ) ) = ( ( 𝑆𝑥 ) + ( 𝑆𝑦 ) ) ) ) ) )