![]() |
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 28484 | . 2 ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐵 − 𝐴)) |
9 | tgcgrcomlr.c | . . 3 ⊢ (𝜑 → 𝐶 ∈ 𝑃) | |
10 | tgcgrcomlr.d | . . 3 ⊢ (𝜑 → 𝐷 ∈ 𝑃) | |
11 | 2, 3, 4, 5, 9, 10 | axtgcgrrflx 28484 | . 2 ⊢ (𝜑 → (𝐶 − 𝐷) = (𝐷 − 𝐶)) |
12 | 1, 8, 11 | 3eqtr3d 2782 | 1 ⊢ (𝜑 → (𝐵 − 𝐴) = (𝐷 − 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1536 ∈ wcel 2105 ‘cfv 6562 (class class class)co 7430 Basecbs 17244 distcds 17306 TarskiGcstrkg 28449 Itvcitv 28455 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-ext 2705 ax-nul 5311 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-ne 2938 df-ral 3059 df-rab 3433 df-v 3479 df-sbc 3791 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-nul 4339 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4912 df-br 5148 df-iota 6515 df-fv 6570 df-ov 7433 df-trkgc 28470 df-trkg 28475 |
This theorem is referenced by: tgcgrextend 28507 tgifscgr 28530 tgcgrsub 28531 iscgrglt 28536 trgcgrg 28537 tgcgrxfr 28540 cgr3swap12 28545 cgr3swap23 28546 tgbtwnxfr 28552 lnext 28589 tgbtwnconn1lem1 28594 tgbtwnconn1lem2 28595 tgbtwnconn1lem3 28596 tgbtwnconn1 28597 legov2 28608 legtri3 28612 legbtwn 28616 tgcgrsub2 28617 miriso 28692 mircgrextend 28704 mirtrcgr 28705 miduniq 28707 colmid 28710 symquadlem 28711 krippenlem 28712 midexlem 28714 ragcom 28720 ragflat 28726 ragcgr 28729 footexALT 28740 footexlem1 28741 footexlem2 28742 colperpexlem1 28752 mideulem2 28756 opphllem 28757 opphllem3 28771 lmiisolem 28818 hypcgrlem1 28821 trgcopy 28826 trgcopyeulem 28827 iscgra1 28832 cgracgr 28840 cgraswap 28842 cgrcgra 28843 cgracom 28844 cgratr 28845 flatcgra 28846 dfcgra2 28852 acopy 28855 acopyeu 28856 cgrg3col4 28875 tgsas1 28876 tgsas3 28879 tgasa1 28880 |
Copyright terms: Public domain | W3C validator |