Theorem strlem4

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	strlem4	⊢ ( 𝜑 → ( 𝑆 ‘ 𝐴 ) = 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	strlem2	⊢ ( 𝐴 ∈ Cℋ → ( 𝑆 ‘ 𝐴 ) = ( ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) ↑ 2 ) )
6	3 5	ax-mp	⊢ ( 𝑆 ‘ 𝐴 ) = ( ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) ↑ 2 )
7		eldifi	⊢ ( 𝑢 ∈ ( 𝐴 ∖ 𝐵 ) → 𝑢 ∈ 𝐴 )
8		pjid	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑢 ∈ 𝐴 ) → ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) = 𝑢 )
9	3 8	mpan	⊢ ( 𝑢 ∈ 𝐴 → ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) = 𝑢 )
10	9	fveq2d	⊢ ( 𝑢 ∈ 𝐴 → ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) = ( normℎ ‘ 𝑢 ) )
11		eqeq2	⊢ ( ( normℎ ‘ 𝑢 ) = 1 → ( ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) = ( normℎ ‘ 𝑢 ) ↔ ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) = 1 ) )
12	10 11	imbitrid	⊢ ( ( normℎ ‘ 𝑢 ) = 1 → ( 𝑢 ∈ 𝐴 → ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) = 1 ) )
13	7 12	mpan9	⊢ ( ( 𝑢 ∈ ( 𝐴 ∖ 𝐵 ) ∧ ( normℎ ‘ 𝑢 ) = 1 ) → ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) = 1 )
14	2 13	sylbi	⊢ ( 𝜑 → ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) = 1 )
15	14	oveq1d	⊢ ( 𝜑 → ( ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) ↑ 2 ) = ( 1 ↑ 2 ) )
16		sq1	⊢ ( 1 ↑ 2 ) = 1
17	15 16	eqtrdi	⊢ ( 𝜑 → ( ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) ↑ 2 ) = 1 )
18	6 17	eqtrid	⊢ ( 𝜑 → ( 𝑆 ‘ 𝐴 ) = 1 )