Theorem strlem6

Description: Lemma for strong state theorem. (Contributed by NM, 2-Nov-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	strlem3.1	⊢ 𝑆 = ( 𝑥 ∈ Cℋ ↦ ( ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ↑ 2 ) )
	strlem3.2	⊢ ( 𝜑 ↔ ( 𝑢 ∈ ( 𝐴 ∖ 𝐵 ) ∧ ( normℎ ‘ 𝑢 ) = 1 ) )
	strlem3.3	⊢ 𝐴 ∈ Cℋ
	strlem3.4	⊢ 𝐵 ∈ Cℋ
Assertion	strlem6	⊢ ( 𝜑 → ¬ ( ( 𝑆 ‘ 𝐴 ) = 1 → ( 𝑆 ‘ 𝐵 ) = 1 ) )

Proof

Step	Hyp	Ref	Expression
1		strlem3.1	⊢ 𝑆 = ( 𝑥 ∈ Cℋ ↦ ( ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ↑ 2 ) )
2		strlem3.2	⊢ ( 𝜑 ↔ ( 𝑢 ∈ ( 𝐴 ∖ 𝐵 ) ∧ ( normℎ ‘ 𝑢 ) = 1 ) )
3		strlem3.3	⊢ 𝐴 ∈ Cℋ
4		strlem3.4	⊢ 𝐵 ∈ Cℋ
5	1 2 3 4	strlem4	⊢ ( 𝜑 → ( 𝑆 ‘ 𝐴 ) = 1 )
6	1 2 3 4	strlem3	⊢ ( 𝜑 → 𝑆 ∈ States )
7		stcl	⊢ ( 𝑆 ∈ States → ( 𝐵 ∈ Cℋ → ( 𝑆 ‘ 𝐵 ) ∈ ℝ ) )
8	6 4 7	mpisyl	⊢ ( 𝜑 → ( 𝑆 ‘ 𝐵 ) ∈ ℝ )
9	1 2 3 4	strlem5	⊢ ( 𝜑 → ( 𝑆 ‘ 𝐵 ) < 1 )
10	8 9	ltned	⊢ ( 𝜑 → ( 𝑆 ‘ 𝐵 ) ≠ 1 )
11	10	neneqd	⊢ ( 𝜑 → ¬ ( 𝑆 ‘ 𝐵 ) = 1 )
12	5 11	jcnd	⊢ ( 𝜑 → ¬ ( ( 𝑆 ‘ 𝐴 ) = 1 → ( 𝑆 ‘ 𝐵 ) = 1 ) )