Metamath Proof Explorer

Theorem jplem1

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

Ref Expression
Hypothesis jplem1.1 ⊢ 𝐴 ∈ Cℋ
Assertion jplem1 ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) → ( 𝑢 ∈ 𝐴 ↔ ( ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) ↑ 2 ) = 1 ) )

Proof

Step Hyp Ref Expression
1 jplem1.1 ⊢ 𝐴 ∈ Cℋ
2 pjnorm2 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑢 ∈ ℋ ) → ( 𝑢 ∈ 𝐴 ↔ ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) = ( normℎ ‘ 𝑢 ) ) )
3 1 2 mpan ⊢ ( 𝑢 ∈ ℋ → ( 𝑢 ∈ 𝐴 ↔ ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) = ( normℎ ‘ 𝑢 ) ) )
4 eqeq2 ⊢ ( ( normℎ ‘ 𝑢 ) = 1 → ( ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) = ( normℎ ‘ 𝑢 ) ↔ ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) = 1 ) )
5 3 4 sylan9bb ⊢ ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) → ( 𝑢 ∈ 𝐴 ↔ ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) = 1 ) )
6 sq1 ⊢ ( 1 ↑ 2 ) = 1
7 6 eqeq2i ⊢ ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) ↑ 2 ) = ( 1 ↑ 2 ) ↔ ( ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) ↑ 2 ) = 1 )
8 1 pjhcli ⊢ ( 𝑢 ∈ ℋ → ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ∈ ℋ )
9 normcl ⊢ ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ∈ ℋ → ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) ∈ ℝ )
10 8 9 syl ⊢ ( 𝑢 ∈ ℋ → ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) ∈ ℝ )
11 normge0 ⊢ ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ∈ ℋ → 0 ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) )
12 8 11 syl ⊢ ( 𝑢 ∈ ℋ → 0 ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) )
13 1re ⊢ 1 ∈ ℝ
14 0le1 ⊢ 0 ≤ 1
15 sq11 ⊢ ( ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) ∈ ℝ ∧ 0 ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) ) ∧ ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ) → ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) ↑ 2 ) = ( 1 ↑ 2 ) ↔ ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) = 1 ) )
16 13 14 15 mpanr12 ⊢ ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) ∈ ℝ ∧ 0 ≤ ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) ) → ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) ↑ 2 ) = ( 1 ↑ 2 ) ↔ ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) = 1 ) )
17 10 12 16 syl2anc ⊢ ( 𝑢 ∈ ℋ → ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) ↑ 2 ) = ( 1 ↑ 2 ) ↔ ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) = 1 ) )
18 7 17 bitr3id ⊢ ( 𝑢 ∈ ℋ → ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) ↑ 2 ) = 1 ↔ ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) = 1 ) )
19 18 adantr ⊢ ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) → ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) ↑ 2 ) = 1 ↔ ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) = 1 ) )
20 5 19 bitr4d ⊢ ( ( 𝑢 ∈ ℋ ∧ ( normℎ ‘ 𝑢 ) = 1 ) → ( 𝑢 ∈ 𝐴 ↔ ( ( normℎ ‘ ( ( projℎ ‘ 𝐴 ) ‘ 𝑢 ) ) ↑ 2 ) = 1 ) )