![]() |
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 25774 | . 2 ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐵 − 𝐴)) |
9 | tgcgrcomlr.c | . . 3 ⊢ (𝜑 → 𝐶 ∈ 𝑃) | |
10 | tgcgrcomlr.d | . . 3 ⊢ (𝜑 → 𝐷 ∈ 𝑃) | |
11 | 2, 3, 4, 5, 9, 10 | axtgcgrrflx 25774 | . 2 ⊢ (𝜑 → (𝐶 − 𝐷) = (𝐷 − 𝐶)) |
12 | 1, 8, 11 | 3eqtr3d 2869 | 1 ⊢ (𝜑 → (𝐵 − 𝐴) = (𝐷 − 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1658 ∈ wcel 2166 ‘cfv 6123 (class class class)co 6905 Basecbs 16222 distcds 16314 TarskiGcstrkg 25742 Itvcitv 25748 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2803 ax-nul 5013 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2605 df-eu 2640 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-ral 3122 df-rex 3123 df-rab 3126 df-v 3416 df-sbc 3663 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-nul 4145 df-if 4307 df-sn 4398 df-pr 4400 df-op 4404 df-uni 4659 df-br 4874 df-iota 6086 df-fv 6131 df-ov 6908 df-trkgc 25760 df-trkg 25765 |
This theorem is referenced by: tgcgrextend 25797 tgifscgr 25820 tgcgrsub 25821 iscgrglt 25826 trgcgrg 25827 tgcgrxfr 25830 cgr3swap12 25835 cgr3swap23 25836 tgbtwnxfr 25842 lnext 25879 tgbtwnconn1lem1 25884 tgbtwnconn1lem2 25885 tgbtwnconn1lem3 25886 tgbtwnconn1 25887 legov2 25898 legtri3 25902 legbtwn 25906 tgcgrsub2 25907 miriso 25982 mircgrextend 25994 mirtrcgr 25995 miduniq 25997 colmid 26000 symquadlem 26001 krippenlem 26002 midexlem 26004 ragcom 26010 ragflat 26016 ragcgr 26019 footex 26030 colperpexlem1 26039 mideulem2 26043 opphllem 26044 opphllem3 26058 lmiisolem 26105 hypcgrlem1 26108 trgcopy 26113 trgcopyeulem 26114 iscgra1 26119 cgracgr 26127 cgraswap 26129 cgrcgra 26130 cgracom 26131 cgratr 26132 dfcgra2 26138 sacgrOLD 26140 acopy 26142 acopyeu 26143 cgrg3col4 26152 tgsas1 26153 tgsas3 26156 tgasa1 26157 |
Copyright terms: Public domain | W3C validator |