Theorem outsideofcom

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

	Ref	Expression
Assertion	outsideofcom	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ↔ 𝑃 OutsideOf ⟨ 𝐵 , 𝐴 ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		3ancoma	⊢ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) ↔ ( 𝐵 ≠ 𝑃 ∧ 𝐴 ≠ 𝑃 ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) )
2		orcom	⊢ ( ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ↔ ( 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ∨ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) )
3	2	3anbi3i	⊢ ( ( 𝐵 ≠ 𝑃 ∧ 𝐴 ≠ 𝑃 ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) ↔ ( 𝐵 ≠ 𝑃 ∧ 𝐴 ≠ 𝑃 ∧ ( 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ∨ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) )
4	1 3	bitri	⊢ ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) ↔ ( 𝐵 ≠ 𝑃 ∧ 𝐴 ≠ 𝑃 ∧ ( 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ∨ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) )
5	4	a1i	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) ↔ ( 𝐵 ≠ 𝑃 ∧ 𝐴 ≠ 𝑃 ∧ ( 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ∨ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) ) )
6		broutsideof2	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ ( 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ∨ 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ) ) ) )
7		3ancomb	⊢ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ↔ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) )
8		broutsideof2	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑃 OutsideOf ⟨ 𝐵 , 𝐴 ⟩ ↔ ( 𝐵 ≠ 𝑃 ∧ 𝐴 ≠ 𝑃 ∧ ( 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ∨ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) ) )
9	7 8	sylan2b	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑃 OutsideOf ⟨ 𝐵 , 𝐴 ⟩ ↔ ( 𝐵 ≠ 𝑃 ∧ 𝐴 ≠ 𝑃 ∧ ( 𝐵 Btwn ⟨ 𝑃 , 𝐴 ⟩ ∨ 𝐴 Btwn ⟨ 𝑃 , 𝐵 ⟩ ) ) ) )
10	5 6 9	3bitr4d	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑃 OutsideOf ⟨ 𝐴 , 𝐵 ⟩ ↔ 𝑃 OutsideOf ⟨ 𝐵 , 𝐴 ⟩ ) )