Theorem 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={\mathrm{Base}}_G$$
	hypcgr.m	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	hypcgr.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	hypcgr.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	hypcgr.h	$$⊢\phi \to G{\mathrm{Dim}}_{𝒢}\ge 2$$
	hypcgr.a	$$⊢\phi \to A\in P$$
	hypcgr.b	$$⊢\phi \to B\in P$$
	hypcgr.c	$$⊢\phi \to C\in P$$
	hypcgr.d	$$⊢\phi \to D\in P$$
	hypcgr.e	$$⊢\phi \to E\in P$$
	hypcgr.f	$$⊢\phi \to F\in P$$
	hypcgr.1	$$⊢\phi \to ⟨“ABC”⟩\in {∟}_{𝒢}\left(G\right)$$
	hypcgr.2	$$⊢\phi \to ⟨“DEF”⟩\in {∟}_{𝒢}\left(G\right)$$
	hypcgr.3	$$⊢\phi \to A\underset{\dot{}}{-}B=D\underset{\dot{}}{-}E$$
	hypcgr.4	$$⊢\phi \to B\underset{\dot{}}{-}C=E\underset{\dot{}}{-}F$$
Assertion	hypcgr	$$⊢\phi \to A\underset{\dot{}}{-}C=D\underset{\dot{}}{-}F$$

Proof

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