Theorem strlem2

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

	Ref	Expression
Hypothesis	strlem2.1	⊢ 𝑆 = ( 𝑥 ∈ Cℋ ↦ ( ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ↑ 2 ) )
Assertion	strlem2	⊢ ( 𝐶 ∈ Cℋ → ( 𝑆 ‘ 𝐶 ) = ( ( normℎ ‘ ( ( projℎ ‘ 𝐶 ) ‘ 𝑢 ) ) ↑ 2 ) )

Proof

Step	Hyp	Ref	Expression
1		strlem2.1	⊢ 𝑆 = ( 𝑥 ∈ Cℋ ↦ ( ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ↑ 2 ) )
2		fveq2	⊢ ( 𝑥 = 𝐶 → ( projℎ ‘ 𝑥 ) = ( projℎ ‘ 𝐶 ) )
3	2	fveq1d	⊢ ( 𝑥 = 𝐶 → ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) = ( ( projℎ ‘ 𝐶 ) ‘ 𝑢 ) )
4	3	fveq2d	⊢ ( 𝑥 = 𝐶 → ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) = ( normℎ ‘ ( ( projℎ ‘ 𝐶 ) ‘ 𝑢 ) ) )
5	4	oveq1d	⊢ ( 𝑥 = 𝐶 → ( ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ↑ 2 ) = ( ( normℎ ‘ ( ( projℎ ‘ 𝐶 ) ‘ 𝑢 ) ) ↑ 2 ) )
6		ovex	⊢ ( ( normℎ ‘ ( ( projℎ ‘ 𝐶 ) ‘ 𝑢 ) ) ↑ 2 ) ∈ V
7	5 1 6	fvmpt	⊢ ( 𝐶 ∈ Cℋ → ( 𝑆 ‘ 𝐶 ) = ( ( normℎ ‘ ( ( projℎ ‘ 𝐶 ) ‘ 𝑢 ) ) ↑ 2 ) )