Metamath Proof Explorer

Theorem ragflat

Description: Deduce equality from two right angles. Theorem 8.7 of Schwabhauser p. 58. (Contributed by Thierry Arnoux, 3-Sep-2019)

Ref Expression
Hypotheses israg.p 
|- P = ( Base ` G )
israg.d 
|- .- = ( dist ` G )
israg.i 
|- I = ( Itv ` G )
israg.l 
|- L = ( LineG ` G )
israg.s 
|- S = ( pInvG ` G )
israg.g 
|- ( ph -> G e. TarskiG )
israg.a 
|- ( ph -> A e. P )
israg.b 
|- ( ph -> B e. P )
israg.c 
|- ( ph -> C e. P )
ragflat.1 
|- ( ph -> <" A B C "> e. ( raG ` G ) )
ragflat.2 
|- ( ph -> <" A C B "> e. ( raG ` G ) )
Assertion ragflat 
|- ( ph -> B = C )

Proof

Step Hyp Ref Expression
1 israg.p 
 |-  P = ( Base ` G )
2 israg.d 
 |-  .- = ( dist ` G )
3 israg.i 
 |-  I = ( Itv ` G )
4 israg.l 
 |-  L = ( LineG ` G )
5 israg.s 
 |-  S = ( pInvG ` G )
6 israg.g 
 |-  ( ph -> G e. TarskiG )
7 israg.a 
 |-  ( ph -> A e. P )
8 israg.b 
 |-  ( ph -> B e. P )
9 israg.c 
 |-  ( ph -> C e. P )
10 ragflat.1 
 |-  ( ph -> <" A B C "> e. ( raG ` G ) )
11 ragflat.2 
 |-  ( ph -> <" A C B "> e. ( raG ` G ) )
12 simpr 
 |-  ( ( ph /\ B = C ) -> B = C )
13 6 adantr 
 |-  ( ( ph /\ B =/= C ) -> G e. TarskiG )
14 7 adantr 
 |-  ( ( ph /\ B =/= C ) -> A e. P )
15 8 adantr 
 |-  ( ( ph /\ B =/= C ) -> B e. P )
16 9 adantr 
 |-  ( ( ph /\ B =/= C ) -> C e. P )
17 eqid 
 |-  ( S ` C ) = ( S ` C )
18 1 2 3 4 5 13 16 17 14 mircl 
 |-  ( ( ph /\ B =/= C ) -> ( ( S ` C ) ` A ) e. P )
19 10 adantr 
 |-  ( ( ph /\ B =/= C ) -> <" A B C "> e. ( raG ` G ) )
20 1 2 3 4 5 13 16 17 14 mircgr 
 |-  ( ( ph /\ B =/= C ) -> ( C .- ( ( S ` C ) ` A ) ) = ( C .- A ) )
21 1 2 3 13 16 18 16 14 20 tgcgrcomlr 
 |-  ( ( ph /\ B =/= C ) -> ( ( ( S ` C ) ` A ) .- C ) = ( A .- C ) )
22 1 2 3 4 5 13 14 15 16 israg 
 |-  ( ( ph /\ B =/= C ) -> ( <" A B C "> e. ( raG ` G ) <-> ( A .- C ) = ( A .- ( ( S ` B ) ` C ) ) ) )
23 19 22 mpbid 
 |-  ( ( ph /\ B =/= C ) -> ( A .- C ) = ( A .- ( ( S ` B ) ` C ) ) )
24 eqid 
 |-  ( S ` B ) = ( S ` B )
25 1 2 3 4 5 13 15 24 16 mircl 
 |-  ( ( ph /\ B =/= C ) -> ( ( S ` B ) ` C ) e. P )
26 11 adantr 
 |-  ( ( ph /\ B =/= C ) -> <" A C B "> e. ( raG ` G ) )
27 1 2 3 4 5 13 14 16 15 26 ragcom 
 |-  ( ( ph /\ B =/= C ) -> <" B C A "> e. ( raG ` G ) )
28 simpr 
 |-  ( ( ph /\ B =/= C ) -> B =/= C )
29 1 2 3 4 5 13 15 24 16 mirbtwn 
 |-  ( ( ph /\ B =/= C ) -> B e. ( ( ( S ` B ) ` C ) I C ) )
30 1 2 3 13 25 15 16 29 tgbtwncom 
 |-  ( ( ph /\ B =/= C ) -> B e. ( C I ( ( S ` B ) ` C ) ) )
31 1 4 3 13 16 25 15 30 btwncolg1 
 |-  ( ( ph /\ B =/= C ) -> ( B e. ( C L ( ( S ` B ) ` C ) ) \/ C = ( ( S ` B ) ` C ) ) )
32 1 2 3 4 5 13 15 16 14 25 27 28 31 ragcol 
 |-  ( ( ph /\ B =/= C ) -> <" ( ( S ` B ) ` C ) C A "> e. ( raG ` G ) )
33 1 2 3 4 5 13 25 16 14 israg 
 |-  ( ( ph /\ B =/= C ) -> ( <" ( ( S ` B ) ` C ) C A "> e. ( raG ` G ) <-> ( ( ( S ` B ) ` C ) .- A ) = ( ( ( S ` B ) ` C ) .- ( ( S ` C ) ` A ) ) ) )
34 32 33 mpbid 
 |-  ( ( ph /\ B =/= C ) -> ( ( ( S ` B ) ` C ) .- A ) = ( ( ( S ` B ) ` C ) .- ( ( S ` C ) ` A ) ) )
35 1 2 3 13 25 14 25 18 34 tgcgrcomlr 
 |-  ( ( ph /\ B =/= C ) -> ( A .- ( ( S ` B ) ` C ) ) = ( ( ( S ` C ) ` A ) .- ( ( S ` B ) ` C ) ) )
36 21 23 35 3eqtrd 
 |-  ( ( ph /\ B =/= C ) -> ( ( ( S ` C ) ` A ) .- C ) = ( ( ( S ` C ) ` A ) .- ( ( S ` B ) ` C ) ) )
37 1 2 3 4 5 13 18 15 16 israg 
 |-  ( ( ph /\ B =/= C ) -> ( <" ( ( S ` C ) ` A ) B C "> e. ( raG ` G ) <-> ( ( ( S ` C ) ` A ) .- C ) = ( ( ( S ` C ) ` A ) .- ( ( S ` B ) ` C ) ) ) )
38 36 37 mpbird 
 |-  ( ( ph /\ B =/= C ) -> <" ( ( S ` C ) ` A ) B C "> e. ( raG ` G ) )
39 1 2 3 4 5 13 16 17 14 mirbtwn 
 |-  ( ( ph /\ B =/= C ) -> C e. ( ( ( S ` C ) ` A ) I A ) )
40 1 2 3 13 18 16 14 39 tgbtwncom 
 |-  ( ( ph /\ B =/= C ) -> C e. ( A I ( ( S ` C ) ` A ) ) )
41 1 2 3 4 5 13 14 15 16 18 19 38 40 ragflat2 
 |-  ( ( ph /\ B =/= C ) -> B = C )
42 12 41 pm2.61dane 
 |-  ( ph -> B = C )