Metamath Proof Explorer

Theorem linecgr

Description: Congruence rule for lines. Theorem 4.17 of Schwabhauser p. 37. (Contributed by Scott Fenton, 6-Oct-2013)

Ref Expression
Assertion linecgr 
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) ) ) -> ( ( ( A =/= B /\ A Colinear <. B , C >. ) /\ ( <. A , P >. Cgr <. A , Q >. /\ <. B , P >. Cgr <. B , Q >. ) ) -> <. C , P >. Cgr <. C , Q >. ) )

Proof

Step Hyp Ref Expression
1 simprlr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) ) ) /\ ( ( A =/= B /\ A Colinear <. B , C >. ) /\ ( <. A , P >. Cgr <. A , Q >. /\ <. B , P >. Cgr <. B , Q >. ) ) ) -> A Colinear <. B , C >. )
2 cgr3rflx 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> <. A , <. B , C >. >. Cgr3 <. A , <. B , C >. >. )
3 2 3adant3 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) ) ) -> <. A , <. B , C >. >. Cgr3 <. A , <. B , C >. >. )
4 3 adantr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) ) ) /\ ( ( A =/= B /\ A Colinear <. B , C >. ) /\ ( <. A , P >. Cgr <. A , Q >. /\ <. B , P >. Cgr <. B , Q >. ) ) ) -> <. A , <. B , C >. >. Cgr3 <. A , <. B , C >. >. )
5 simprr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) ) ) /\ ( ( A =/= B /\ A Colinear <. B , C >. ) /\ ( <. A , P >. Cgr <. A , Q >. /\ <. B , P >. Cgr <. B , Q >. ) ) ) -> ( <. A , P >. Cgr <. A , Q >. /\ <. B , P >. Cgr <. B , Q >. ) )
6 1 4 5 3jca 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) ) ) /\ ( ( A =/= B /\ A Colinear <. B , C >. ) /\ ( <. A , P >. Cgr <. A , Q >. /\ <. B , P >. Cgr <. B , Q >. ) ) ) -> ( A Colinear <. B , C >. /\ <. A , <. B , C >. >. Cgr3 <. A , <. B , C >. >. /\ ( <. A , P >. Cgr <. A , Q >. /\ <. B , P >. Cgr <. B , Q >. ) ) )
7 simprll 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) ) ) /\ ( ( A =/= B /\ A Colinear <. B , C >. ) /\ ( <. A , P >. Cgr <. A , Q >. /\ <. B , P >. Cgr <. B , Q >. ) ) ) -> A =/= B )
8 6 7 jca 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) ) ) /\ ( ( A =/= B /\ A Colinear <. B , C >. ) /\ ( <. A , P >. Cgr <. A , Q >. /\ <. B , P >. Cgr <. B , Q >. ) ) ) -> ( ( A Colinear <. B , C >. /\ <. A , <. B , C >. >. Cgr3 <. A , <. B , C >. >. /\ ( <. A , P >. Cgr <. A , Q >. /\ <. B , P >. Cgr <. B , Q >. ) ) /\ A =/= B ) )
9 8 ex 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) ) ) -> ( ( ( A =/= B /\ A Colinear <. B , C >. ) /\ ( <. A , P >. Cgr <. A , Q >. /\ <. B , P >. Cgr <. B , Q >. ) ) -> ( ( A Colinear <. B , C >. /\ <. A , <. B , C >. >. Cgr3 <. A , <. B , C >. >. /\ ( <. A , P >. Cgr <. A , Q >. /\ <. B , P >. Cgr <. B , Q >. ) ) /\ A =/= B ) ) )
10 simp1 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) ) ) -> N e. NN )
11 simp21 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
12 simp22 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
13 simp23 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
14 simp3l 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) ) ) -> P e. ( EE ` N ) )
15 simp3r 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) ) ) -> Q e. ( EE ` N ) )
16 brfs 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ Q e. ( EE ` N ) ) ) -> ( <. <. A , B >. , <. C , P >. >. FiveSeg <. <. A , B >. , <. C , Q >. >. <-> ( A Colinear <. B , C >. /\ <. A , <. B , C >. >. Cgr3 <. A , <. B , C >. >. /\ ( <. A , P >. Cgr <. A , Q >. /\ <. B , P >. Cgr <. B , Q >. ) ) ) )
17 16 anbi1d 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ Q e. ( EE ` N ) ) ) -> ( ( <. <. A , B >. , <. C , P >. >. FiveSeg <. <. A , B >. , <. C , Q >. >. /\ A =/= B ) <-> ( ( A Colinear <. B , C >. /\ <. A , <. B , C >. >. Cgr3 <. A , <. B , C >. >. /\ ( <. A , P >. Cgr <. A , Q >. /\ <. B , P >. Cgr <. B , Q >. ) ) /\ A =/= B ) ) )
18 fscgr 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ Q e. ( EE ` N ) ) ) -> ( ( <. <. A , B >. , <. C , P >. >. FiveSeg <. <. A , B >. , <. C , Q >. >. /\ A =/= B ) -> <. C , P >. Cgr <. C , Q >. ) )
19 17 18 sylbird 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ P e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ Q e. ( EE ` N ) ) ) -> ( ( ( A Colinear <. B , C >. /\ <. A , <. B , C >. >. Cgr3 <. A , <. B , C >. >. /\ ( <. A , P >. Cgr <. A , Q >. /\ <. B , P >. Cgr <. B , Q >. ) ) /\ A =/= B ) -> <. C , P >. Cgr <. C , Q >. ) )
20 10 11 12 13 14 11 12 13 15 19 syl333anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) ) ) -> ( ( ( A Colinear <. B , C >. /\ <. A , <. B , C >. >. Cgr3 <. A , <. B , C >. >. /\ ( <. A , P >. Cgr <. A , Q >. /\ <. B , P >. Cgr <. B , Q >. ) ) /\ A =/= B ) -> <. C , P >. Cgr <. C , Q >. ) )
21 9 20 syld 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) ) ) -> ( ( ( A =/= B /\ A Colinear <. B , C >. ) /\ ( <. A , P >. Cgr <. A , Q >. /\ <. B , P >. Cgr <. B , Q >. ) ) -> <. C , P >. Cgr <. C , Q >. ) )