Metamath Proof Explorer


Theorem oppnid

Description: The "opposite to a line" relation is irreflexive. (Contributed by Thierry Arnoux, 4-Mar-2020)

Ref Expression
Hypotheses hpg.p P=BaseG
hpg.d -˙=distG
hpg.i I=ItvG
hpg.o O=ab|aPDbPDtDtaIb
opphl.l L=Line𝒢G
opphl.d φDranL
opphl.g φG𝒢Tarski
oppnid.1 φAP
Assertion oppnid φ¬AOA

Proof

Step Hyp Ref Expression
1 hpg.p P=BaseG
2 hpg.d -˙=distG
3 hpg.i I=ItvG
4 hpg.o O=ab|aPDbPDtDtaIb
5 opphl.l L=Line𝒢G
6 opphl.d φDranL
7 opphl.g φG𝒢Tarski
8 oppnid.1 φAP
9 7 ad3antrrr φAOAtDtAIAG𝒢Tarski
10 8 ad3antrrr φAOAtDtAIAAP
11 6 ad3antrrr φAOAtDtAIADranL
12 simplr φAOAtDtAIAtD
13 1 5 3 9 11 12 tglnpt φAOAtDtAIAtP
14 simpr φAOAtDtAIAtAIA
15 1 2 3 9 10 13 14 axtgbtwnid φAOAtDtAIAA=t
16 15 12 eqeltrd φAOAtDtAIAAD
17 1 2 3 4 8 8 islnopp φAOA¬AD¬ADtDtAIA
18 17 simplbda φAOAtDtAIA
19 16 18 r19.29a φAOAAD
20 17 simprbda φAOA¬AD¬AD
21 20 simpld φAOA¬AD
22 19 21 pm2.65da φ¬AOA