Metamath Proof Explorer

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 ⊢ 𝑃 = ( Base ‘ 𝐺 )
hypcgr.m ⊢ − = ( dist ‘ 𝐺 )
hypcgr.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
hypcgr.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
hypcgr.h ⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
hypcgr.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
hypcgr.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
hypcgr.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
hypcgr.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
hypcgr.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
hypcgr.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
hypcgr.1 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
hypcgr.2 ⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
hypcgr.3 ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
hypcgr.4 ⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) )
Assertion hypcgr ( 𝜑 → ( 𝐴 − 𝐶 ) = ( 𝐷 − 𝐹 ) )

Proof

Step Hyp Ref Expression
1 hypcgr.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 hypcgr.m ⊢ − = ( dist ‘ 𝐺 )
3 hypcgr.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 hypcgr.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 hypcgr.h ⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
6 hypcgr.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
7 hypcgr.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
8 hypcgr.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
9 hypcgr.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
10 hypcgr.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
11 hypcgr.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
12 hypcgr.1 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
13 hypcgr.2 ⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
14 hypcgr.3 ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
15 hypcgr.4 ⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) )
16 eqid ⊢ ( LineG ‘ 𝐺 ) = ( LineG ‘ 𝐺 )
17 eqid ⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
18 1 2 3 4 5 7 10 midcl ⊢ ( 𝜑 → ( 𝐵 ( midG ‘ 𝐺 ) 𝐸 ) ∈ 𝑃 )
19 eqid ⊢ ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) 𝐸 ) ) = ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) 𝐸 ) )
20 1 2 3 16 17 4 18 19 9 mircl ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) 𝐸 ) ) ‘ 𝐷 ) ∈ 𝑃 )
21 1 2 3 16 17 4 18 19 10 mircl ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) 𝐸 ) ) ‘ 𝐸 ) ∈ 𝑃 )
22 1 2 3 16 17 4 18 19 11 mircl ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) 𝐸 ) ) ‘ 𝐹 ) ∈ 𝑃 )
23 1 2 3 16 17 4 9 10 11 13 19 18 mirrag ⊢ ( 𝜑 → ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) 𝐸 ) ) ‘ 𝐷 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) 𝐸 ) ) ‘ 𝐸 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) 𝐸 ) ) ‘ 𝐹 ) ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
24 1 2 3 16 17 4 18 19 9 10 miriso ⊢ ( 𝜑 → ( ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) 𝐸 ) ) ‘ 𝐷 ) − ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) 𝐸 ) ) ‘ 𝐸 ) ) = ( 𝐷 − 𝐸 ) )
25 14 24 eqtr4d ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) 𝐸 ) ) ‘ 𝐷 ) − ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) 𝐸 ) ) ‘ 𝐸 ) ) )
26 1 2 3 16 17 4 18 19 10 11 miriso ⊢ ( 𝜑 → ( ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) 𝐸 ) ) ‘ 𝐸 ) − ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) 𝐸 ) ) ‘ 𝐹 ) ) = ( 𝐸 − 𝐹 ) )
27 15 26 eqtr4d ⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) 𝐸 ) ) ‘ 𝐸 ) − ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) 𝐸 ) ) ‘ 𝐹 ) ) )
28 1 2 3 4 5 10 7 midcom ⊢ ( 𝜑 → ( 𝐸 ( midG ‘ 𝐺 ) 𝐵 ) = ( 𝐵 ( midG ‘ 𝐺 ) 𝐸 ) )
29 1 2 3 4 5 10 7 17 18 ismidb ⊢ ( 𝜑 → ( 𝐵 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) 𝐸 ) ) ‘ 𝐸 ) ↔ ( 𝐸 ( midG ‘ 𝐺 ) 𝐵 ) = ( 𝐵 ( midG ‘ 𝐺 ) 𝐸 ) ) )
30 28 29 mpbird ⊢ ( 𝜑 → 𝐵 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) 𝐸 ) ) ‘ 𝐸 ) )
31 eqid ⊢ ( ( lInvG ‘ 𝐺 ) ‘ ( ( 𝐶 ( midG ‘ 𝐺 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) 𝐸 ) ) ‘ 𝐹 ) ) ( LineG ‘ 𝐺 ) 𝐵 ) ) = ( ( lInvG ‘ 𝐺 ) ‘ ( ( 𝐶 ( midG ‘ 𝐺 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) 𝐸 ) ) ‘ 𝐹 ) ) ( LineG ‘ 𝐺 ) 𝐵 ) )
32 1 2 3 4 5 6 7 8 20 21 22 12 23 25 27 30 31 hypcgrlem2 ⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) = ( ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) 𝐸 ) ) ‘ 𝐷 ) − ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) 𝐸 ) ) ‘ 𝐹 ) ) )
33 1 2 3 16 17 4 18 19 9 11 miriso ⊢ ( 𝜑 → ( ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) 𝐸 ) ) ‘ 𝐷 ) − ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐵 ( midG ‘ 𝐺 ) 𝐸 ) ) ‘ 𝐹 ) ) = ( 𝐷 − 𝐹 ) )
34 32 33 eqtrd ⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) = ( 𝐷 − 𝐹 ) )