Metamath Proof Explorer

Theorem israg

Description: Property for 3 points A, B, C to form a right angle. Definition 8.1 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 )
Assertion israg 
|- ( ph -> ( <" A B C "> e. ( raG ` G ) <-> ( A .- C ) = ( A .- ( ( S ` 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 7 8 9 s3cld 
 |-  ( ph -> <" A B C "> e. Word P )
11 fveqeq2 
 |-  ( w = <" A B C "> -> ( ( # ` w ) = 3 <-> ( # ` <" A B C "> ) = 3 ) )
12 fveq1 
 |-  ( w = <" A B C "> -> ( w ` 0 ) = ( <" A B C "> ` 0 ) )
13 fveq1 
 |-  ( w = <" A B C "> -> ( w ` 2 ) = ( <" A B C "> ` 2 ) )
14 12 13 oveq12d 
 |-  ( w = <" A B C "> -> ( ( w ` 0 ) .- ( w ` 2 ) ) = ( ( <" A B C "> ` 0 ) .- ( <" A B C "> ` 2 ) ) )
15 fveq1 
 |-  ( w = <" A B C "> -> ( w ` 1 ) = ( <" A B C "> ` 1 ) )
16 15 fveq2d 
 |-  ( w = <" A B C "> -> ( S ` ( w ` 1 ) ) = ( S ` ( <" A B C "> ` 1 ) ) )
17 16 13 fveq12d 
 |-  ( w = <" A B C "> -> ( ( S ` ( w ` 1 ) ) ` ( w ` 2 ) ) = ( ( S ` ( <" A B C "> ` 1 ) ) ` ( <" A B C "> ` 2 ) ) )
18 12 17 oveq12d 
 |-  ( w = <" A B C "> -> ( ( w ` 0 ) .- ( ( S ` ( w ` 1 ) ) ` ( w ` 2 ) ) ) = ( ( <" A B C "> ` 0 ) .- ( ( S ` ( <" A B C "> ` 1 ) ) ` ( <" A B C "> ` 2 ) ) ) )
19 14 18 eqeq12d 
 |-  ( w = <" A B C "> -> ( ( ( w ` 0 ) .- ( w ` 2 ) ) = ( ( w ` 0 ) .- ( ( S ` ( w ` 1 ) ) ` ( w ` 2 ) ) ) <-> ( ( <" A B C "> ` 0 ) .- ( <" A B C "> ` 2 ) ) = ( ( <" A B C "> ` 0 ) .- ( ( S ` ( <" A B C "> ` 1 ) ) ` ( <" A B C "> ` 2 ) ) ) ) )
