Theorem plngmiropp

Description: Given a line A and a point X not on A , then a point Y on the plane defined by A and X is either opposite to X , or opposite to the mirror point of X by any point Z of A . (Contributed by Thierry Arnoux, 5-Jul-2026)

	Ref	Expression
Hypotheses	plngmiropp.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	plngmiropp.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	plngmiropp.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	plngmiropp.e	⊢ 𝐸 = ( hlG ‘ 𝐺 )
	plngmiropp.s	⊢ 𝑆 = ( pInvG ‘ 𝐺 )
	plngmiropp.m	⊢ 𝑀 = ( 𝑆 ‘ 𝑍 )
	plngmiropp.o	⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
	plngmiropp.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	plngmiropp.a	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
	plngmiropp.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑃 ∖ 𝐴 ) )
	plngmiropp.y	⊢ ( 𝜑 → 𝑌 ∈ ( ( 𝐴 𝐸 𝑋 ) ∖ 𝐴 ) )
	plngmiropp.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐴 )
Assertion	plngmiropp	⊢ ( 𝜑 → ( 𝑋 𝑂 𝑌 ∨ ( 𝑀 ‘ 𝑋 ) 𝑂 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		plngmiropp.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		plngmiropp.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		plngmiropp.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
4		plngmiropp.e	⊢ 𝐸 = ( hlG ‘ 𝐺 )
5		plngmiropp.s	⊢ 𝑆 = ( pInvG ‘ 𝐺 )
6		plngmiropp.m	⊢ 𝑀 = ( 𝑆 ‘ 𝑍 )
7		plngmiropp.o	⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
8		plngmiropp.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
9		plngmiropp.a	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
10		plngmiropp.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑃 ∖ 𝐴 ) )
11		plngmiropp.y	⊢ ( 𝜑 → 𝑌 ∈ ( ( 𝐴 𝐸 𝑋 ) ∖ 𝐴 ) )
12		plngmiropp.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐴 )
13		eqid	⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
14	9	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 ) → 𝐴 ∈ ran 𝐿 )
15	8	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 ) → 𝐺 ∈ TarskiG )
16	11	eldifad	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐴 𝐸 𝑋 ) )
17	1 2 3 4 8 9 10 16	plngssp	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
18	17	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 ) → 𝑌 ∈ 𝑃 )
19	1 3 2 8 9 12	tglnpt	⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
20	10	eldifad	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
21	1 13 2 3 5 8 19 6 20	mircl	⊢ ( 𝜑 → ( 𝑀 ‘ 𝑋 ) ∈ 𝑃 )
22	21	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 ) → ( 𝑀 ‘ 𝑋 ) ∈ 𝑃 )
23	20	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 ) → 𝑋 ∈ 𝑃 )
24		simpr	⊢ ( ( 𝜑 ∧ 𝑌 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 ) → 𝑌 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 )
25	1 2 3 15 14 18 7 23 24	hpgcom	⊢ ( ( 𝜑 ∧ 𝑌 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 ) → 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑌 )
26	1 2 5 6 7 8 9 12 10 3	oppmir	⊢ ( 𝜑 → 𝑋 𝑂 ( 𝑀 ‘ 𝑋 ) )
27	1 2 3 7 8 9 20 17 21 26	lnopp2hpgb	⊢ ( 𝜑 → ( 𝑌 𝑂 ( 𝑀 ‘ 𝑋 ) ↔ 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑌 ) )
28	27	biimpar	⊢ ( ( 𝜑 ∧ 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑌 ) → 𝑌 𝑂 ( 𝑀 ‘ 𝑋 ) )
29	25 28	syldan	⊢ ( ( 𝜑 ∧ 𝑌 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 ) → 𝑌 𝑂 ( 𝑀 ‘ 𝑋 ) )
30	1 13 2 7 3 14 15 18 22 29	oppcom	⊢ ( ( 𝜑 ∧ 𝑌 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 ) → ( 𝑀 ‘ 𝑋 ) 𝑂 𝑌 )
31	9	adantr	⊢ ( ( 𝜑 ∧ 𝑌 𝑂 𝑋 ) → 𝐴 ∈ ran 𝐿 )
32	8	adantr	⊢ ( ( 𝜑 ∧ 𝑌 𝑂 𝑋 ) → 𝐺 ∈ TarskiG )
33	17	adantr	⊢ ( ( 𝜑 ∧ 𝑌 𝑂 𝑋 ) → 𝑌 ∈ 𝑃 )
34	20	adantr	⊢ ( ( 𝜑 ∧ 𝑌 𝑂 𝑋 ) → 𝑋 ∈ 𝑃 )
35		simpr	⊢ ( ( 𝜑 ∧ 𝑌 𝑂 𝑋 ) → 𝑌 𝑂 𝑋 )
36	1 13 2 7 3 31 32 33 34 35	oppcom	⊢ ( ( 𝜑 ∧ 𝑌 𝑂 𝑋 ) → 𝑋 𝑂 𝑌 )
37	1 2 3 4 8 9 10 7 17	elplng	⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝐴 𝐸 𝑋 ) ↔ ( 𝑌 ∈ 𝐴 ∨ 𝑌 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 ∨ 𝑌 𝑂 𝑋 ) ) )
38	16 37	mpbid	⊢ ( 𝜑 → ( 𝑌 ∈ 𝐴 ∨ 𝑌 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 ∨ 𝑌 𝑂 𝑋 ) )
39		3orass	⊢ ( ( 𝑌 ∈ 𝐴 ∨ 𝑌 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 ∨ 𝑌 𝑂 𝑋 ) ↔ ( 𝑌 ∈ 𝐴 ∨ ( 𝑌 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 ∨ 𝑌 𝑂 𝑋 ) ) )
40	38 39	sylib	⊢ ( 𝜑 → ( 𝑌 ∈ 𝐴 ∨ ( 𝑌 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 ∨ 𝑌 𝑂 𝑋 ) ) )
41	11	eldifbd	⊢ ( 𝜑 → ¬ 𝑌 ∈ 𝐴 )
42	40 41	orcnd	⊢ ( 𝜑 → ( 𝑌 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 ∨ 𝑌 𝑂 𝑋 ) )
43	30 36 42	orim12da	⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑋 ) 𝑂 𝑌 ∨ 𝑋 𝑂 𝑌 ) )
44	43	orcomd	⊢ ( 𝜑 → ( 𝑋 𝑂 𝑌 ∨ ( 𝑀 ‘ 𝑋 ) 𝑂 𝑌 ) )