lmimot - Metamath Proof Explorer

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

Theorem lmimot 28732

Description: Line mirroring is a motion of the geometric space. Theorem 10.11 of [Schwabhauser] p. 90. (Contributed by Thierry Arnoux, 15-Dec-2019.)

**Hypotheses**
Ref	Expression
ismid.p	⊢ 𝑃 = (Base‘𝐺)
ismid.d	⊢ − = (dist‘𝐺)
ismid.i	⊢ 𝐼 = (Itv‘𝐺)
ismid.g	⊢ (𝜑 → 𝐺 ∈ TarskiG)
ismid.1	⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
lmif.m	⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷)
lmif.l	⊢ 𝐿 = (LineG‘𝐺)
lmif.d	⊢ (𝜑 → 𝐷 ∈ ran 𝐿)

**Assertion**
Ref	Expression
lmimot	⊢ (𝜑 → 𝑀 ∈ (𝐺Ismt𝐺))

Proof of Theorem lmimot Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ismid.p	. . 3 ⊢ 𝑃 = (Base‘𝐺)
2		ismid.d	. . 3 ⊢ − = (dist‘𝐺)
3		ismid.i	. . 3 ⊢ 𝐼 = (Itv‘𝐺)
4		ismid.g	. . 3 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
5		ismid.1	. . 3 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
6		lmif.m	. . 3 ⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷)
7		lmif.l	. . 3 ⊢ 𝐿 = (LineG‘𝐺)
8		lmif.d	. . 3 ⊢ (𝜑 → 𝐷 ∈ ran 𝐿)
9	1, 2, 3, 4, 5, 6, 7, 8	lmif1o 28729	. 2 ⊢ (𝜑 → 𝑀:𝑃–1-1-onto→𝑃)
10	4	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → 𝐺 ∈ TarskiG)
11	5	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → 𝐺Dim_TarskiG≥2)
12	8	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → 𝐷 ∈ ran 𝐿)
13		simprl 770	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → 𝑎 ∈ 𝑃)
14		simprr 772	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → 𝑏 ∈ 𝑃)
15	1, 2, 3, 10, 11, 6, 7, 12, 13, 14	lmiiso 28731	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)) → ((𝑀‘𝑎) − (𝑀‘𝑏)) = (𝑎 − 𝑏))
16	15	ralrimivva 3182	. 2 ⊢ (𝜑 → ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ((𝑀‘𝑎) − (𝑀‘𝑏)) = (𝑎 − 𝑏))
17	1, 2	ismot 28469	. . 3 ⊢ (𝐺 ∈ TarskiG → (𝑀 ∈ (𝐺Ismt𝐺) ↔ (𝑀:𝑃–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ((𝑀‘𝑎) − (𝑀‘𝑏)) = (𝑎 − 𝑏))))
18	4, 17	syl 17	. 2 ⊢ (𝜑 → (𝑀 ∈ (𝐺Ismt𝐺) ↔ (𝑀:𝑃–1-1-onto→𝑃 ∧ ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ((𝑀‘𝑎) − (𝑀‘𝑏)) = (𝑎 − 𝑏))))
19	9, 16, 18	mpbir2and 713	1 ⊢ (𝜑 → 𝑀 ∈ (𝐺Ismt𝐺))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ∀wral 3046 class class class wbr 5115 ran crn 5647 –1-1-onto→wf1o 6518 ‘cfv 6519 (class class class)co 7394 2c2 12252 Basecbs 17185 distcds 17235 TarskiGcstrkg 28361 Dim_TarskiG≥cstrkgld 28365 Itvcitv 28367 LineGclng 28368 Ismtcismt 28466 lInvGclmi 28707

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-rep 5242 ax-sep 5259 ax-nul 5269 ax-pow 5328 ax-pr 5395 ax-un 7718 ax-cnex 11142 ax-resscn 11143 ax-1cn 11144 ax-icn 11145 ax-addcl 11146 ax-addrcl 11147 ax-mulcl 11148 ax-mulrcl 11149 ax-mulcom 11150 ax-addass 11151 ax-mulass 11152 ax-distr 11153 ax-i2m1 11154 ax-1ne0 11155 ax-1rid 11156 ax-rnegex 11157 ax-rrecex 11158 ax-cnre 11159 ax-pre-lttri 11160 ax-pre-lttrn 11161 ax-pre-ltadd 11162 ax-pre-mulgt0 11163

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2880 df-ne 2928 df-nel 3032 df-ral 3047 df-rex 3056 df-rmo 3357 df-reu 3358 df-rab 3412 df-v 3457 df-sbc 3762 df-csb 3871 df-dif 3925 df-un 3927 df-in 3929 df-ss 3939 df-pss 3942 df-nul 4305 df-if 4497 df-pw 4573 df-sn 4598 df-pr 4600 df-tp 4602 df-op 4604 df-uni 4880 df-int 4919 df-iun 4965 df-br 5116 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5541 df-eprel 5546 df-po 5554 df-so 5555 df-fr 5599 df-we 5601 df-xp 5652 df-rel 5653 df-cnv 5654 df-co 5655 df-dm 5656 df-rn 5657 df-res 5658 df-ima 5659 df-pred 6282 df-ord 6343 df-on 6344 df-lim 6345 df-suc 6346 df-iota 6472 df-fun 6521 df-fn 6522 df-f 6523 df-f1 6524 df-fo 6525 df-f1o 6526 df-fv 6527 df-riota 7351 df-ov 7397 df-oprab 7398 df-mpo 7399 df-om 7851 df-1st 7977 df-2nd 7978 df-frecs 8269 df-wrecs 8300 df-recs 8349 df-rdg 8387 df-1o 8443 df-oadd 8447 df-er 8682 df-map 8805 df-pm 8806 df-en 8923 df-dom 8924 df-sdom 8925 df-fin 8926 df-dju 9872 df-card 9910 df-pnf 11228 df-mnf 11229 df-xr 11230 df-ltxr 11231 df-le 11232 df-sub 11425 df-neg 11426 df-nn 12198 df-2 12260 df-3 12261 df-n0 12459 df-xnn0 12532 df-z 12546 df-uz 12810 df-fz 13482 df-fzo 13629 df-hash 14306 df-word 14489 df-concat 14546 df-s1 14571 df-s2 14824 df-s3 14825 df-trkgc 28382 df-trkgb 28383 df-trkgcb 28384 df-trkgld 28386 df-trkg 28387 df-cgrg 28445 df-ismt 28467 df-leg 28517 df-mir 28587 df-rag 28628 df-perpg 28630 df-mid 28708 df-lmi 28709

This theorem is referenced by: hypcgrlem2 28734

W3C validator