Theorem oppcom

Description: Commutativity rule for "opposite" Theorem 9.2 of Schwabhauser p. 67. (Contributed by Thierry Arnoux, 19-Dec-2019)

	Ref	Expression
Hypotheses	hpg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	hpg.d	⊢ − = ( dist ‘ 𝐺 )
	hpg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	hpg.o	⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
	opphl.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	opphl.d	⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
	opphl.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	oppcom.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	oppcom.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	oppcom.o	⊢ ( 𝜑 → 𝐴 𝑂 𝐵 )
Assertion	oppcom	⊢ ( 𝜑 → 𝐵 𝑂 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		hpg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		hpg.d	⊢ − = ( dist ‘ 𝐺 )
3		hpg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		hpg.o	⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
5		opphl.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
6		opphl.d	⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
7		opphl.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
8		oppcom.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
9		oppcom.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
10		oppcom.o	⊢ ( 𝜑 → 𝐴 𝑂 𝐵 )
11	1 2 3 4 8 9	islnopp	⊢ ( 𝜑 → ( 𝐴 𝑂 𝐵 ↔ ( ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) ) )
12	10 11	mpbid	⊢ ( 𝜑 → ( ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) )
13	12	simpld	⊢ ( 𝜑 → ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) )
14	13	simprd	⊢ ( 𝜑 → ¬ 𝐵 ∈ 𝐷 )
15	13	simpld	⊢ ( 𝜑 → ¬ 𝐴 ∈ 𝐷 )
16	12	simprd	⊢ ( 𝜑 → ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) )
17	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐺 ∈ TarskiG )
18	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐴 ∈ 𝑃 )
19	7	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → 𝐺 ∈ TarskiG )
20	6	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → 𝐷 ∈ ran 𝐿 )
21		simpr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → 𝑡 ∈ 𝐷 )
22	1 5 3 19 20 21	tglnpt	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → 𝑡 ∈ 𝑃 )
23	22	adantr	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝑡 ∈ 𝑃 )
24	9	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐵 ∈ 𝑃 )
25		simpr	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) )
26	1 2 3 17 18 23 24 25	tgbtwncom	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝑡 ∈ ( 𝐵 𝐼 𝐴 ) )
27	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐵 𝐼 𝐴 ) ) → 𝐺 ∈ TarskiG )
28	9	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐵 𝐼 𝐴 ) ) → 𝐵 ∈ 𝑃 )
29	22	adantr	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐵 𝐼 𝐴 ) ) → 𝑡 ∈ 𝑃 )
30	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐵 𝐼 𝐴 ) ) → 𝐴 ∈ 𝑃 )
31		simpr	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐵 𝐼 𝐴 ) ) → 𝑡 ∈ ( 𝐵 𝐼 𝐴 ) )
32	1 2 3 27 28 29 30 31	tgbtwncom	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) ∧ 𝑡 ∈ ( 𝐵 𝐼 𝐴 ) ) → 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) )
33	26 32	impbida	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ↔ 𝑡 ∈ ( 𝐵 𝐼 𝐴 ) ) )
34	33	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 𝐵 ) ↔ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐵 𝐼 𝐴 ) ) )
35	16 34	mpbid	⊢ ( 𝜑 → ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐵 𝐼 𝐴 ) )
36	14 15 35	jca31	⊢ ( 𝜑 → ( ( ¬ 𝐵 ∈ 𝐷 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐵 𝐼 𝐴 ) ) )
37	1 2 3 4 9 8	islnopp	⊢ ( 𝜑 → ( 𝐵 𝑂 𝐴 ↔ ( ( ¬ 𝐵 ∈ 𝐷 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐵 𝐼 𝐴 ) ) ) )
38	36 37	mpbird	⊢ ( 𝜑 → 𝐵 𝑂 𝐴 )