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 e. CH
Assertion jplem1 
|- ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> ( u e. A <-> ( ( normh ` ( ( projh ` A ) ` u ) ) ^ 2 ) = 1 ) )

Proof

Step Hyp Ref Expression
1 jplem1.1 
 |-  A e. CH
2 pjnorm2 
 |-  ( ( A e. CH /\ u e. ~H ) -> ( u e. A <-> ( normh ` ( ( projh ` A ) ` u ) ) = ( normh ` u ) ) )
3 1 2 mpan 
 |-  ( u e. ~H -> ( u e. A <-> ( normh ` ( ( projh ` A ) ` u ) ) = ( normh ` u ) ) )
4 eqeq2 
 |-  ( ( normh ` u ) = 1 -> ( ( normh ` ( ( projh ` A ) ` u ) ) = ( normh ` u ) <-> ( normh ` ( ( projh ` A ) ` u ) ) = 1 ) )
5 3 4 sylan9bb 
 |-  ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> ( u e. A <-> ( normh ` ( ( projh ` A ) ` u ) ) = 1 ) )
6 sq1 
 |-  ( 1 ^ 2 ) = 1
7 6 eqeq2i 
 |-  ( ( ( normh ` ( ( projh ` A ) ` u ) ) ^ 2 ) = ( 1 ^ 2 ) <-> ( ( normh ` ( ( projh ` A ) ` u ) ) ^ 2 ) = 1 )
8 1 pjhcli 
 |-  ( u e. ~H -> ( ( projh ` A ) ` u ) e. ~H )
9 normcl 
 |-  ( ( ( projh ` A ) ` u ) e. ~H -> ( normh ` ( ( projh ` A ) ` u ) ) e. RR )
10 8 9 syl 
 |-  ( u e. ~H -> ( normh ` ( ( projh ` A ) ` u ) ) e. RR )
11 normge0 
 |-  ( ( ( projh ` A ) ` u ) e. ~H -> 0 <_ ( normh ` ( ( projh ` A ) ` u ) ) )
12 8 11 syl 
 |-  ( u e. ~H -> 0 <_ ( normh ` ( ( projh ` A ) ` u ) ) )
13 1re 
 |-  1 e. RR
14 0le1 
 |-  0 <_ 1
15 sq11 
 |-  ( ( ( ( normh ` ( ( projh ` A ) ` u ) ) e. RR /\ 0 <_ ( normh ` ( ( projh ` A ) ` u ) ) ) /\ ( 1 e. RR /\ 0 <_ 1 ) ) -> ( ( ( normh ` ( ( projh ` A ) ` u ) ) ^ 2 ) = ( 1 ^ 2 ) <-> ( normh ` ( ( projh ` A ) ` u ) ) = 1 ) )
16 13 14 15 mpanr12 
 |-  ( ( ( normh ` ( ( projh ` A ) ` u ) ) e. RR /\ 0 <_ ( normh ` ( ( projh ` A ) ` u ) ) ) -> ( ( ( normh ` ( ( projh ` A ) ` u ) ) ^ 2 ) = ( 1 ^ 2 ) <-> ( normh ` ( ( projh ` A ) ` u ) ) = 1 ) )
17 10 12 16 syl2anc 
 |-  ( u e. ~H -> ( ( ( normh ` ( ( projh ` A ) ` u ) ) ^ 2 ) = ( 1 ^ 2 ) <-> ( normh ` ( ( projh ` A ) ` u ) ) = 1 ) )
18 7 17 bitr3id 
 |-  ( u e. ~H -> ( ( ( normh ` ( ( projh ` A ) ` u ) ) ^ 2 ) = 1 <-> ( normh ` ( ( projh ` A ) ` u ) ) = 1 ) )
19 18 adantr 
 |-  ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> ( ( ( normh ` ( ( projh ` A ) ` u ) ) ^ 2 ) = 1 <-> ( normh ` ( ( projh ` A ) ` u ) ) = 1 ) )
20 5 19 bitr4d 
 |-  ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> ( u e. A <-> ( ( normh ` ( ( projh ` A ) ` u ) ) ^ 2 ) = 1 ) )