Metamath Proof Explorer

Theorem cgrtriv

Description: Degenerate segments are congruent. Theorem 2.8 of Schwabhauser p. 28. (Contributed by Scott Fenton, 12-Jun-2013)

Ref Expression
Assertion cgrtriv 
|- ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> <. A , A >. Cgr <. B , B >. )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> N e. NN )
2 simp2 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> A e. ( EE ` N ) )
3 simp3 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> B e. ( EE ` N ) )
4 axsegcon 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> E. x e. ( EE ` N ) ( A Btwn <. A , x >. /\ <. A , x >. Cgr <. B , B >. ) )
5 1 2 2 3 3 4 syl122anc 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> E. x e. ( EE ` N ) ( A Btwn <. A , x >. /\ <. A , x >. Cgr <. B , B >. ) )
6 simpl1 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ x e. ( EE ` N ) ) -> N e. NN )
7 simpl2 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ x e. ( EE ` N ) ) -> A e. ( EE ` N ) )
8 simpr 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ x e. ( EE ` N ) ) -> x e. ( EE ` N ) )
9 simpl3 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ x e. ( EE ` N ) ) -> B e. ( EE ` N ) )
10 axcgrid 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ x e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( <. A , x >. Cgr <. B , B >. -> A = x ) )
11 6 7 8 9 10 syl13anc 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ x e. ( EE ` N ) ) -> ( <. A , x >. Cgr <. B , B >. -> A = x ) )
12 opeq2 
 |-  ( A = x -> <. A , A >. = <. A , x >. )
13 12 breq1d 
 |-  ( A = x -> ( <. A , A >. Cgr <. B , B >. <-> <. A , x >. Cgr <. B , B >. ) )
14 13 biimprd 
 |-  ( A = x -> ( <. A , x >. Cgr <. B , B >. -> <. A , A >. Cgr <. B , B >. ) )
15 11 14 syli 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ x e. ( EE ` N ) ) -> ( <. A , x >. Cgr <. B , B >. -> <. A , A >. Cgr <. B , B >. ) )
16 15 adantld 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ x e. ( EE ` N ) ) -> ( ( A Btwn <. A , x >. /\ <. A , x >. Cgr <. B , B >. ) -> <. A , A >. Cgr <. B , B >. ) )
17 16 rexlimdva 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( E. x e. ( EE ` N ) ( A Btwn <. A , x >. /\ <. A , x >. Cgr <. B , B >. ) -> <. A , A >. Cgr <. B , B >. ) )
18 5 17 mpd 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> <. A , A >. Cgr <. B , B >. )