Theorem ofscom

Description: The outer five segment predicate commutes. (Contributed by Scott Fenton, 26-Sep-2013)

	Ref	Expression
Assertion	ofscom	|- ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. <. A , B >. , <. C , D >. >. OuterFiveSeg <. <. E , F >. , <. G , H >. >. <-> <. <. E , F >. , <. G , H >. >. OuterFiveSeg <. <. A , B >. , <. C , D >. >. ) )

Proof

Step	Hyp	Ref	Expression
1		ancom	|- ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) <-> ( F Btwn <. E , G >. /\ B Btwn <. A , C >. ) )
2	1	a1i	|- ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) <-> ( F Btwn <. E , G >. /\ B Btwn <. A , C >. ) ) )
3		simp11	|- ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> N e. NN )
4		simp12	|- ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
5		simp13	|- ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
6		simp23	|- ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> E e. ( EE ` N ) )
7		simp31	|- ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> F e. ( EE ` N ) )
8		cgrcom	|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( <. A , B >. Cgr <. E , F >. <-> <. E , F >. Cgr <. A , B >. ) )
9	3 4 5 6 7 8	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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. A , B >. Cgr <. E , F >. <-> <. E , F >. Cgr <. A , B >. ) )
10		simp21	|- ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
11		simp32	|- ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> G e. ( EE ` N ) )
12		cgrcom	|- ( ( N e. NN /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) ) ) -> ( <. B , C >. Cgr <. F , G >. <-> <. F , G >. Cgr <. B , C >. ) )
13	3 5 10 7 11 12	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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. B , C >. Cgr <. F , G >. <-> <. F , G >. Cgr <. B , C >. ) )
14	9 13	anbi12d	|- ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( <. A , B >. Cgr <. E , F >. /\ <. B , C >. Cgr <. F , G >. ) <-> ( <. E , F >. Cgr <. A , B >. /\ <. F , G >. Cgr <. B , C >. ) ) )
15		simp22	|- ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> D e. ( EE ` N ) )
16		simp33	|- ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> H e. ( EE ` N ) )
17		cgrcom	|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. A , D >. Cgr <. E , H >. <-> <. E , H >. Cgr <. A , D >. ) )
18	3 4 15 6 16 17	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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. A , D >. Cgr <. E , H >. <-> <. E , H >. Cgr <. A , D >. ) )
19		cgrcom	|- ( ( N e. NN /\ ( B e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. B , D >. Cgr <. F , H >. <-> <. F , H >. Cgr <. B , D >. ) )
20	3 5 15 7 16 19	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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. B , D >. Cgr <. F , H >. <-> <. F , H >. Cgr <. B , D >. ) )
21	18 20	anbi12d	|- ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) <-> ( <. E , H >. Cgr <. A , D >. /\ <. F , H >. Cgr <. B , D >. ) ) )
22	2 14 21	3anbi123d	|- ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , B >. Cgr <. E , F >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) ) <-> ( ( F Btwn <. E , G >. /\ B Btwn <. A , C >. ) /\ ( <. E , F >. Cgr <. A , B >. /\ <. F , G >. Cgr <. B , C >. ) /\ ( <. E , H >. Cgr <. A , D >. /\ <. F , H >. Cgr <. B , D >. ) ) ) )
23		brofs	|- ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. <. A , B >. , <. C , D >. >. OuterFiveSeg <. <. E , F >. , <. G , H >. >. <-> ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , B >. Cgr <. E , F >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) ) ) )
24		brofs	|- ( ( ( N e. NN /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) /\ ( G e. ( EE ` N ) /\ H e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( <. <. E , F >. , <. G , H >. >. OuterFiveSeg <. <. A , B >. , <. C , D >. >. <-> ( ( F Btwn <. E , G >. /\ B Btwn <. A , C >. ) /\ ( <. E , F >. Cgr <. A , B >. /\ <. F , G >. Cgr <. B , C >. ) /\ ( <. E , H >. Cgr <. A , D >. /\ <. F , H >. Cgr <. B , D >. ) ) ) )
25	3 6 7 11 16 4 5 10 15 24	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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. <. E , F >. , <. G , H >. >. OuterFiveSeg <. <. A , B >. , <. C , D >. >. <-> ( ( F Btwn <. E , G >. /\ B Btwn <. A , C >. ) /\ ( <. E , F >. Cgr <. A , B >. /\ <. F , G >. Cgr <. B , C >. ) /\ ( <. E , H >. Cgr <. A , D >. /\ <. F , H >. Cgr <. B , D >. ) ) ) )
26	22 23 25	3bitr4d	|- ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. <. A , B >. , <. C , D >. >. OuterFiveSeg <. <. E , F >. , <. G , H >. >. <-> <. <. E , F >. , <. G , H >. >. OuterFiveSeg <. <. A , B >. , <. C , D >. >. ) )