![]() |
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 28343 | . 2 ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐵 − 𝐴)) |
9 | tgcgrcomlr.c | . . 3 ⊢ (𝜑 → 𝐶 ∈ 𝑃) | |
10 | tgcgrcomlr.d | . . 3 ⊢ (𝜑 → 𝐷 ∈ 𝑃) | |
11 | 2, 3, 4, 5, 9, 10 | axtgcgrrflx 28343 | . 2 ⊢ (𝜑 → (𝐶 − 𝐷) = (𝐷 − 𝐶)) |
12 | 1, 8, 11 | 3eqtr3d 2773 | 1 ⊢ (𝜑 → (𝐵 − 𝐴) = (𝐷 − 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1533 ∈ wcel 2098 ‘cfv 6549 (class class class)co 7419 Basecbs 17188 distcds 17250 TarskiGcstrkg 28308 Itvcitv 28314 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 ax-nul 5307 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-ne 2930 df-ral 3051 df-rab 3419 df-v 3463 df-sbc 3774 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-br 5150 df-iota 6501 df-fv 6557 df-ov 7422 df-trkgc 28329 df-trkg 28334 |
This theorem is referenced by: tgcgrextend 28366 tgifscgr 28389 tgcgrsub 28390 iscgrglt 28395 trgcgrg 28396 tgcgrxfr 28399 cgr3swap12 28404 cgr3swap23 28405 tgbtwnxfr 28411 lnext 28448 tgbtwnconn1lem1 28453 tgbtwnconn1lem2 28454 tgbtwnconn1lem3 28455 tgbtwnconn1 28456 legov2 28467 legtri3 28471 legbtwn 28475 tgcgrsub2 28476 miriso 28551 mircgrextend 28563 mirtrcgr 28564 miduniq 28566 colmid 28569 symquadlem 28570 krippenlem 28571 midexlem 28573 ragcom 28579 ragflat 28585 ragcgr 28588 footexALT 28599 footexlem1 28600 footexlem2 28601 colperpexlem1 28611 mideulem2 28615 opphllem 28616 opphllem3 28630 lmiisolem 28677 hypcgrlem1 28680 trgcopy 28685 trgcopyeulem 28686 iscgra1 28691 cgracgr 28699 cgraswap 28701 cgrcgra 28702 cgracom 28703 cgratr 28704 flatcgra 28705 dfcgra2 28711 acopy 28714 acopyeu 28715 cgrg3col4 28734 tgsas1 28735 tgsas3 28738 tgasa1 28739 |
Copyright terms: Public domain | W3C validator |