Theorem hstrlem6

Description: Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		hstrlem3.1	⊢ 𝑆 = ( 𝑥 ∈ Cℋ ↦ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) )
2		hstrlem3.2	⊢ ( 𝜑 ↔ ( 𝑢 ∈ ( 𝐴 ∖ 𝐵 ) ∧ ( normℎ ‘ 𝑢 ) = 1 ) )
3		hstrlem3.3	⊢ 𝐴 ∈ Cℋ
4		hstrlem3.4	⊢ 𝐵 ∈ Cℋ
5	1 2 3 4	hstrlem4	⊢ ( 𝜑 → ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) = 1 )
6	1 2 3 4	hstrlem3	⊢ ( 𝜑 → 𝑆 ∈ CHStates )
7		hstcl	⊢ ( ( 𝑆 ∈ CHStates ∧ 𝐵 ∈ Cℋ ) → ( 𝑆 ‘ 𝐵 ) ∈ ℋ )
8	6 4 7	sylancl	⊢ ( 𝜑 → ( 𝑆 ‘ 𝐵 ) ∈ ℋ )
9		normcl	⊢ ( ( 𝑆 ‘ 𝐵 ) ∈ ℋ → ( normℎ ‘ ( 𝑆 ‘ 𝐵 ) ) ∈ ℝ )
10	8 9	syl	⊢ ( 𝜑 → ( normℎ ‘ ( 𝑆 ‘ 𝐵 ) ) ∈ ℝ )
11	1 2 3 4	hstrlem5	⊢ ( 𝜑 → ( normℎ ‘ ( 𝑆 ‘ 𝐵 ) ) < 1 )
12	10 11	ltned	⊢ ( 𝜑 → ( normℎ ‘ ( 𝑆 ‘ 𝐵 ) ) ≠ 1 )
13	12	neneqd	⊢ ( 𝜑 → ¬ ( normℎ ‘ ( 𝑆 ‘ 𝐵 ) ) = 1 )
14	5 13	jcnd	⊢ ( 𝜑 → ¬ ( ( normℎ ‘ ( 𝑆 ‘ 𝐴 ) ) = 1 → ( normℎ ‘ ( 𝑆 ‘ 𝐵 ) ) = 1 ) )