dfcgrg2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > dfcgrg2		Structured version Visualization version GIF version

Theorem dfcgrg2 29020

Description: Congruence for two triangles can also be defined as congruence of sides and angles (6 parts). This is often the actual textbook definition of triangle congruence, see for example https://en.wikipedia.org/wiki/Congruence_(geometry)#Congruence_of_triangles. With this definition, the "SSS" congruence theorem has an additional part, namely, that triangle congruence implies congruence of the sides (which means equality of the lengths). Because our development of elementary geometry strives to closely follow Schwabhaeuser's, our original definition of shape congruence, df-cgrg 28668, already covers that part: see trgcgr 28673. This theorem is also named "CPCTC", which stands for "Corresponding Parts of Congruent Triangles are Congruent", see https://en.wikipedia.org/wiki/Congruence_(geometry)#CPCTC 28673. (Contributed by Thierry Arnoux, 18-Jan-2023.)

**Hypotheses**
Ref	Expression
dfcgrg2.p	⊢ 𝑃 = (Base‘𝐺)
dfcgrg2.m	⊢ − = (dist‘𝐺)
dfcgrg2.g	⊢ (𝜑 → 𝐺 ∈ TarskiG)
dfcgrg2.a	⊢ (𝜑 → 𝐴 ∈ 𝑃)
dfcgrg2.b	⊢ (𝜑 → 𝐵 ∈ 𝑃)
dfcgrg2.c	⊢ (𝜑 → 𝐶 ∈ 𝑃)
dfcgrg2.d	⊢ (𝜑 → 𝐷 ∈ 𝑃)
dfcgrg2.e	⊢ (𝜑 → 𝐸 ∈ 𝑃)
dfcgrg2.f	⊢ (𝜑 → 𝐹 ∈ 𝑃)
dfcgrg2.1	⊢ (𝜑 → 𝐴 ≠ 𝐵)
dfcgrg2.2	⊢ (𝜑 → 𝐵 ≠ 𝐶)
dfcgrg2.3	⊢ (𝜑 → 𝐶 ≠ 𝐴)

**Assertion**
Ref	Expression
dfcgrg2	⊢ (𝜑 → (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩ ↔ (((𝐴 − 𝐵) = (𝐷 − 𝐸) ∧ (𝐵 − 𝐶) = (𝐸 − 𝐹) ∧ (𝐶 − 𝐴) = (𝐹 − 𝐷)) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ ⟨“𝐶𝐴𝐵”⟩(cgrA‘𝐺)⟨“𝐹𝐷𝐸”⟩ ∧ ⟨“𝐵𝐶𝐴”⟩(cgrA‘𝐺)⟨“𝐸𝐹𝐷”⟩))))

