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