Metamath Proof Explorer


Theorem ragcom

Description: Commutative rule for right angles. Theorem 8.2 of Schwabhauser p. 57. (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 )
ragcom.1
|- ( ph -> <" A B C "> e. ( raG ` G ) )
Assertion ragcom
|- ( ph -> <" C B A "> 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 ragcom.1
 |-  ( ph -> <" A B C "> e. ( raG ` G ) )
11 eqid
 |-  ( S ` B ) = ( S ` B )
12 1 2 3 4 5 6 8 11 9 mircl
 |-  ( ph -> ( ( S ` B ) ` C ) e. P )
13 1 2 3 4 5 6 7 8 9 israg
 |-  ( ph -> ( <" A B C "> e. ( raG ` G ) <-> ( A .- C ) = ( A .- ( ( S ` B ) ` C ) ) ) )
14 10 13 mpbid
 |-  ( ph -> ( A .- C ) = ( A .- ( ( S ` B ) ` C ) ) )
15 1 2 3 6 7 9 7 12 14 tgcgrcomlr
 |-  ( ph -> ( C .- A ) = ( ( ( S ` B ) ` C ) .- A ) )
16 1 2 3 4 5 6 8 11 12 7 miriso
 |-  ( ph -> ( ( ( S ` B ) ` ( ( S ` B ) ` C ) ) .- ( ( S ` B ) ` A ) ) = ( ( ( S ` B ) ` C ) .- A ) )
17 1 2 3 4 5 6 8 11 9 mirmir
 |-  ( ph -> ( ( S ` B ) ` ( ( S ` B ) ` C ) ) = C )
18 17 oveq1d
 |-  ( ph -> ( ( ( S ` B ) ` ( ( S ` B ) ` C ) ) .- ( ( S ` B ) ` A ) ) = ( C .- ( ( S ` B ) ` A ) ) )
19 15 16 18 3eqtr2d
 |-  ( ph -> ( C .- A ) = ( C .- ( ( S ` B ) ` A ) ) )
20 1 2 3 4 5 6 9 8 7 israg
 |-  ( ph -> ( <" C B A "> e. ( raG ` G ) <-> ( C .- A ) = ( C .- ( ( S ` B ) ` A ) ) ) )
21 19 20 mpbird
 |-  ( ph -> <" C B A "> e. ( raG ` G ) )