Metamath Proof Explorer

Theorem stri

Description: Strong state theorem. The states on a Hilbert lattice define an ordering. Remark in Mayet p. 370. (Contributed by NM, 2-Nov-1999) (New usage is discouraged.)

Ref Expression
Hypotheses str.1 ⊢ 𝐴 ∈ Cℋ
str.2 ⊢ 𝐵 ∈ Cℋ
Assertion stri ( ∀ 𝑓 ∈ States ( ( 𝑓 ‘ 𝐴 ) = 1 → ( 𝑓 ‘ 𝐵 ) = 1 ) → 𝐴 ⊆ 𝐵 )

Proof

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