Metamath Proof Explorer


Theorem ragflat2

Description: Deduce equality from two right angles. Theorem 8.6 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 )
ragflat2.d
|- ( ph -> D e. P )
ragflat2.1
|- ( ph -> <" A B C "> e. ( raG ` G ) )
ragflat2.2
|- ( ph -> <" D B C "> e. ( raG ` G ) )
ragflat2.3
|- ( ph -> C e. ( A I D ) )
Assertion ragflat2
|- ( 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 ragflat2.d
 |-  ( ph -> D e. P )
11 ragflat2.1
 |-  ( ph -> <" A B C "> e. ( raG ` G ) )
12 ragflat2.2
 |-  ( ph -> <" D B C "> e. ( raG ` G ) )
13 ragflat2.3
 |-  ( ph -> C e. ( A I 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 1 2 3 4 5 6 7 8 9 israg
 |-  ( ph -> ( <" A B C "> e. ( raG ` G ) <-> ( A .- C ) = ( A .- ( ( S ` B ) ` C ) ) ) )
18 11 17 mpbid
 |-  ( ph -> ( A .- C ) = ( A .- ( ( S ` B ) ` C ) ) )
19 1 2 3 4 5 6 10 8 9 israg
 |-  ( ph -> ( <" D B C "> e. ( raG ` G ) <-> ( D .- C ) = ( D .- ( ( S ` B ) ` C ) ) ) )
20 12 19 mpbid
 |-  ( ph -> ( D .- C ) = ( D .- ( ( S ` B ) ` C ) ) )
21 1 4 3 6 7 10 9 14 16 7 2 13 18 20 tgidinside
 |-  ( ph -> C = ( ( S ` B ) ` C ) )
22 21 eqcomd
 |-  ( ph -> ( ( S ` B ) ` C ) = C )
23 1 2 3 4 5 6 8 15 9 mirinv
 |-  ( ph -> ( ( ( S ` B ) ` C ) = C <-> B = C ) )
24 22 23 mpbid
 |-  ( ph -> B = C )