Metamath Proof Explorer


Theorem ragcol

Description: The right angle property is independent of the choice of point on one side. Theorem 8.3 of Schwabhauser p. 58. (Contributed by Thierry Arnoux, 25-Aug-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 )
ragcol.d
|- ( ph -> D e. P )
ragcol.1
|- ( ph -> <" A B C "> e. ( raG ` G ) )
ragcol.2
|- ( ph -> A =/= B )
ragcol.3
|- ( ph -> ( A e. ( B L D ) \/ B = D ) )
Assertion ragcol
|- ( ph -> <" D B C "> 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 ragcol.d
 |-  ( ph -> D e. P )
11 ragcol.1
 |-  ( ph -> <" A B C "> e. ( raG ` G ) )
12 ragcol.2
 |-  ( ph -> A =/= B )
13 ragcol.3
 |-  ( ph -> ( A e. ( B L D ) \/ B = D ) )
14 eqid
 |-  ( cgrG ` G ) = ( cgrG ` G )
15 eqid
 |-  ( S ` B ) = ( S ` B )
16 1 2 3 4 5 6 8 15 9 mircl
 |-  ( ph -> ( ( S ` B ) ` C ) e. P )
17 12 necomd
 |-  ( ph -> B =/= A )
18 1 2 3 4 5 6 8 15 9 mircgr
 |-  ( ph -> ( B .- ( ( S ` B ) ` C ) ) = ( B .- C ) )
19 18 eqcomd
 |-  ( ph -> ( B .- C ) = ( B .- ( ( S ` B ) ` C ) ) )
20 1 2 3 4 5 6 7 8 9 israg
 |-  ( ph -> ( <" A B C "> e. ( raG ` G ) <-> ( A .- C ) = ( A .- ( ( S ` B ) ` C ) ) ) )
21 11 20 mpbid
 |-  ( ph -> ( A .- C ) = ( A .- ( ( S ` B ) ` C ) ) )
22 1 4 3 6 8 7 10 14 9 16 2 17 13 19 21 lncgr
 |-  ( ph -> ( D .- C ) = ( D .- ( ( S ` B ) ` C ) ) )
23 1 2 3 4 5 6 10 8 9 israg
 |-  ( ph -> ( <" D B C "> e. ( raG ` G ) <-> ( D .- C ) = ( D .- ( ( S ` B ) ` C ) ) ) )
24 22 23 mpbird
 |-  ( ph -> <" D B C "> e. ( raG ` G ) )