Theorem cgrsub

Description: Removing identical parts from the end of a line segment preserves congruence. Theorem 4.3 of Schwabhauser p. 35. (Contributed by Scott Fenton, 4-Oct-2013)

	Ref	Expression
Assertion	cgrsub	|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , C >. Cgr <. D , F >. /\ <. B , C >. Cgr <. E , F >. ) ) -> <. A , B >. Cgr <. D , E >. ) )

Proof

Step	Hyp	Ref	Expression
1		simprl	|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , C >. Cgr <. D , F >. /\ <. B , C >. Cgr <. E , F >. ) ) ) -> ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) )
2		simprr	|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , C >. Cgr <. D , F >. /\ <. B , C >. Cgr <. E , F >. ) ) ) -> ( <. A , C >. Cgr <. D , F >. /\ <. B , C >. Cgr <. E , F >. ) )
3		simpl1	|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , C >. Cgr <. D , F >. /\ <. B , C >. Cgr <. E , F >. ) ) ) -> N e. NN )
4		simpl21	|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , C >. Cgr <. D , F >. /\ <. B , C >. Cgr <. E , F >. ) ) ) -> A e. ( EE ` N ) )
5		simpl31	|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , C >. Cgr <. D , F >. /\ <. B , C >. Cgr <. E , F >. ) ) ) -> D e. ( EE ` N ) )
6		cgrtriv	|- ( ( N e. NN /\ A e. ( EE ` N ) /\ D e. ( EE ` N ) ) -> <. A , A >. Cgr <. D , D >. )
7	3 4 5 6	syl3anc	|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , C >. Cgr <. D , F >. /\ <. B , C >. Cgr <. E , F >. ) ) ) -> <. A , A >. Cgr <. D , D >. )
8		simprrl	|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , C >. Cgr <. D , F >. /\ <. B , C >. Cgr <. E , F >. ) ) ) -> <. A , C >. Cgr <. D , F >. )
9		simpl23	|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , C >. Cgr <. D , F >. /\ <. B , C >. Cgr <. E , F >. ) ) ) -> C e. ( EE ` N ) )
10		simpl33	|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , C >. Cgr <. D , F >. /\ <. B , C >. Cgr <. E , F >. ) ) ) -> F e. ( EE ` N ) )
11		cgrcomlr	|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( <. A , C >. Cgr <. D , F >. <-> <. C , A >. Cgr <. F , D >. ) )
12	3 4 9 5 10 11	syl122anc	|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , C >. Cgr <. D , F >. /\ <. B , C >. Cgr <. E , F >. ) ) ) -> ( <. A , C >. Cgr <. D , F >. <-> <. C , A >. Cgr <. F , D >. ) )
13	8 12	mpbid	|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , C >. Cgr <. D , F >. /\ <. B , C >. Cgr <. E , F >. ) ) ) -> <. C , A >. Cgr <. F , D >. )
14	7 13	jca	|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , C >. Cgr <. D , F >. /\ <. B , C >. Cgr <. E , F >. ) ) ) -> ( <. A , A >. Cgr <. D , D >. /\ <. C , A >. Cgr <. F , D >. ) )
15		simpl22	|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , C >. Cgr <. D , F >. /\ <. B , C >. Cgr <. E , F >. ) ) ) -> B e. ( EE ` N ) )
16		simpl32	|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , C >. Cgr <. D , F >. /\ <. B , C >. Cgr <. E , F >. ) ) ) -> E e. ( EE ` N ) )
17		brifs	|- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ A e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ F e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( <. <. A , B >. , <. C , A >. >. InnerFiveSeg <. <. D , E >. , <. F , D >. >. <-> ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , C >. Cgr <. D , F >. /\ <. B , C >. Cgr <. E , F >. ) /\ ( <. A , A >. Cgr <. D , D >. /\ <. C , A >. Cgr <. F , D >. ) ) ) )
18		ifscgr	|- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ A e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ F e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( <. <. A , B >. , <. C , A >. >. InnerFiveSeg <. <. D , E >. , <. F , D >. >. -> <. B , A >. Cgr <. E , D >. ) )
19	17 18	sylbird	|- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ A e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ F e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , C >. Cgr <. D , F >. /\ <. B , C >. Cgr <. E , F >. ) /\ ( <. A , A >. Cgr <. D , D >. /\ <. C , A >. Cgr <. F , D >. ) ) -> <. B , A >. Cgr <. E , D >. ) )
20	3 4 15 9 4 5 16 10 5 19	syl333anc	|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , C >. Cgr <. D , F >. /\ <. B , C >. Cgr <. E , F >. ) ) ) -> ( ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , C >. Cgr <. D , F >. /\ <. B , C >. Cgr <. E , F >. ) /\ ( <. A , A >. Cgr <. D , D >. /\ <. C , A >. Cgr <. F , D >. ) ) -> <. B , A >. Cgr <. E , D >. ) )
21	1 2 14 20	mp3and	|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , C >. Cgr <. D , F >. /\ <. B , C >. Cgr <. E , F >. ) ) ) -> <. B , A >. Cgr <. E , D >. )
22		cgrcomlr	|- ( ( N e. NN /\ ( B e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( <. B , A >. Cgr <. E , D >. <-> <. A , B >. Cgr <. D , E >. ) )
23	3 15 4 16 5 22	syl122anc	|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , C >. Cgr <. D , F >. /\ <. B , C >. Cgr <. E , F >. ) ) ) -> ( <. B , A >. Cgr <. E , D >. <-> <. A , B >. Cgr <. D , E >. ) )
24	21 23	mpbid	|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , C >. Cgr <. D , F >. /\ <. B , C >. Cgr <. E , F >. ) ) ) -> <. A , B >. Cgr <. D , E >. )
25	24	ex	|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( ( ( B Btwn <. A , C >. /\ E Btwn <. D , F >. ) /\ ( <. A , C >. Cgr <. D , F >. /\ <. B , C >. Cgr <. E , F >. ) ) -> <. A , B >. Cgr <. D , E >. ) )