Theorem oppmir

Description: The mirror point with regard to a point X on a line A lies on the other side of A . (Contributed by Thierry Arnoux, 5-Jul-2026)

	Ref	Expression
Hypotheses	oppmir.p	|- P = ( Base ` G )
	oppmir.i	|- I = ( Itv ` G )
	oppmir.s	|- S = ( pInvG ` G )
	oppmir.m	|- M = ( S ` X )
	oppmir.o	|- O = { <. a , b >. | ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) /\ E. t e. A t e. ( a I b ) ) }
	oppmir.g	|- ( ph -> G e. TarskiG )
	oppmir.a	|- ( ph -> A e. ran L )
	oppmir.x	|- ( ph -> X e. A )
	oppmir.y	|- ( ph -> Y e. ( P \ A ) )
	oppmir.1	|- L = ( LineG ` G )
Assertion	oppmir	|- ( ph -> Y O ( M ` Y ) )

Proof

Step	Hyp	Ref	Expression
1		oppmir.p	|- P = ( Base ` G )
2		oppmir.i	|- I = ( Itv ` G )
3		oppmir.s	|- S = ( pInvG ` G )
4		oppmir.m	|- M = ( S ` X )
5		oppmir.o	|- O = { <. a , b >. | ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) /\ E. t e. A t e. ( a I b ) ) }
6		oppmir.g	|- ( ph -> G e. TarskiG )
7		oppmir.a	|- ( ph -> A e. ran L )
8		oppmir.x	|- ( ph -> X e. A )
9		oppmir.y	|- ( ph -> Y e. ( P \ A ) )
10		oppmir.1	|- L = ( LineG ` G )
11		eqid	|- ( dist ` G ) = ( dist ` G )
12	9	eldifad	|- ( ph -> Y e. P )
13	1 10 2 6 7 8	tglnpt	|- ( ph -> X e. P )
14	1 11 2 10 3 6 13 4 12	mircl	|- ( ph -> ( M ` Y ) e. P )
15	9	eldifbd	|- ( ph -> -. Y e. A )
16	1 11 2 10 3 6 13 4 12	mirmir	|- ( ph -> ( M ` ( M ` Y ) ) = Y )
17	16	adantr	|- ( ( ph /\ ( M ` Y ) e. A ) -> ( M ` ( M ` Y ) ) = Y )
18	6	adantr	|- ( ( ph /\ ( M ` Y ) e. A ) -> G e. TarskiG )
19	7	adantr	|- ( ( ph /\ ( M ` Y ) e. A ) -> A e. ran L )
20	8	adantr	|- ( ( ph /\ ( M ` Y ) e. A ) -> X e. A )
21		simpr	|- ( ( ph /\ ( M ` Y ) e. A ) -> ( M ` Y ) e. A )
22	1 11 2 10 3 18 4 19 20 21	mirln	|- ( ( ph /\ ( M ` Y ) e. A ) -> ( M ` ( M ` Y ) ) e. A )
23	17 22	eqeltrrd	|- ( ( ph /\ ( M ` Y ) e. A ) -> Y e. A )
24	15 23	mtand	|- ( ph -> -. ( M ` Y ) e. A )
25	1 11 2 10 3 6 13 4 12	mirbtwn	|- ( ph -> X e. ( ( M ` Y ) I Y ) )
26	1 11 2 6 14 13 12 25	tgbtwncom	|- ( ph -> X e. ( Y I ( M ` Y ) ) )
27	1 11 2 5 12 14 8 15 24 26	islnoppd	|- ( ph -> Y O ( M ` Y ) )