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 syl5bbr 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