20 11 19 anbi12d 
 |-  ( w = <" A B C "> -> ( ( ( # ` w ) = 3 /\ ( ( w ` 0 ) .- ( w ` 2 ) ) = ( ( w ` 0 ) .- ( ( S ` ( w ` 1 ) ) ` ( w ` 2 ) ) ) ) <-> ( ( # ` <" A B C "> ) = 3 /\ ( ( <" A B C "> ` 0 ) .- ( <" A B C "> ` 2 ) ) = ( ( <" A B C "> ` 0 ) .- ( ( S ` ( <" A B C "> ` 1 ) ) ` ( <" A B C "> ` 2 ) ) ) ) ) )
21 20 elrab3 
 |-  ( <" A B C "> e. Word P -> ( <" A B C "> e. { w e. Word P | ( ( # ` w ) = 3 /\ ( ( w ` 0 ) .- ( w ` 2 ) ) = ( ( w ` 0 ) .- ( ( S ` ( w ` 1 ) ) ` ( w ` 2 ) ) ) ) } <-> ( ( # ` <" A B C "> ) = 3 /\ ( ( <" A B C "> ` 0 ) .- ( <" A B C "> ` 2 ) ) = ( ( <" A B C "> ` 0 ) .- ( ( S ` ( <" A B C "> ` 1 ) ) ` ( <" A B C "> ` 2 ) ) ) ) ) )
22 10 21 syl 
 |-  ( ph -> ( <" A B C "> e. { w e. Word P | ( ( # ` w ) = 3 /\ ( ( w ` 0 ) .- ( w ` 2 ) ) = ( ( w ` 0 ) .- ( ( S ` ( w ` 1 ) ) ` ( w ` 2 ) ) ) ) } <-> ( ( # ` <" A B C "> ) = 3 /\ ( ( <" A B C "> ` 0 ) .- ( <" A B C "> ` 2 ) ) = ( ( <" A B C "> ` 0 ) .- ( ( S ` ( <" A B C "> ` 1 ) ) ` ( <" A B C "> ` 2 ) ) ) ) ) )
23 df-rag 
 |-  raG = ( g e. _V |-> { w e. Word ( Base ` g ) | ( ( # ` w ) = 3 /\ ( ( w ` 0 ) ( dist ` g ) ( w ` 2 ) ) = ( ( w ` 0 ) ( dist ` g ) ( ( ( pInvG ` g ) ` ( w ` 1 ) ) ` ( w ` 2 ) ) ) ) } )
24 simpr 
 |-  ( ( ph /\ g = G ) -> g = G )
25 24 fveq2d 
 |-  ( ( ph /\ g = G ) -> ( Base ` g ) = ( Base ` G ) )
26 25 1 eqtr4di 
 |-  ( ( ph /\ g = G ) -> ( Base ` g ) = P )
27 wrdeq 
 |-  ( ( Base ` g ) = P -> Word ( Base ` g ) = Word P )
28 26 27 syl 
 |-  ( ( ph /\ g = G ) -> Word ( Base ` g ) = Word P )
29 24 fveq2d 
 |-  ( ( ph /\ g = G ) -> ( dist ` g ) = ( dist ` G ) )
30 29 2 eqtr4di 
 |-  ( ( ph /\ g = G ) -> ( dist ` g ) = .- )
31 30 oveqd 
 |-  ( ( ph /\ g = G ) -> ( ( w ` 0 ) ( dist ` g ) ( w ` 2 ) ) = ( ( w ` 0 ) .- ( w ` 2 ) ) )
32 eqidd 
 |-  ( ( ph /\ g = G ) -> ( w ` 0 ) = ( w ` 0 ) )
33 24 fveq2d 
 |-  ( ( ph /\ g = G ) -> ( pInvG ` g ) = ( pInvG ` G ) )
34 33 5 eqtr4di 
 |-  ( ( ph /\ g = G ) -> ( pInvG ` g ) = S )
35 34 fveq1d 
 |-  ( ( ph /\ g = G ) -> ( ( pInvG ` g ) ` ( w ` 1 ) ) = ( S ` ( w ` 1 ) ) )
36 35 fveq1d 
 |-  ( ( ph /\ g = G ) -> ( ( ( pInvG ` g ) ` ( w ` 1 ) ) ` ( w ` 2 ) ) = ( ( S ` ( w ` 1 ) ) ` ( w ` 2 ) ) )
37 30 32 36 oveq123d 
 |-  ( ( ph /\ g = G ) -> ( ( w ` 0 ) ( dist ` g ) ( ( ( pInvG ` g ) ` ( w ` 1 ) ) ` ( w ` 2 ) ) ) = ( ( w ` 0 ) .- ( ( S ` ( w ` 1 ) ) ` ( w ` 2 ) ) ) )
38 31 37 eqeq12d 
 |-  ( ( ph /\ g = G ) -> ( ( ( w ` 0 ) ( dist ` g ) ( w ` 2 ) ) = ( ( w ` 0 ) ( dist ` g ) ( ( ( pInvG ` g ) ` ( w ` 1 ) ) ` ( w ` 2 ) ) ) <-> ( ( w ` 0 ) .- ( w ` 2 ) ) = ( ( w ` 0 ) .- ( ( S ` ( w ` 1 ) ) ` ( w ` 2 ) ) ) ) )
39 38 anbi2d 
 |-  ( ( ph /\ g = G ) -> ( ( ( # ` w ) = 3 /\ ( ( w ` 0 ) ( dist ` g ) ( w ` 2 ) ) = ( ( w ` 0 ) ( dist ` g ) ( ( ( pInvG ` g ) ` ( w ` 1 ) ) ` ( w ` 2 ) ) ) ) <-> ( ( # ` w ) = 3 /\ ( ( w ` 0 ) .- ( w ` 2 ) ) = ( ( w ` 0 ) .- ( ( S ` ( w ` 1 ) ) ` ( w ` 2 ) ) ) ) ) )
40 28 39 rabeqbidv 
 |-  ( ( ph /\ g = G ) -> { w e. Word ( Base ` g ) | ( ( # ` w ) = 3 /\ ( ( w ` 0 ) ( dist ` g ) ( w ` 2 ) ) = ( ( w ` 0 ) ( dist ` g ) ( ( ( pInvG ` g ) ` ( w ` 1 ) ) ` ( w ` 2 ) ) ) ) } = { w e. Word P | ( ( # ` w ) = 3 /\ ( ( w ` 0 ) .- ( w ` 2 ) ) = ( ( w ` 0 ) .- ( ( S ` ( w ` 1 ) ) ` ( w ` 2 ) ) ) ) } )
41 6 elexd 
 |-  ( ph -> G e. _V )
42 1 fvexi 
 |-  P e. _V
43 42 wrdexi 
 |-  Word P e. _V
44 43 rabex 
 |-  { w e. Word P | ( ( # ` w ) = 3 /\ ( ( w ` 0 ) .- ( w ` 2 ) ) = ( ( w ` 0 ) .- ( ( S ` ( w ` 1 ) ) ` ( w ` 2 ) ) ) ) } e. _V
45 44 a1i 
 |-  ( ph -> { w e. Word P | ( ( # ` w ) = 3 /\ ( ( w ` 0 ) .- ( w ` 2 ) ) = ( ( w ` 0 ) .- ( ( S ` ( w ` 1 ) ) ` ( w ` 2 ) ) ) ) } e. _V )
46 23 40 41 45 fvmptd2 
 |-  ( ph -> ( raG ` G ) = { w e. Word P | ( ( # ` w ) = 3 /\ ( ( w ` 0 ) .- ( w ` 2 ) ) = ( ( w ` 0 ) .- ( ( S ` ( w ` 1 ) ) ` ( w ` 2 ) ) ) ) } )
47 46 eleq2d 
 |-  ( ph -> ( <" A B C "> e. ( raG ` G ) <-> <" A B C "> e. { w e. Word P | ( ( # ` w ) = 3 /\ ( ( w ` 0 ) .- ( w ` 2 ) ) = ( ( w ` 0 ) .- ( ( S ` ( w ` 1 ) ) ` ( w ` 2 ) ) ) ) } ) )
48 s3fv0 
 |-  ( A e. P -> ( <" A B C "> ` 0 ) = A )
49 7 48 syl 
 |-  ( ph -> ( <" A B C "> ` 0 ) = A )
50 49 eqcomd 
 |-  ( ph -> A = ( <" A B C "> ` 0 ) )
51 s3fv2 
 |-  ( C e. P -> ( <" A B C "> ` 2 ) = C )
52 9 51 syl 
 |-  ( ph -> ( <" A B C "> ` 2 ) = C )
53 52 eqcomd 
 |-  ( ph -> C = ( <" A B C "> ` 2 ) )
54 50 53 oveq12d 
 |-  ( ph -> ( A .- C ) = ( ( <" A B C "> ` 0 ) .- ( <" A B C "> ` 2 ) ) )
55 s3fv1 
 |-  ( B e. P -> ( <" A B C "> ` 1 ) = B )
56 8 55 syl 
 |-  ( ph -> ( <" A B C "> ` 1 ) = B )
57 56 eqcomd 
 |-  ( ph -> B = ( <" A B C "> ` 1 ) )
58 57 fveq2d 
 |-  ( ph -> ( S ` B ) = ( S ` ( <" A B C "> ` 1 ) ) )
59 58 53 fveq12d 
 |-  ( ph -> ( ( S ` B ) ` C ) = ( ( S ` ( <" A B C "> ` 1 ) ) ` ( <" A B C "> ` 2 ) ) )
60 50 59 oveq12d 
 |-  ( ph -> ( A .- ( ( S ` B ) ` C ) ) = ( ( <" A B C "> ` 0 ) .- ( ( S ` ( <" A B C "> ` 1 ) ) ` ( <" A B C "> ` 2 ) ) ) )
61 54 60 eqeq12d 
 |-  ( ph -> ( ( A .- C ) = ( A .- ( ( S ` B ) ` C ) ) <-> ( ( <" A B C "> ` 0 ) .- ( <" A B C "> ` 2 ) ) = ( ( <" A B C "> ` 0 ) .- ( ( S ` ( <" A B C "> ` 1 ) ) ` ( <" A B C "> ` 2 ) ) ) ) )
62 s3len 
 |-  ( # ` <" A B C "> ) = 3
63 62 a1i 
 |-  ( ph -> ( # ` <" A B C "> ) = 3 )
64 63 biantrurd 
 |-  ( ph -> ( ( ( <" A B C "> ` 0 ) .- ( <" A B C "> ` 2 ) ) = ( ( <" A B C "> ` 0 ) .- ( ( S ` ( <" A B C "> ` 1 ) ) ` ( <" A B C "> ` 2 ) ) ) <-> ( ( # ` <" A B C "> ) = 3 /\ ( ( <" A B C "> ` 0 ) .- ( <" A B C "> ` 2 ) ) = ( ( <" A B C "> ` 0 ) .- ( ( S ` ( <" A B C "> ` 1 ) ) ` ( <" A B C "> ` 2 ) ) ) ) ) )
65 61 64 bitrd 
 |-  ( ph -> ( ( A .- C ) = ( A .- ( ( S ` B ) ` C ) ) <-> ( ( # ` <" A B C "> ) = 3 /\ ( ( <" A B C "> ` 0 ) .- ( <" A B C "> ` 2 ) ) = ( ( <" A B C "> ` 0 ) .- ( ( S ` ( <" A B C "> ` 1 ) ) ` ( <" A B C "> ` 2 ) ) ) ) ) )
66 22 47 65 3bitr4d 
 |-  ( ph -> ( <" A B C "> e. ( raG ` G ) <-> ( A .- C ) = ( A .- ( ( S ` B ) ` C ) ) ) )