# 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 $⊢ A ∈ C ℋ$
Assertion jplem1 $⊢ u ∈ ℋ ∧ norm ℎ ⁡ u = 1 → u ∈ A ↔ norm ℎ ⁡ proj ℎ ⁡ A ⁡ u 2 = 1$

### Proof

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