Metamath Proof Explorer


Theorem outsideoftr

Description: Transitivity law for outsideness. Theorem 6.7 of Schwabhauser p. 44. (Contributed by Scott Fenton, 18-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion outsideoftr N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N P OutsideOf A B P OutsideOf B C P OutsideOf A C

Proof

Step Hyp Ref Expression
1 simpll A P B P B P C P A P
2 simplr A P B P B P C P B P
3 simprr A P B P B P C P C P
4 1 2 3 3jca A P B P B P C P A P B P C P
5 simplr1 N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P A Btwn P B B Btwn P A B Btwn P C C Btwn P B A P
6 simplr3 N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P A Btwn P B B Btwn P A B Btwn P C C Btwn P B C P
7 df-3an A P B P C P A Btwn P B B Btwn P C A P B P C P A Btwn P B B Btwn P C
8 simp1 N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N N
9 simp3r N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N P 𝔼 N
10 simp2l N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A 𝔼 N
11 simp2r N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N B 𝔼 N
12 simp3l N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N C 𝔼 N
13 simpr2 N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P A Btwn P B B Btwn P C A Btwn P B
14 simpr3 N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P A Btwn P B B Btwn P C B Btwn P C
15 8 9 10 11 12 13 14 btwnexchand N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P A Btwn P B B Btwn P C A Btwn P C
16 15 orcd N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P A Btwn P B B Btwn P C A Btwn P C C Btwn P A
17 7 16 sylan2br N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P A Btwn P B B Btwn P C A Btwn P C C Btwn P A
18 17 expr N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P A Btwn P B B Btwn P C A Btwn P C C Btwn P A
19 simprlr N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P A Btwn P B C Btwn P B A Btwn P B
20 simprr N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P A Btwn P B C Btwn P B C Btwn P B
21 btwnconn3 N P 𝔼 N A 𝔼 N C 𝔼 N B 𝔼 N A Btwn P B C Btwn P B A Btwn P C C Btwn P A
22 8 9 10 12 11 21 syl122anc N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A Btwn P B C Btwn P B A Btwn P C C Btwn P A
23 22 adantr N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P A Btwn P B C Btwn P B A Btwn P B C Btwn P B A Btwn P C C Btwn P A
24 19 20 23 mp2and N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P A Btwn P B C Btwn P B A Btwn P C C Btwn P A
25 24 expr N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P A Btwn P B C Btwn P B A Btwn P C C Btwn P A
26 18 25 jaod N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P A Btwn P B B Btwn P C C Btwn P B A Btwn P C C Btwn P A
27 26 expr N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P A Btwn P B B Btwn P C C Btwn P B A Btwn P C C Btwn P A
28 simpll2 A P B P C P B Btwn P A B Btwn P C B P
29 28 adantl N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P B Btwn P A B Btwn P C B P
30 29 necomd N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P B Btwn P A B Btwn P C P B
31 simprlr N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P B Btwn P A B Btwn P C B Btwn P A
32 simprr N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P B Btwn P A B Btwn P C B Btwn P C
33 btwnconn1 N P 𝔼 N B 𝔼 N A 𝔼 N C 𝔼 N P B B Btwn P A B Btwn P C A Btwn P C C Btwn P A
34 8 9 11 10 12 33 syl122anc N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N P B B Btwn P A B Btwn P C A Btwn P C C Btwn P A
35 34 adantr N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P B Btwn P A B Btwn P C P B B Btwn P A B Btwn P C A Btwn P C C Btwn P A
36 30 31 32 35 mp3and N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P B Btwn P A B Btwn P C A Btwn P C C Btwn P A
37 36 expr N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P B Btwn P A B Btwn P C A Btwn P C C Btwn P A
38 df-3an A P B P C P B Btwn P A C Btwn P B A P B P C P B Btwn P A C Btwn P B
39 simpr3 N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P B Btwn P A C Btwn P B C Btwn P B
40 simpr2 N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P B Btwn P A C Btwn P B B Btwn P A
41 8 9 12 11 10 39 40 btwnexchand N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P B Btwn P A C Btwn P B C Btwn P A
42 41 olcd N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P B Btwn P A C Btwn P B A Btwn P C C Btwn P A
43 38 42 sylan2br N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P B Btwn P A C Btwn P B A Btwn P C C Btwn P A
44 43 expr N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P B Btwn P A C Btwn P B A Btwn P C C Btwn P A
45 37 44 jaod N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P B Btwn P A B Btwn P C C Btwn P B A Btwn P C C Btwn P A
46 45 expr N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P B Btwn P A B Btwn P C C Btwn P B A Btwn P C C Btwn P A
47 27 46 jaod N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P A Btwn P B B Btwn P A B Btwn P C C Btwn P B A Btwn P C C Btwn P A
48 47 imp32 N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P A Btwn P B B Btwn P A B Btwn P C C Btwn P B A Btwn P C C Btwn P A
49 5 6 48 3jca N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P A Btwn P B B Btwn P A B Btwn P C C Btwn P B A P C P A Btwn P C C Btwn P A
50 49 exp31 N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P C P A Btwn P B B Btwn P A B Btwn P C C Btwn P B A P C P A Btwn P C C Btwn P A
51 4 50 syl5 N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P B P C P A Btwn P B B Btwn P A B Btwn P C C Btwn P B A P C P A Btwn P C C Btwn P A
52 51 impd N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N A P B P B P C P A Btwn P B B Btwn P A B Btwn P C C Btwn P B A P C P A Btwn P C C Btwn P A
53 broutsideof2 N P 𝔼 N A 𝔼 N B 𝔼 N P OutsideOf A B A P B P A Btwn P B B Btwn P A
54 8 9 10 11 53 syl13anc N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N P OutsideOf A B A P B P A Btwn P B B Btwn P A
55 broutsideof2 N P 𝔼 N B 𝔼 N C 𝔼 N P OutsideOf B C B P C P B Btwn P C C Btwn P B
56 8 9 11 12 55 syl13anc N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N P OutsideOf B C B P C P B Btwn P C C Btwn P B
57 54 56 anbi12d N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N P OutsideOf A B P OutsideOf B C A P B P A Btwn P B B Btwn P A B P C P B Btwn P C C Btwn P B
58 df-3an A P B P A Btwn P B B Btwn P A A P B P A Btwn P B B Btwn P A
59 df-3an B P C P B Btwn P C C Btwn P B B P C P B Btwn P C C Btwn P B
60 58 59 anbi12i A P B P A Btwn P B B Btwn P A B P C P B Btwn P C C Btwn P B A P B P A Btwn P B B Btwn P A B P C P B Btwn P C C Btwn P B
61 an4 A P B P B P C P A Btwn P B B Btwn P A B Btwn P C C Btwn P B A P B P A Btwn P B B Btwn P A B P C P B Btwn P C C Btwn P B
62 60 61 bitr4i A P B P A Btwn P B B Btwn P A B P C P B Btwn P C C Btwn P B A P B P B P C P A Btwn P B B Btwn P A B Btwn P C C Btwn P B
63 57 62 bitrdi N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N P OutsideOf A B P OutsideOf B C A P B P B P C P A Btwn P B B Btwn P A B Btwn P C C Btwn P B
64 broutsideof2 N P 𝔼 N A 𝔼 N C 𝔼 N P OutsideOf A C A P C P A Btwn P C C Btwn P A
65 8 9 10 12 64 syl13anc N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N P OutsideOf A C A P C P A Btwn P C C Btwn P A
66 52 63 65 3imtr4d N A 𝔼 N B 𝔼 N C 𝔼 N P 𝔼 N P OutsideOf A B P OutsideOf B C P OutsideOf A C