Metamath Proof Explorer

Theorem pjhtheu2

Description: Uniqueness of y for the projection theorem. (Contributed by NM, 6-Nov-1999) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Assertion pjhtheu2 
|- ( ( H e. CH /\ A e. ~H ) -> E! y e. ( _|_ ` H ) E. x e. H A = ( x +h y ) )

Proof

Step Hyp Ref Expression
1 choccl 
 |-  ( H e. CH -> ( _|_ ` H ) e. CH )
2 pjhtheu 
 |-  ( ( ( _|_ ` H ) e. CH /\ A e. ~H ) -> E! y e. ( _|_ ` H ) E. x e. ( _|_ ` ( _|_ ` H ) ) A = ( y +h x ) )
3 1 2 sylan 
 |-  ( ( H e. CH /\ A e. ~H ) -> E! y e. ( _|_ ` H ) E. x e. ( _|_ ` ( _|_ ` H ) ) A = ( y +h x ) )
4 simpll 
 |-  ( ( ( H e. CH /\ A e. ~H ) /\ y e. ( _|_ ` H ) ) -> H e. CH )
5 ococ 
 |-  ( H e. CH -> ( _|_ ` ( _|_ ` H ) ) = H )
6 4 5 syl 
 |-  ( ( ( H e. CH /\ A e. ~H ) /\ y e. ( _|_ ` H ) ) -> ( _|_ ` ( _|_ ` H ) ) = H )
7 6 rexeqdv 
 |-  ( ( ( H e. CH /\ A e. ~H ) /\ y e. ( _|_ ` H ) ) -> ( E. x e. ( _|_ ` ( _|_ ` H ) ) A = ( y +h x ) <-> E. x e. H A = ( y +h x ) ) )
8 1 adantr 
 |-  ( ( H e. CH /\ A e. ~H ) -> ( _|_ ` H ) e. CH )
9 chel 
 |-  ( ( ( _|_ ` H ) e. CH /\ y e. ( _|_ ` H ) ) -> y e. ~H )
10 8 9 sylan 
 |-  ( ( ( H e. CH /\ A e. ~H ) /\ y e. ( _|_ ` H ) ) -> y e. ~H )
11 10 adantr 
 |-  ( ( ( ( H e. CH /\ A e. ~H ) /\ y e. ( _|_ ` H ) ) /\ x e. H ) -> y e. ~H )
12 chel 
 |-  ( ( H e. CH /\ x e. H ) -> x e. ~H )
13 4 12 sylan 
 |-  ( ( ( ( H e. CH /\ A e. ~H ) /\ y e. ( _|_ ` H ) ) /\ x e. H ) -> x e. ~H )
14 ax-hvcom 
 |-  ( ( y e. ~H /\ x e. ~H ) -> ( y +h x ) = ( x +h y ) )
15 11 13 14 syl2anc 
 |-  ( ( ( ( H e. CH /\ A e. ~H ) /\ y e. ( _|_ ` H ) ) /\ x e. H ) -> ( y +h x ) = ( x +h y ) )
16 15 eqeq2d 
 |-  ( ( ( ( H e. CH /\ A e. ~H ) /\ y e. ( _|_ ` H ) ) /\ x e. H ) -> ( A = ( y +h x ) <-> A = ( x +h y ) ) )
17 16 rexbidva 
 |-  ( ( ( H e. CH /\ A e. ~H ) /\ y e. ( _|_ ` H ) ) -> ( E. x e. H A = ( y +h x ) <-> E. x e. H A = ( x +h y ) ) )
18 7 17 bitrd 
 |-  ( ( ( H e. CH /\ A e. ~H ) /\ y e. ( _|_ ` H ) ) -> ( E. x e. ( _|_ ` ( _|_ ` H ) ) A = ( y +h x ) <-> E. x e. H A = ( x +h y ) ) )
19 18 reubidva 
 |-  ( ( H e. CH /\ A e. ~H ) -> ( E! y e. ( _|_ ` H ) E. x e. ( _|_ ` ( _|_ ` H ) ) A = ( y +h x ) <-> E! y e. ( _|_ ` H ) E. x e. H A = ( x +h y ) ) )
20 3 19 mpbid 
 |-  ( ( H e. CH /\ A e. ~H ) -> E! y e. ( _|_ ` H ) E. x e. H A = ( x +h y ) )