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 
|- P = ( Base ` G )
hypcgr.m 
|- .- = ( dist ` G )
hypcgr.i 
|- I = ( Itv ` G )
hypcgr.g 
|- ( ph -> G e. TarskiG )
hypcgr.h 
|- ( ph -> G TarskiGDim>= 2 )
hypcgr.a 
|- ( ph -> A e. P )
hypcgr.b 
|- ( ph -> B e. P )
hypcgr.c 
|- ( ph -> C e. P )
hypcgr.d 
|- ( ph -> D e. P )
hypcgr.e 
|- ( ph -> E e. P )
hypcgr.f 
|- ( ph -> F e. P )
hypcgr.1 
|- ( ph -> <" A B C "> e. ( raG ` G ) )
hypcgr.2 
|- ( ph -> <" D E F "> e. ( raG ` G ) )
hypcgr.3 
|- ( ph -> ( A .- B ) = ( D .- E ) )
hypcgr.4 
|- ( ph -> ( B .- C ) = ( E .- F ) )
Assertion hypcgr 
|- ( ph -> ( A .- C ) = ( D .- F ) )

Proof

Step Hyp Ref Expression
1 hypcgr.p 
 |-  P = ( Base ` G )
2 hypcgr.m 
 |-  .- = ( dist ` G )
3 hypcgr.i 
 |-  I = ( Itv ` G )
4 hypcgr.g 
 |-  ( ph -> G e. TarskiG )
5 hypcgr.h 
 |-  ( ph -> G TarskiGDim>= 2 )
6 hypcgr.a 
 |-  ( ph -> A e. P )
7 hypcgr.b 
 |-  ( ph -> B e. P )
8 hypcgr.c 
 |-  ( ph -> C e. P )
9 hypcgr.d 
 |-  ( ph -> D e. P )
10 hypcgr.e 
 |-  ( ph -> E e. P )
11 hypcgr.f 
 |-  ( ph -> F e. P )
12 hypcgr.1 
 |-  ( ph -> <" A B C "> e. ( raG ` G ) )
13 hypcgr.2 
 |-  ( ph -> <" D E F "> e. ( raG ` G ) )
14 hypcgr.3 
 |-  ( ph -> ( A .- B ) = ( D .- E ) )
15 hypcgr.4 
 |-  ( ph -> ( B .- C ) = ( E .- F ) )
16 eqid 
 |-  ( LineG ` G ) = ( LineG ` G )
17 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
18 1 2 3 4 5 7 10 midcl 
 |-  ( ph -> ( B ( midG ` G ) E ) e. P )
19 eqid 
 |-  ( ( pInvG ` G ) ` ( B ( midG ` G ) E ) ) = ( ( pInvG ` G ) ` ( B ( midG ` G ) E ) )
20 1 2 3 16 17 4 18 19 9 mircl 
 |-  ( ph -> ( ( ( pInvG ` G ) ` ( B ( midG ` G ) E ) ) ` D ) e. P )
21 1 2 3 16 17 4 18 19 10 mircl 
 |-  ( ph -> ( ( ( pInvG ` G ) ` ( B ( midG ` G ) E ) ) ` E ) e. P )
22 1 2 3 16 17 4 18 19 11 mircl 
 |-  ( ph -> ( ( ( pInvG ` G ) ` ( B ( midG ` G ) E ) ) ` F ) e. P )
23 1 2 3 16 17 4 9 10 11 13 19 18 mirrag 
 |-  ( ph -> <" ( ( ( pInvG ` G ) ` ( B ( midG ` G ) E ) ) ` D ) ( ( ( pInvG ` G ) ` ( B ( midG ` G ) E ) ) ` E ) ( ( ( pInvG ` G ) ` ( B ( midG ` G ) E ) ) ` F ) "> e. ( raG ` G ) )
24 1 2 3 16 17 4 18 19 9 10 miriso 
 |-  ( ph -> ( ( ( ( pInvG ` G ) ` ( B ( midG ` G ) E ) ) ` D ) .- ( ( ( pInvG ` G ) ` ( B ( midG ` G ) E ) ) ` E ) ) = ( D .- E ) )
25 14 24 eqtr4d 
 |-  ( ph -> ( A .- B ) = ( ( ( ( pInvG ` G ) ` ( B ( midG ` G ) E ) ) ` D ) .- ( ( ( pInvG ` G ) ` ( B ( midG ` G ) E ) ) ` E ) ) )
26 1 2 3 16 17 4 18 19 10 11 miriso 
 |-  ( ph -> ( ( ( ( pInvG ` G ) ` ( B ( midG ` G ) E ) ) ` E ) .- ( ( ( pInvG ` G ) ` ( B ( midG ` G ) E ) ) ` F ) ) = ( E .- F ) )
27 15 26 eqtr4d 
 |-  ( ph -> ( B .- C ) = ( ( ( ( pInvG ` G ) ` ( B ( midG ` G ) E ) ) ` E ) .- ( ( ( pInvG ` G ) ` ( B ( midG ` G ) E ) ) ` F ) ) )
28 1 2 3 4 5 10 7 midcom 
 |-  ( ph -> ( E ( midG ` G ) B ) = ( B ( midG ` G ) E ) )
29 1 2 3 4 5 10 7 17 18 ismidb 
 |-  ( ph -> ( B = ( ( ( pInvG ` G ) ` ( B ( midG ` G ) E ) ) ` E ) <-> ( E ( midG ` G ) B ) = ( B ( midG ` G ) E ) ) )
30 28 29 mpbird 
 |-  ( ph -> B = ( ( ( pInvG ` G ) ` ( B ( midG ` G ) E ) ) ` E ) )
31 eqid 
 |-  ( ( lInvG ` G ) ` ( ( C ( midG ` G ) ( ( ( pInvG ` G ) ` ( B ( midG ` G ) E ) ) ` F ) ) ( LineG ` G ) B ) ) = ( ( lInvG ` G ) ` ( ( C ( midG ` G ) ( ( ( pInvG ` G ) ` ( B ( midG ` G ) E ) ) ` F ) ) ( LineG ` G ) B ) )
32 1 2 3 4 5 6 7 8 20 21 22 12 23 25 27 30 31 hypcgrlem2 
 |-  ( ph -> ( A .- C ) = ( ( ( ( pInvG ` G ) ` ( B ( midG ` G ) E ) ) ` D ) .- ( ( ( pInvG ` G ) ` ( B ( midG ` G ) E ) ) ` F ) ) )
33 1 2 3 16 17 4 18 19 9 11 miriso 
 |-  ( ph -> ( ( ( ( pInvG ` G ) ` ( B ( midG ` G ) E ) ) ` D ) .- ( ( ( pInvG ` G ) ` ( B ( midG ` G ) E ) ) ` F ) ) = ( D .- F ) )
34 32 33 eqtrd 
 |-  ( ph -> ( A .- C ) = ( D .- F ) )