Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > lmiiso | Structured version Visualization version GIF version |
Description: The line mirroring function is an isometry, i.e. it is conserves congruence. Because it is also a bijection, it is also a motion. Theorem 10.10 of [Schwabhauser] p. 89. (Contributed by Thierry Arnoux, 11-Dec-2019.) |
Ref | Expression |
---|---|
ismid.p | ⊢ 𝑃 = (Base‘𝐺) |
ismid.d | ⊢ − = (dist‘𝐺) |
ismid.i | ⊢ 𝐼 = (Itv‘𝐺) |
ismid.g | ⊢ (𝜑 → 𝐺 ∈ TarskiG) |
ismid.1 | ⊢ (𝜑 → 𝐺DimTarskiG≥2) |
lmif.m | ⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷) |
lmif.l | ⊢ 𝐿 = (LineG‘𝐺) |
lmif.d | ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) |
lmiiso.1 | ⊢ (𝜑 → 𝐴 ∈ 𝑃) |
lmiiso.2 | ⊢ (𝜑 → 𝐵 ∈ 𝑃) |
Ref | Expression |
---|---|
lmiiso | ⊢ (𝜑 → ((𝑀‘𝐴) − (𝑀‘𝐵)) = (𝐴 − 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ismid.p | . 2 ⊢ 𝑃 = (Base‘𝐺) | |
2 | ismid.d | . 2 ⊢ − = (dist‘𝐺) | |
3 | ismid.i | . 2 ⊢ 𝐼 = (Itv‘𝐺) | |
4 | ismid.g | . 2 ⊢ (𝜑 → 𝐺 ∈ TarskiG) | |
5 | ismid.1 | . 2 ⊢ (𝜑 → 𝐺DimTarskiG≥2) | |
6 | lmif.m | . 2 ⊢ 𝑀 = ((lInvG‘𝐺)‘𝐷) | |
7 | lmif.l | . 2 ⊢ 𝐿 = (LineG‘𝐺) | |
8 | lmif.d | . 2 ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) | |
9 | lmiiso.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ 𝑃) | |
10 | lmiiso.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ 𝑃) | |
11 | eqid 2759 | . 2 ⊢ ((pInvG‘𝐺)‘((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐵(midG‘𝐺)(𝑀‘𝐵)))) = ((pInvG‘𝐺)‘((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐵(midG‘𝐺)(𝑀‘𝐵)))) | |
12 | eqid 2759 | . 2 ⊢ ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐵(midG‘𝐺)(𝑀‘𝐵))) = ((𝐴(midG‘𝐺)(𝑀‘𝐴))(midG‘𝐺)(𝐵(midG‘𝐺)(𝑀‘𝐵))) | |
13 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 | lmiisolem 26704 | 1 ⊢ (𝜑 → ((𝑀‘𝐴) − (𝑀‘𝐵)) = (𝐴 − 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1539 ∈ wcel 2112 class class class wbr 5037 ran crn 5530 ‘cfv 6341 (class class class)co 7157 2c2 11743 Basecbs 16556 distcds 16647 TarskiGcstrkg 26338 DimTarskiG≥cstrkgld 26342 Itvcitv 26344 LineGclng 26345 pInvGcmir 26560 midGcmid 26680 lInvGclmi 26681 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2159 ax-12 2176 ax-ext 2730 ax-rep 5161 ax-sep 5174 ax-nul 5181 ax-pow 5239 ax-pr 5303 ax-un 7466 ax-cnex 10645 ax-resscn 10646 ax-1cn 10647 ax-icn 10648 ax-addcl 10649 ax-addrcl 10650 ax-mulcl 10651 ax-mulrcl 10652 ax-mulcom 10653 ax-addass 10654 ax-mulass 10655 ax-distr 10656 ax-i2m1 10657 ax-1ne0 10658 ax-1rid 10659 ax-rnegex 10660 ax-rrecex 10661 ax-cnre 10662 ax-pre-lttri 10663 ax-pre-lttrn 10664 ax-pre-ltadd 10665 ax-pre-mulgt0 10666 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2071 df-mo 2558 df-eu 2589 df-clab 2737 df-cleq 2751 df-clel 2831 df-nfc 2902 df-ne 2953 df-nel 3057 df-ral 3076 df-rex 3077 df-reu 3078 df-rmo 3079 df-rab 3080 df-v 3412 df-sbc 3700 df-csb 3809 df-dif 3864 df-un 3866 df-in 3868 df-ss 3878 df-pss 3880 df-nul 4229 df-if 4425 df-pw 4500 df-sn 4527 df-pr 4529 df-tp 4531 df-op 4533 df-uni 4803 df-int 4843 df-iun 4889 df-br 5038 df-opab 5100 df-mpt 5118 df-tr 5144 df-id 5435 df-eprel 5440 df-po 5448 df-so 5449 df-fr 5488 df-we 5490 df-xp 5535 df-rel 5536 df-cnv 5537 df-co 5538 df-dm 5539 df-rn 5540 df-res 5541 df-ima 5542 df-pred 6132 df-ord 6178 df-on 6179 df-lim 6180 df-suc 6181 df-iota 6300 df-fun 6343 df-fn 6344 df-f 6345 df-f1 6346 df-fo 6347 df-f1o 6348 df-fv 6349 df-riota 7115 df-ov 7160 df-oprab 7161 df-mpo 7162 df-om 7587 df-1st 7700 df-2nd 7701 df-wrecs 7964 df-recs 8025 df-rdg 8063 df-1o 8119 df-oadd 8123 df-er 8306 df-map 8425 df-pm 8426 df-en 8542 df-dom 8543 df-sdom 8544 df-fin 8545 df-dju 9377 df-card 9415 df-pnf 10729 df-mnf 10730 df-xr 10731 df-ltxr 10732 df-le 10733 df-sub 10924 df-neg 10925 df-nn 11689 df-2 11751 df-3 11752 df-n0 11949 df-xnn0 12021 df-z 12035 df-uz 12297 df-fz 12954 df-fzo 13097 df-hash 13755 df-word 13928 df-concat 13984 df-s1 14011 df-s2 14271 df-s3 14272 df-trkgc 26356 df-trkgb 26357 df-trkgcb 26358 df-trkgld 26360 df-trkg 26361 df-cgrg 26419 df-leg 26491 df-mir 26561 df-rag 26602 df-perpg 26604 df-mid 26682 df-lmi 26683 |
This theorem is referenced by: lmimot 26706 hypcgrlem1 26707 hypcgrlem2 26708 trgcopyeulem 26713 |
Copyright terms: Public domain | W3C validator |