Theorem jplem2

Description: Lemma for Jauch-Piron theorem. (Contributed by NM, 8-Apr-2001) (New usage is discouraged.)

	Ref	Expression
Hypotheses	jp.1	⊢ 𝑆 = ( 𝑥 ∈ Cℋ ↦ ( ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ↑ 2 ) )
	jp.2	⊢ 𝐴 ∈ Cℋ
Assertion	jplem2	⊢ ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) → ( 𝑢 ∈ 𝐴 ↔ ( 𝑆 ‘ 𝐴 ) = 1 ) )

Proof

Step	Hyp	Ref	Expression
1		jp.1	⊢ 𝑆 = ( 𝑥 ∈ Cℋ ↦ ( ( normℎ ‘ ( ( projℎ ‘ 𝑥 ) ‘ 𝑢 ) ) ↑ 2 ) )
2		jp.2	⊢ 𝐴 ∈ Cℋ
3	2	jplem1	⊢ ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) → ( 𝑢 ∈ 𝐴 ↔ ( ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) ↑ 2 ) = 1 ) )
4	1	strlem2	⊢ ( 𝐴 ∈ Cℋ → ( 𝑆 ‘ 𝐴 ) = ( ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) ↑ 2 ) )
5	2 4	ax-mp	⊢ ( 𝑆 ‘ 𝐴 ) = ( ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) ↑ 2 )
6	5	eqeq1i	⊢ ( ( 𝑆 ‘ 𝐴 ) = 1 ↔ ( ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) ↑ 2 ) = 1 )
7	3 6	bitr4di	⊢ ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) → ( 𝑢 ∈ 𝐴 ↔ ( 𝑆 ‘ 𝐴 ) = 1 ) )