Theorem hstrlem5

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	hstrlem5	⊢ ( 𝜑 → ( 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	hstrlem2	⊢ ( 𝐵 ∈ Cℋ → ( 𝑆 ‘ 𝐵 ) = ( ( projℎ ‘ 𝐵 ) ‘ 𝑢 ) )
6	5	fveq2d	⊢ ( 𝐵 ∈ Cℋ → ( normℎ ‘ ( 𝑆 ‘ 𝐵 ) ) = ( normℎ ‘ ( ( projℎ ‘ 𝐵 ) ‘ 𝑢 ) ) )
7	4 6	ax-mp	⊢ ( normℎ ‘ ( 𝑆 ‘ 𝐵 ) ) = ( normℎ ‘ ( ( projℎ ‘ 𝐵 ) ‘ 𝑢 ) )
8		eldif	⊢ ( 𝑢 ∈ ( 𝐴 ∖ 𝐵 ) ↔ ( 𝑢 ∈ 𝐴 ∧ ¬ 𝑢 ∈ 𝐵 ) )
9	3	cheli	⊢ ( 𝑢 ∈ 𝐴 → 𝑢 ∈ ℋ )
10		pjnel	⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝑢 ∈ ℋ ) → ( ¬ 𝑢 ∈ 𝐵 ↔ ( normℎ ‘ ( ( projℎ ‘ 𝐵 ) ‘ 𝑢 ) ) < ( normℎ ‘ 𝑢 ) ) )
11	4 10	mpan	⊢ ( 𝑢 ∈ ℋ → ( ¬ 𝑢 ∈ 𝐵 ↔ ( normℎ ‘ ( ( projℎ ‘ 𝐵 ) ‘ 𝑢 ) ) < ( normℎ ‘ 𝑢 ) ) )
12	11	biimpa	⊢ ( ( 𝑢 ∈ ℋ ∧ ¬ 𝑢 ∈ 𝐵 ) → ( normℎ ‘ ( ( projℎ ‘ 𝐵 ) ‘ 𝑢 ) ) < ( normℎ ‘ 𝑢 ) )
13	9 12	sylan	⊢ ( ( 𝑢 ∈ 𝐴 ∧ ¬ 𝑢 ∈ 𝐵 ) → ( normℎ ‘ ( ( projℎ ‘ 𝐵 ) ‘ 𝑢 ) ) < ( normℎ ‘ 𝑢 ) )
14	8 13	sylbi	⊢ ( 𝑢 ∈ ( 𝐴 ∖ 𝐵 ) → ( normℎ ‘ ( ( projℎ ‘ 𝐵 ) ‘ 𝑢 ) ) < ( normℎ ‘ 𝑢 ) )
15		breq2	⊢ ( ( normℎ ‘ 𝑢 ) = 1 → ( ( normℎ ‘ ( ( projℎ ‘ 𝐵 ) ‘ 𝑢 ) ) < ( normℎ ‘ 𝑢 ) ↔ ( normℎ ‘ ( ( projℎ ‘ 𝐵 ) ‘ 𝑢 ) ) < 1 ) )
16	14 15	imbitrid	⊢ ( ( normℎ ‘ 𝑢 ) = 1 → ( 𝑢 ∈ ( 𝐴 ∖ 𝐵 ) → ( normℎ ‘ ( ( projℎ ‘ 𝐵 ) ‘ 𝑢 ) ) < 1 ) )
17	16	impcom	⊢ ( ( 𝑢 ∈ ( 𝐴 ∖ 𝐵 ) ∧ ( normℎ ‘ 𝑢 ) = 1 ) → ( normℎ ‘ ( ( projℎ ‘ 𝐵 ) ‘ 𝑢 ) ) < 1 )
18	7 17	eqbrtrid	⊢ ( ( 𝑢 ∈ ( 𝐴 ∖ 𝐵 ) ∧ ( normℎ ‘ 𝑢 ) = 1 ) → ( normℎ ‘ ( 𝑆 ‘ 𝐵 ) ) < 1 )
19	2 18	sylbi	⊢ ( 𝜑 → ( normℎ ‘ ( 𝑆 ‘ 𝐵 ) ) < 1 )