hypcgr

Description: If the catheti of two right-angled triangles are congruent, so is their hypothenuse. Theorem 10.12 of Schwabhauser p. 91. (Contributed by Thierry Arnoux, 16-Dec-2019)

	Ref	Expression
Hypotheses	hypcgr.p	$⊢ P = {Base}_{G}$
	hypcgr.m	$⊢ \underset{˙}{-} = dist (G)$
	hypcgr.i	$⊢ I = Itv (G)$
	hypcgr.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	hypcgr.h	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
	hypcgr.a	$⊢ φ \to A \in P$
	hypcgr.b	$⊢ φ \to B \in P$
	hypcgr.c	$⊢ φ \to C \in P$
	hypcgr.d	$⊢ φ \to D \in P$
	hypcgr.e	$⊢ φ \to E \in P$
	hypcgr.f	$⊢ φ \to F \in P$
	hypcgr.1	$⊢ φ \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
	hypcgr.2	$⊢ φ \to ⟨“ D E F ”⟩ \in ∟_{𝒢} (G)$
	hypcgr.3	$⊢ φ \to A \underset{˙}{-} B = D \underset{˙}{-} E$
	hypcgr.4	$⊢ φ \to B \underset{˙}{-} C = E \underset{˙}{-} F$
Assertion	hypcgr	$⊢ φ \to A \underset{˙}{-} C = D \underset{˙}{-} F$

Proof

Step	Hyp	Ref	Expression
1		hypcgr.p	$⊢ P = {Base}_{G}$
2		hypcgr.m	$⊢ \underset{˙}{-} = dist (G)$
3		hypcgr.i	$⊢ I = Itv (G)$
4		hypcgr.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		hypcgr.h	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
6		hypcgr.a	$⊢ φ \to A \in P$
7		hypcgr.b	$⊢ φ \to B \in P$
8		hypcgr.c	$⊢ φ \to C \in P$
9		hypcgr.d	$⊢ φ \to D \in P$
10		hypcgr.e	$⊢ φ \to E \in P$
11		hypcgr.f	$⊢ φ \to F \in P$
12		hypcgr.1	$⊢ φ \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
13		hypcgr.2	$⊢ φ \to ⟨“ D E F ”⟩ \in ∟_{𝒢} (G)$
14		hypcgr.3	$⊢ φ \to A \underset{˙}{-} B = D \underset{˙}{-} E$
15		hypcgr.4	$⊢ φ \to B \underset{˙}{-} C = E \underset{˙}{-} F$
16		eqid	$⊢ {Line}_{𝒢} (G) = {Line}_{𝒢} (G)$
17		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
18	1 2 3 4 5 7 10	midcl	$⊢ φ \to B {mid}_{𝒢} (G) E \in P$
19		eqid	$⊢ {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) E) = {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) E)$
20	1 2 3 16 17 4 18 19 9	mircl	$⊢ φ \to {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) E) (D) \in P$
21	1 2 3 16 17 4 18 19 10	mircl	$⊢ φ \to {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) E) (E) \in P$
22	1 2 3 16 17 4 18 19 11	mircl	$⊢ φ \to {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) E) (F) \in P$
23	1 2 3 16 17 4 9 10 11 13 19 18	mirrag	$⊢ φ \to ⟨“ {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) E) (D) {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) E) (E) {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) E) (F) ”⟩ \in ∟_{𝒢} (G)$
24	1 2 3 16 17 4 18 19 9 10	miriso	$⊢ φ \to {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) E) (D) \underset{˙}{-} {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) E) (E) = D \underset{˙}{-} E$
25	14 24	eqtr4d	$⊢ φ \to A \underset{˙}{-} B = {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) E) (D) \underset{˙}{-} {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) E) (E)$
26	1 2 3 16 17 4 18 19 10 11	miriso	$⊢ φ \to {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) E) (E) \underset{˙}{-} {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) E) (F) = E \underset{˙}{-} F$
27	15 26	eqtr4d	$⊢ φ \to B \underset{˙}{-} C = {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) E) (E) \underset{˙}{-} {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) E) (F)$
28	1 2 3 4 5 10 7	midcom	$⊢ φ \to E {mid}_{𝒢} (G) B = B {mid}_{𝒢} (G) E$
29	1 2 3 4 5 10 7 17 18	ismidb	$⊢ φ \to (B = {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) E) (E) \leftrightarrow E {mid}_{𝒢} (G) B = B {mid}_{𝒢} (G) E)$
30	28 29	mpbird	$⊢ φ \to B = {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) E) (E)$
31		eqid	$⊢ {lInv}_{𝒢} (G) ((C {mid}_{𝒢} (G) {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) E) (F)) {Line}_{𝒢} (G) B) = {lInv}_{𝒢} (G) ((C {mid}_{𝒢} (G) {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) E) (F)) {Line}_{𝒢} (G) B)$
32	1 2 3 4 5 6 7 8 20 21 22 12 23 25 27 30 31	hypcgrlem2	$⊢ φ \to A \underset{˙}{-} C = {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) E) (D) \underset{˙}{-} {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) E) (F)$
33	1 2 3 16 17 4 18 19 9 11	miriso	$⊢ φ \to {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) E) (D) \underset{˙}{-} {pInv}_{𝒢} (G) (B {mid}_{𝒢} (G) E) (F) = D \underset{˙}{-} F$
34	32 33	eqtrd	$⊢ φ \to A \underset{˙}{-} C = D \underset{˙}{-} F$

Metamath Proof Explorer

Theorem hypcgr

Proof