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⁡u2=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 ⊢12=1
7 6 eqeq2i ⊢normℎ⁡projℎ⁡A⁡u2=12↔normℎ⁡projℎ⁡A⁡u2=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⁡u2=12↔normℎ⁡projℎ⁡A⁡u=1
16 13 14 15 mpanr12 ⊢normℎ⁡projℎ⁡A⁡u∈ℝ∧0≤normℎ⁡projℎ⁡A⁡u→normℎ⁡projℎ⁡A⁡u2=12↔normℎ⁡projℎ⁡A⁡u=1
17 10 12 16 syl2anc ⊢u∈ℋ→normℎ⁡projℎ⁡A⁡u2=12↔normℎ⁡projℎ⁡A⁡u=1
18 7 17 bitr3id ⊢u∈ℋ→normℎ⁡projℎ⁡A⁡u2=1↔normℎ⁡projℎ⁡A⁡u=1
19 18 adantr ⊢u∈ℋ∧normℎ⁡u=1→normℎ⁡projℎ⁡A⁡u2=1↔normℎ⁡projℎ⁡A⁡u=1
20 5 19 bitr4d ⊢u∈ℋ∧normℎ⁡u=1→u∈A↔normℎ⁡projℎ⁡A⁡u2=1