**Proof of Theorem dfcgrg2**
Step	Hyp	Ref	Expression
1		dfcgrg2.p	. . . . . 6 ⊢ 𝑃 = (Base‘𝐺)
2		dfcgrg2.m	. . . . . 6 ⊢ − = (dist‘𝐺)
3		eqid 2761	. . . . . 6 ⊢ (Itv‘𝐺) = (Itv‘𝐺)
4		dfcgrg2.g	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
5	4	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐺 ∈ TarskiG)
6		dfcgrg2.a	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
7	6	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐴 ∈ 𝑃)
8		dfcgrg2.b	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
9	8	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐵 ∈ 𝑃)
10		dfcgrg2.c	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
11	10	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐶 ∈ 𝑃)
12		dfcgrg2.d	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ 𝑃)
13	12	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐷 ∈ 𝑃)
14		dfcgrg2.e	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ 𝑃)
15	14	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐸 ∈ 𝑃)
16		dfcgrg2.f	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ 𝑃)
17	16	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐹 ∈ 𝑃)
18		eqid 2761	. . . . . . . . 9 ⊢ (cgrG‘𝐺) = (cgrG‘𝐺)
19	1, 2, 18, 4, 6, 8, 10, 12, 14, 16	trgcgrg 28672	. . . . . . . 8 ⊢ (𝜑 → (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩ ↔ ((𝐴 − 𝐵) = (𝐷 − 𝐸) ∧ (𝐵 − 𝐶) = (𝐸 − 𝐹) ∧ (𝐶 − 𝐴) = (𝐹 − 𝐷))))
20	19	biimpa 480	. . . . . . 7 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩) → ((𝐴 − 𝐵) = (𝐷 − 𝐸) ∧ (𝐵 − 𝐶) = (𝐸 − 𝐹) ∧ (𝐶 − 𝐴) = (𝐹 − 𝐷)))
21	20	simp1d 1154	. . . . . 6 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩) → (𝐴 − 𝐵) = (𝐷 − 𝐸))
22	20	simp2d 1155	. . . . . 6 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩) → (𝐵 − 𝐶) = (𝐸 − 𝐹))
23	20	simp3d 1156	. . . . . 6 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩) → (𝐶 − 𝐴) = (𝐹 − 𝐷))
24		dfcgrg2.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
25	24	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐴 ≠ 𝐵)
26		dfcgrg2.2	. . . . . . 7 ⊢ (𝜑 → 𝐵 ≠ 𝐶)
27	26	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐵 ≠ 𝐶)
28		dfcgrg2.3	. . . . . . 7 ⊢ (𝜑 → 𝐶 ≠ 𝐴)
29	28	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐶 ≠ 𝐴)
30	1, 2, 3, 5, 7, 9, 11, 13, 15, 17, 21, 22, 23, 25, 27, 29	tgsss1 29017	. . . . 5 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
31	1, 2, 3, 5, 11, 7, 9, 17, 13, 15, 23, 21, 22, 29, 25, 27	tgsss1 29017	. . . . 5 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩) → ⟨“𝐶𝐴𝐵”⟩(cgrA‘𝐺)⟨“𝐹𝐷𝐸”⟩)
32	1, 2, 3, 5, 9, 11, 7, 15, 17, 13, 22, 23, 21, 27, 29, 25	tgsss1 29017	. . . . 5 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩) → ⟨“𝐵𝐶𝐴”⟩(cgrA‘𝐺)⟨“𝐸𝐹𝐷”⟩)
33	30, 31, 32	3jca 1140	. . . 4 ⊢ ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩) → (⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ ⟨“𝐶𝐴𝐵”⟩(cgrA‘𝐺)⟨“𝐹𝐷𝐸”⟩ ∧ ⟨“𝐵𝐶𝐴”⟩(cgrA‘𝐺)⟨“𝐸𝐹𝐷”⟩))
34	33	ex 416	. . 3 ⊢ (𝜑 → (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩ → (⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ ⟨“𝐶𝐴𝐵”⟩(cgrA‘𝐺)⟨“𝐹𝐷𝐸”⟩ ∧ ⟨“𝐵𝐶𝐴”⟩(cgrA‘𝐺)⟨“𝐸𝐹𝐷”⟩)))
35	34	pm4.71d 569	. 2 ⊢ (𝜑 → (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩ ↔ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ (⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ ⟨“𝐶𝐴𝐵”⟩(cgrA‘𝐺)⟨“𝐹𝐷𝐸”⟩ ∧ ⟨“𝐵𝐶𝐴”⟩(cgrA‘𝐺)⟨“𝐸𝐹𝐷”⟩))))
36	19	anbi1d 640	. 2 ⊢ (𝜑 → ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ (⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ ⟨“𝐶𝐴𝐵”⟩(cgrA‘𝐺)⟨“𝐹𝐷𝐸”⟩ ∧ ⟨“𝐵𝐶𝐴”⟩(cgrA‘𝐺)⟨“𝐸𝐹𝐷”⟩)) ↔ (((𝐴 − 𝐵) = (𝐷 − 𝐸) ∧ (𝐵 − 𝐶) = (𝐸 − 𝐹) ∧ (𝐶 − 𝐴) = (𝐹 − 𝐷)) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ ⟨“𝐶𝐴𝐵”⟩(cgrA‘𝐺)⟨“𝐹𝐷𝐸”⟩ ∧ ⟨“𝐵𝐶𝐴”⟩(cgrA‘𝐺)⟨“𝐸𝐹𝐷”⟩))))
37	35, 36	bitrd 281	1 ⊢ (𝜑 → (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝐹”⟩ ↔ (((𝐴 − 𝐵) = (𝐷 − 𝐸) ∧ (𝐵 − 𝐶) = (𝐸 − 𝐹) ∧ (𝐶 − 𝐴) = (𝐹 − 𝐷)) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ∧ ⟨“𝐶𝐴𝐵”⟩(cgrA‘𝐺)⟨“𝐹𝐷𝐸”⟩ ∧ ⟨“𝐵𝐶𝐴”⟩(cgrA‘𝐺)⟨“𝐸𝐹𝐷”⟩))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 399 ∧ w3a 1097 = wceq 1559 ∈ wcel 2141 ≠ wne 2956 class class class wbr 5097 ‘cfv 6516 (class class class)co 7391 ⟨“cs3 14849 Basecbs 17236 distcds 17286 TarskiGcstrkg 28584 Itvcitv 28590 cgrGccgrg 28667 cgrAccgra 28964

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5224 ax-sep 5243 ax-nul 5253 ax-pow 5319 ax-pr 5387 ax-un 7713 ax-cnex 11123 ax-resscn 11124 ax-1cn 11125 ax-icn 11126 ax-addcl 11127 ax-addrcl 11128 ax-mulcl 11129 ax-mulrcl 11130 ax-mulcom 11131 ax-addass 11132 ax-mulass 11133 ax-distr 11134 ax-i2m1 11135 ax-1ne0 11136 ax-1rid 11137 ax-rnegex 11138 ax-rrecex 11139 ax-cnre 11140 ax-pre-lttri 11141 ax-pre-lttrn 11142 ax-pre-ltadd 11143 ax-pre-mulgt0 11144

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-tp 4584 df-op 4586 df-uni 4863 df-int 4903 df-iun 4948 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5538 df-eprel 5543 df-po 5551 df-so 5552 df-fr 5596 df-we 5598 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-pred 6283 df-ord 6344 df-on 6345 df-lim 6346 df-suc 6347 df-iota 6472 df-fun 6518 df-fn 6519 df-f 6520 df-f1 6521 df-fo 6522 df-f1o 6523 df-fv 6524 df-riota 7348 df-ov 7394 df-oprab 7395 df-mpo 7396 df-om 7842 df-1st 7965 df-2nd 7966 df-frecs 8256 df-wrecs 8287 df-recs 8336 df-rdg 8375 df-1o 8431 df-er 8672 df-map 8804 df-pm 8805 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-card 9891 df-pnf 11212 df-mnf 11213 df-xr 11214 df-ltxr 11215 df-le 11216 df-sub 11410 df-neg 11411 df-nn 12205 df-2 12274 df-3 12275 df-n0 12476 df-z 12563 df-uz 12834 df-fz 13507 df-fzo 13654 df-hash 14338 df-word 14521 df-concat 14578 df-s1 14604 df-s2 14855 df-s3 14856 df-trkgc 28605 df-trkgcb 28607 df-trkg 28610 df-cgrg 28668 df-hlg 28758 df-cgra 28965

This theorem is referenced by: (None)

W3C validator