plngmiropp - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > plngmiropp		Structured version Visualization version GIF version

Theorem plngmiropp 29057

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

**Hypotheses**
Ref	Expression
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**
Ref	Expression
plngmiropp	⊢ (𝜑 → (𝑋𝑂𝑌 ∨ (𝑀‘𝑋)𝑂𝑌))

Distinct variable groups: 𝐴,𝑎,𝑏,𝑡 𝐺,𝑎,𝑏,𝑡 𝐼,𝑎,𝑏,𝑡 𝐿,𝑎,𝑏,𝑡 𝑀,𝑎,𝑏,𝑡 𝑂,𝑎,𝑏,𝑡 𝑃,𝑎,𝑏,𝑡 𝑋,𝑎,𝑏,𝑡 𝑌,𝑎,𝑏,𝑡 𝑡,𝑍 𝜑,𝑡 Allowed substitution hints: 𝜑(𝑎,𝑏) 𝑆(𝑡,𝑎,𝑏) 𝐸(𝑡,𝑎,𝑏) 𝑍(𝑎,𝑏)

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 ∨ wo 860 ∨ w3o 1102 = wceq 1570 ∈ wcel 2143 ∃wrex 3089 ∖ cdif 3903 class class class wbr 5110 {copab 5174 ran crn 5664 ‘cfv 6538 (class class class)co 7412 Basecbs 17270 distcds 17320 TarskiGcstrkg 28677 Itvcitv 28683 LineGclng 28684 pInvGcmir 28910 hpGchpg 29020 hlGcplng 29036

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5239 ax-sep 5258 ax-nul 5270 ax-pow 5338 ax-pr 5406 ax-un 7734 ax-cnex 11157 ax-resscn 11158 ax-1cn 11159 ax-icn 11160 ax-addcl 11161 ax-addrcl 11162 ax-mulcl 11163 ax-mulrcl 11164 ax-mulcom 11165 ax-addass 11166 ax-mulass 11167 ax-distr 11168 ax-i2m1 11169 ax-1ne0 11170 ax-1rid 11171 ax-rnegex 11172 ax-rrecex 11173 ax-cnre 11174 ax-pre-lttri 11175 ax-pre-lttrn 11176 ax-pre-ltadd 11177 ax-pre-mulgt0 11178

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3746 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4288 df-if 4489 df-pw 4565 df-sn 4591 df-pr 4593 df-tp 4595 df-op 4597 df-uni 4874 df-int 4914 df-iun 4959 df-br 5111 df-opab 5175 df-mpt 5194 df-tr 5220 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7864 df-1st 7987 df-2nd 7988 df-frecs 8279 df-wrecs 8310 df-recs 8359 df-rdg 8398 df-1o 8454 df-oadd 8458 df-er 8695 df-map 8827 df-pm 8828 df-en 8945 df-dom 8946 df-sdom 8947 df-fin 8948 df-dju 9888 df-card 9926 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11444 df-neg 11445 df-nn 12235 df-2 12304 df-3 12305 df-n0 12506 df-xnn0 12579 df-z 12593 df-uz 12864 df-fz 13537 df-fzo 13685 df-hash 14369 df-word 14553 df-concat 14610 df-s1 14636 df-s2 14887 df-s3 14888 df-trkgc 28698 df-trkgb 28699 df-trkgcb 28700 df-trkgld 28702 df-trkg 28703 df-cgrg 28761 df-leg 28833 df-hlg 28851 df-mir 28911 df-rag 28955 df-perpg 28957 df-hpg 29021 df-plng 29037

This theorem is referenced by: prlngmolem2 29184

W3C validator