Metamath Proof Explorer

Theorem ragcgr

Description: Right angle and colinearity. Theorem 8.10 of Schwabhauser p. 58. (Contributed by Thierry Arnoux, 4-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 )
ragcgr.c 
|- .~ = ( cgrG ` G )
ragcgr.d 
|- ( ph -> D e. P )
ragcgr.e 
|- ( ph -> E e. P )
ragcgr.f 
|- ( ph -> F e. P )
ragcgr.1 
|- ( ph -> <" A B C "> e. ( raG ` G ) )
ragcgr.2 
|- ( ph -> <" A B C "> .~ <" D E F "> )
Assertion ragcgr 
|- ( ph -> <" D E F "> e. ( raG ` G ) )

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 ragcgr.c 
 |-  .~ = ( cgrG ` G )
11 ragcgr.d 
 |-  ( ph -> D e. P )
12 ragcgr.e 
 |-  ( ph -> E e. P )
13 ragcgr.f 
 |-  ( ph -> F e. P )
14 ragcgr.1 
 |-  ( ph -> <" A B C "> e. ( raG ` G ) )
15 ragcgr.2 
 |-  ( ph -> <" A B C "> .~ <" D E F "> )
16 eqidd 
 |-  ( ( ph /\ B = C ) -> D = D )
17 6 adantr 
 |-  ( ( ph /\ B = C ) -> G e. TarskiG )
18 8 adantr 
 |-  ( ( ph /\ B = C ) -> B e. P )
19 9 adantr 
 |-  ( ( ph /\ B = C ) -> C e. P )
20 12 adantr 
 |-  ( ( ph /\ B = C ) -> E e. P )
21 13 adantr 
 |-  ( ( ph /\ B = C ) -> F e. P )
22 7 adantr 
 |-  ( ( ph /\ B = C ) -> A e. P )
23 11 adantr 
 |-  ( ( ph /\ B = C ) -> D e. P )
24 15 adantr 
 |-  ( ( ph /\ B = C ) -> <" A B C "> .~ <" D E F "> )
25 1 2 3 10 17 22 18 19 23 20 21 24 cgr3simp2 
 |-  ( ( ph /\ B = C ) -> ( B .- C ) = ( E .- F ) )
26 simpr 
 |-  ( ( ph /\ B = C ) -> B = C )
27 1 2 3 17 18 19 20 21 25 26 tgcgreq 
 |-  ( ( ph /\ B = C ) -> E = F )
28 eqidd 
 |-  ( ( ph /\ B = C ) -> F = F )
29 16 27 28 s3eqd 
 |-  ( ( ph /\ B = C ) -> <" D E F "> = <" D F F "> )
30 1 2 3 4 5 17 23 21 20 ragtrivb 
 |-  ( ( ph /\ B = C ) -> <" D F F "> e. ( raG ` G ) )
31 29 30 eqeltrd 
 |-  ( ( ph /\ B = C ) -> <" D E F "> e. ( raG ` G ) )
32 14 adantr 
 |-  ( ( ph /\ B =/= C ) -> <" A B C "> e. ( raG ` G ) )
33 6 adantr 
 |-  ( ( ph /\ B =/= C ) -> G e. TarskiG )
34 7 adantr 
 |-  ( ( ph /\ B =/= C ) -> A e. P )
35 8 adantr 
 |-  ( ( ph /\ B =/= C ) -> B e. P )
36 9 adantr 
 |-  ( ( ph /\ B =/= C ) -> C e. P )
37 1 2 3 4 5 33 34 35 36 israg 
 |-  ( ( ph /\ B =/= C ) -> ( <" A B C "> e. ( raG ` G ) <-> ( A .- C ) = ( A .- ( ( S ` B ) ` C ) ) ) )
38 32 37 mpbid 
 |-  ( ( ph /\ B =/= C ) -> ( A .- C ) = ( A .- ( ( S ` B ) ` C ) ) )
39 13 adantr 
 |-  ( ( ph /\ B =/= C ) -> F e. P )
40 11 adantr 
 |-  ( ( ph /\ B =/= C ) -> D e. P )
41 12 adantr 
 |-  ( ( ph /\ B =/= C ) -> E e. P )
42 15 adantr 
 |-  ( ( ph /\ B =/= C ) -> <" A B C "> .~ <" D E F "> )
43 1 2 3 10 33 34 35 36 40 41 39 42 cgr3simp3 
 |-  ( ( ph /\ B =/= C ) -> ( C .- A ) = ( F .- D ) )
44 1 2 3 33 36 34 39 40 43 tgcgrcomlr 
 |-  ( ( ph /\ B =/= C ) -> ( A .- C ) = ( D .- F ) )
45 eqid 
 |-  ( S ` B ) = ( S ` B )
46 1 2 3 4 5 33 35 45 36 mircl 
 |-  ( ( ph /\ B =/= C ) -> ( ( S ` B ) ` C ) e. P )
47 eqid 
 |-  ( S ` E ) = ( S ` E )
48 1 2 3 4 5 33 41 47 39 mircl 
 |-  ( ( ph /\ B =/= C ) -> ( ( S ` E ) ` F ) e. P )
49 simpr 
 |-  ( ( ph /\ B =/= C ) -> B =/= C )
50 49 necomd 
 |-  ( ( ph /\ B =/= C ) -> C =/= B )
51 1 2 3 4 5 33 35 45 36 mirbtwn 
 |-  ( ( ph /\ B =/= C ) -> B e. ( ( ( S ` B ) ` C ) I C ) )
52 1 2 3 33 46 35 36 51 tgbtwncom 
 |-  ( ( ph /\ B =/= C ) -> B e. ( C I ( ( S ` B ) ` C ) ) )
53 1 2 3 4 5 33 41 47 39 mirbtwn 
 |-  ( ( ph /\ B =/= C ) -> E e. ( ( ( S ` E ) ` F ) I F ) )
54 1 2 3 33 48 41 39 53 tgbtwncom 
 |-  ( ( ph /\ B =/= C ) -> E e. ( F I ( ( S ` E ) ` F ) ) )
55 1 2 3 10 33 34 35 36 40 41 39 42 cgr3simp2 
 |-  ( ( ph /\ B =/= C ) -> ( B .- C ) = ( E .- F ) )
56 1 2 3 33 35 36 41 39 55 tgcgrcomlr 
 |-  ( ( ph /\ B =/= C ) -> ( C .- B ) = ( F .- E ) )
57 1 2 3 4 5 33 35 45 36 mircgr 
 |-  ( ( ph /\ B =/= C ) -> ( B .- ( ( S ` B ) ` C ) ) = ( B .- C ) )
58 1 2 3 4 5 33 41 47 39 mircgr 
 |-  ( ( ph /\ B =/= C ) -> ( E .- ( ( S ` E ) ` F ) ) = ( E .- F ) )
59 55 57 58 3eqtr4d 
 |-  ( ( ph /\ B =/= C ) -> ( B .- ( ( S ` B ) ` C ) ) = ( E .- ( ( S ` E ) ` F ) ) )
60 1 2 3 10 33 34 35 36 40 41 39 42 cgr3simp1 
 |-  ( ( ph /\ B =/= C ) -> ( A .- B ) = ( D .- E ) )
61 1 2 3 33 34 35 40 41 60 tgcgrcomlr 
 |-  ( ( ph /\ B =/= C ) -> ( B .- A ) = ( E .- D ) )
62 1 2 3 33 36 35 46 39 41 48 34 40 50 52 54 56 59 43 61 axtg5seg 
 |-  ( ( ph /\ B =/= C ) -> ( ( ( S ` B ) ` C ) .- A ) = ( ( ( S ` E ) ` F ) .- D ) )
63 1 2 3 33 46 34 48 40 62 tgcgrcomlr 
 |-  ( ( ph /\ B =/= C ) -> ( A .- ( ( S ` B ) ` C ) ) = ( D .- ( ( S ` E ) ` F ) ) )
64 38 44 63 3eqtr3d 
 |-  ( ( ph /\ B =/= C ) -> ( D .- F ) = ( D .- ( ( S ` E ) ` F ) ) )
65 1 2 3 4 5 33 40 41 39 israg 
 |-  ( ( ph /\ B =/= C ) -> ( <" D E F "> e. ( raG ` G ) <-> ( D .- F ) = ( D .- ( ( S ` E ) ` F ) ) ) )
66 64 65 mpbird 
 |-  ( ( ph /\ B =/= C ) -> <" D E F "> e. ( raG ` G ) )
67 31 66 pm2.61dane 
 |-  ( ph -> <" D E F "> e. ( raG ` G ) )