Metamath Proof Explorer


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 ( 𝜑𝐵 𝑂 𝐴 )