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 ) → 𝐴𝐵 )