Theorem oppnid

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

	Ref	Expression
Hypotheses	hpg.p	|- P = ( Base ` G )
	hpg.d	|- .- = ( dist ` G )
	hpg.i	|- I = ( Itv ` G )
	hpg.o	|- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }
	opphl.l	|- L = ( LineG ` G )
	opphl.d	|- ( ph -> D e. ran L )
	opphl.g	|- ( ph -> G e. TarskiG )
	oppnid.1	|- ( ph -> A e. P )
Assertion	oppnid	|- ( ph -> -. A O A )

Proof

Step	Hyp	Ref	Expression
1		hpg.p	|- P = ( Base ` G )
2		hpg.d	|- .- = ( dist ` G )
3		hpg.i	|- I = ( Itv ` G )
4		hpg.o	|- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }
5		opphl.l	|- L = ( LineG ` G )
6		opphl.d	|- ( ph -> D e. ran L )
7		opphl.g	|- ( ph -> G e. TarskiG )
8		oppnid.1	|- ( ph -> A e. P )
9	7	ad3antrrr	|- ( ( ( ( ph /\ A O A ) /\ t e. D ) /\ t e. ( A I A ) ) -> G e. TarskiG )
10	8	ad3antrrr	|- ( ( ( ( ph /\ A O A ) /\ t e. D ) /\ t e. ( A I A ) ) -> A e. P )
11	6	ad3antrrr	|- ( ( ( ( ph /\ A O A ) /\ t e. D ) /\ t e. ( A I A ) ) -> D e. ran L )
12		simplr	|- ( ( ( ( ph /\ A O A ) /\ t e. D ) /\ t e. ( A I A ) ) -> t e. D )
13	1 5 3 9 11 12	tglnpt	|- ( ( ( ( ph /\ A O A ) /\ t e. D ) /\ t e. ( A I A ) ) -> t e. P )
14		simpr	|- ( ( ( ( ph /\ A O A ) /\ t e. D ) /\ t e. ( A I A ) ) -> t e. ( A I A ) )
15	1 2 3 9 10 13 14	axtgbtwnid	|- ( ( ( ( ph /\ A O A ) /\ t e. D ) /\ t e. ( A I A ) ) -> A = t )
16	15 12	eqeltrd	|- ( ( ( ( ph /\ A O A ) /\ t e. D ) /\ t e. ( A I A ) ) -> A e. D )
17	1 2 3 4 8 8	islnopp	|- ( ph -> ( A O A <-> ( ( -. A e. D /\ -. A e. D ) /\ E. t e. D t e. ( A I A ) ) ) )
18	17	simplbda	|- ( ( ph /\ A O A ) -> E. t e. D t e. ( A I A ) )
19	16 18	r19.29a	|- ( ( ph /\ A O A ) -> A e. D )
20	17	simprbda	|- ( ( ph /\ A O A ) -> ( -. A e. D /\ -. A e. D ) )
21	20	simpld	|- ( ( ph /\ A O A ) -> -. A e. D )
22	19 21	pm2.65da	|- ( ph -> -. A O A )