Metamath Proof Explorer

Theorem hstri

Description: Hilbert space admits a strong set of Hilbert-space-valued states (CH-states). Theorem in Mayet3 p. 10. (Contributed by NM, 30-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypotheses hstr.1 ⊢ 𝐴 ∈ Cℋ
hstr.2 ⊢ 𝐵 ∈ Cℋ
Assertion hstri ( ∀ 𝑓 ∈ CHStates ( ( normℎ ‘ ( 𝑓 ‘ 𝐴 ) ) = 1 → ( normℎ ‘ ( 𝑓 ‘ 𝐵 ) ) = 1 ) → 𝐴 ⊆ 𝐵 )

Proof

Step Hyp Ref Expression
1 hstr.1 ⊢ 𝐴 ∈ Cℋ
2 hstr.2 ⊢ 𝐵 ∈ Cℋ
3 dfral2 ⊢ ( ∀ 𝑓 ∈ CHStates ( ( normℎ ‘ ( 𝑓 ‘ 𝐴 ) ) = 1 → ( normℎ ‘ ( 𝑓 ‘ 𝐵 ) ) = 1 ) ↔ ¬ ∃ 𝑓 ∈ CHStates ¬ ( ( normℎ ‘ ( 𝑓 ‘ 𝐴 ) ) = 1 → ( normℎ ‘ ( 𝑓 ‘ 𝐵 ) ) = 1 ) )
4 1 2 strlem1 ⊢ ( ¬ 𝐴 ⊆ 𝐵 → ∃ 𝑢 ∈ ( 𝐴 ∖ 𝐵 ) ( normℎ ‘ 𝑢 ) = 1 )
5 eqid ⊢ ( 𝑥 ∈ Cℋ ↦ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) = ( 𝑥 ∈ Cℋ ↦ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) )
6 biid ⊢ ( ( 𝑢 ∈ ( 𝐴 ∖ 𝐵 ) ∧ ( normℎ ‘ 𝑢 ) = 1 ) ↔ ( 𝑢 ∈ ( 𝐴 ∖ 𝐵 ) ∧ ( normℎ ‘ 𝑢 ) = 1 ) )
7 5 6 1 2 hstrlem3 ⊢ ( ( 𝑢 ∈ ( 𝐴 ∖ 𝐵 ) ∧ ( normℎ ‘ 𝑢 ) = 1 ) → ( 𝑥 ∈ Cℋ ↦ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ∈ CHStates )
8 5 6 1 2 hstrlem6 ⊢ ( ( 𝑢 ∈ ( 𝐴 ∖ 𝐵 ) ∧ ( normℎ ‘ 𝑢 ) = 1 ) → ¬ ( ( normℎ ‘ ( ( 𝑥 ∈ Cℋ ↦ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ‘ 𝐴 ) ) = 1 → ( normℎ ‘ ( ( 𝑥 ∈ Cℋ ↦ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ‘ 𝐵 ) ) = 1 ) )
9 fveq1 ⊢ ( 𝑓 = ( 𝑥 ∈ Cℋ ↦ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) → ( 𝑓 ‘ 𝐴 ) = ( ( 𝑥 ∈ Cℋ ↦ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ‘ 𝐴 ) )
10 9 fveqeq2d ⊢ ( 𝑓 = ( 𝑥 ∈ Cℋ ↦ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) → ( ( normℎ ‘ ( 𝑓 ‘ 𝐴 ) ) = 1 ↔ ( normℎ ‘ ( ( 𝑥 ∈ Cℋ ↦ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ‘ 𝐴 ) ) = 1 ) )
11 fveq1 ⊢ ( 𝑓 = ( 𝑥 ∈ Cℋ ↦ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) → ( 𝑓 ‘ 𝐵 ) = ( ( 𝑥 ∈ Cℋ ↦ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ‘ 𝐵 ) )
12 11 fveqeq2d ⊢ ( 𝑓 = ( 𝑥 ∈ Cℋ ↦ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) → ( ( normℎ ‘ ( 𝑓 ‘ 𝐵 ) ) = 1 ↔ ( normℎ ‘ ( ( 𝑥 ∈ Cℋ ↦ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ‘ 𝐵 ) ) = 1 ) )
13 10 12 imbi12d ⊢ ( 𝑓 = ( 𝑥 ∈ Cℋ ↦ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) → ( ( ( normℎ ‘ ( 𝑓 ‘ 𝐴 ) ) = 1 → ( normℎ ‘ ( 𝑓 ‘ 𝐵 ) ) = 1 ) ↔ ( ( normℎ ‘ ( ( 𝑥 ∈ Cℋ ↦ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ‘ 𝐴 ) ) = 1 → ( normℎ ‘ ( ( 𝑥 ∈ Cℋ ↦ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ‘ 𝐵 ) ) = 1 ) ) )
14 13 notbid ⊢ ( 𝑓 = ( 𝑥 ∈ Cℋ ↦ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) → ( ¬ ( ( normℎ ‘ ( 𝑓 ‘ 𝐴 ) ) = 1 → ( normℎ ‘ ( 𝑓 ‘ 𝐵 ) ) = 1 ) ↔ ¬ ( ( normℎ ‘ ( ( 𝑥 ∈ Cℋ ↦ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ‘ 𝐴 ) ) = 1 → ( normℎ ‘ ( ( 𝑥 ∈ Cℋ ↦ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ‘ 𝐵 ) ) = 1 ) ) )
15 14 rspcev ⊢ ( ( ( 𝑥 ∈ Cℋ ↦ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ∈ CHStates ∧ ¬ ( ( normℎ ‘ ( ( 𝑥 ∈ Cℋ ↦ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ‘ 𝐴 ) ) = 1 → ( normℎ ‘ ( ( 𝑥 ∈ Cℋ ↦ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ‘ 𝐵 ) ) = 1 ) ) → ∃ 𝑓 ∈ CHStates ¬ ( ( normℎ ‘ ( 𝑓 ‘ 𝐴 ) ) = 1 → ( normℎ ‘ ( 𝑓 ‘ 𝐵 ) ) = 1 ) )
16 7 8 15 syl2anc ⊢ ( ( 𝑢 ∈ ( 𝐴 ∖ 𝐵 ) ∧ ( normℎ ‘ 𝑢 ) = 1 ) → ∃ 𝑓 ∈ CHStates ¬ ( ( normℎ ‘ ( 𝑓 ‘ 𝐴 ) ) = 1 → ( normℎ ‘ ( 𝑓 ‘ 𝐵 ) ) = 1 ) )
17 16 rexlimiva ⊢ ( ∃ 𝑢 ∈ ( 𝐴 ∖ 𝐵 ) ( normℎ ‘ 𝑢 ) = 1 → ∃ 𝑓 ∈ CHStates ¬ ( ( normℎ ‘ ( 𝑓 ‘ 𝐴 ) ) = 1 → ( normℎ ‘ ( 𝑓 ‘ 𝐵 ) ) = 1 ) )
18 4 17 syl ⊢ ( ¬ 𝐴 ⊆ 𝐵 → ∃ 𝑓 ∈ CHStates ¬ ( ( normℎ ‘ ( 𝑓 ‘ 𝐴 ) ) = 1 → ( normℎ ‘ ( 𝑓 ‘ 𝐵 ) ) = 1 ) )
19 18 con1i ⊢ ( ¬ ∃ 𝑓 ∈ CHStates ¬ ( ( normℎ ‘ ( 𝑓 ‘ 𝐴 ) ) = 1 → ( normℎ ‘ ( 𝑓 ‘ 𝐵 ) ) = 1 ) → 𝐴 ⊆ 𝐵 )
20 3 19 sylbi ⊢ ( ∀ 𝑓 ∈ CHStates ( ( normℎ ‘ ( 𝑓 ‘ 𝐴 ) ) = 1 → ( normℎ ‘ ( 𝑓 ‘ 𝐵 ) ) = 1 ) → 𝐴 ⊆ 𝐵 )