Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > tgcgrcomlr | Structured version Visualization version GIF version |
Description: Congruence commutes on both sides. (Contributed by Thierry Arnoux, 23-Mar-2019.) |
Ref | Expression |
---|---|
tkgeom.p | ⊢ 𝑃 = (Base‘𝐺) |
tkgeom.d | ⊢ − = (dist‘𝐺) |
tkgeom.i | ⊢ 𝐼 = (Itv‘𝐺) |
tkgeom.g | ⊢ (𝜑 → 𝐺 ∈ TarskiG) |
tgcgrcomlr.a | ⊢ (𝜑 → 𝐴 ∈ 𝑃) |
tgcgrcomlr.b | ⊢ (𝜑 → 𝐵 ∈ 𝑃) |
tgcgrcomlr.c | ⊢ (𝜑 → 𝐶 ∈ 𝑃) |
tgcgrcomlr.d | ⊢ (𝜑 → 𝐷 ∈ 𝑃) |
tgcgrcomlr.6 | ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐶 − 𝐷)) |
Ref | Expression |
---|---|
tgcgrcomlr | ⊢ (𝜑 → (𝐵 − 𝐴) = (𝐷 − 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tgcgrcomlr.6 | . 2 ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐶 − 𝐷)) | |
2 | tkgeom.p | . . 3 ⊢ 𝑃 = (Base‘𝐺) | |
3 | tkgeom.d | . . 3 ⊢ − = (dist‘𝐺) | |
4 | tkgeom.i | . . 3 ⊢ 𝐼 = (Itv‘𝐺) | |
5 | tkgeom.g | . . 3 ⊢ (𝜑 → 𝐺 ∈ TarskiG) | |
6 | tgcgrcomlr.a | . . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑃) | |
7 | tgcgrcomlr.b | . . 3 ⊢ (𝜑 → 𝐵 ∈ 𝑃) | |
8 | 2, 3, 4, 5, 6, 7 | axtgcgrrflx 26251 | . 2 ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐵 − 𝐴)) |
9 | tgcgrcomlr.c | . . 3 ⊢ (𝜑 → 𝐶 ∈ 𝑃) | |
10 | tgcgrcomlr.d | . . 3 ⊢ (𝜑 → 𝐷 ∈ 𝑃) | |
11 | 2, 3, 4, 5, 9, 10 | axtgcgrrflx 26251 | . 2 ⊢ (𝜑 → (𝐶 − 𝐷) = (𝐷 − 𝐶)) |
12 | 1, 8, 11 | 3eqtr3d 2867 | 1 ⊢ (𝜑 → (𝐵 − 𝐴) = (𝐷 − 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1536 ∈ wcel 2113 ‘cfv 6358 (class class class)co 7159 Basecbs 16486 distcds 16577 TarskiGcstrkg 26219 Itvcitv 26225 |
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 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 ax-nul 5213 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-mo 2621 df-eu 2653 df-clab 2803 df-cleq 2817 df-clel 2896 df-nfc 2966 df-ral 3146 df-rex 3147 df-rab 3150 df-v 3499 df-sbc 3776 df-dif 3942 df-un 3944 df-in 3946 df-ss 3955 df-nul 4295 df-if 4471 df-sn 4571 df-pr 4573 df-op 4577 df-uni 4842 df-br 5070 df-iota 6317 df-fv 6366 df-ov 7162 df-trkgc 26237 df-trkg 26242 |
This theorem is referenced by: tgcgrextend 26274 tgifscgr 26297 tgcgrsub 26298 iscgrglt 26303 trgcgrg 26304 tgcgrxfr 26307 cgr3swap12 26312 cgr3swap23 26313 tgbtwnxfr 26319 lnext 26356 tgbtwnconn1lem1 26361 tgbtwnconn1lem2 26362 tgbtwnconn1lem3 26363 tgbtwnconn1 26364 legov2 26375 legtri3 26379 legbtwn 26383 tgcgrsub2 26384 miriso 26459 mircgrextend 26471 mirtrcgr 26472 miduniq 26474 colmid 26477 symquadlem 26478 krippenlem 26479 midexlem 26481 ragcom 26487 ragflat 26493 ragcgr 26496 footexALT 26507 footexlem1 26508 footexlem2 26509 colperpexlem1 26519 mideulem2 26523 opphllem 26524 opphllem3 26538 lmiisolem 26585 hypcgrlem1 26588 trgcopy 26593 trgcopyeulem 26594 iscgra1 26599 cgracgr 26607 cgraswap 26609 cgrcgra 26610 cgracom 26611 cgratr 26612 flatcgra 26613 dfcgra2 26619 acopy 26622 acopyeu 26623 cgrg3col4 26642 tgsas1 26643 tgsas3 26646 tgasa1 26647 |
Copyright terms: Public domain | W3C validator |