Metamath Proof Explorer

Theorem isinag

Description: Property for point X to lie in the angle <" A B C "> . Definition 11.23 of Schwabhauser p. 101. (Contributed by Thierry Arnoux, 15-Aug-2020)

Ref Expression
Hypotheses isinag.p 
|- P = ( Base ` G )
isinag.i 
|- I = ( Itv ` G )
isinag.k 
|- K = ( hlG ` G )
isinag.x 
|- ( ph -> X e. P )
isinag.a 
|- ( ph -> A e. P )
isinag.b 
|- ( ph -> B e. P )
isinag.c 
|- ( ph -> C e. P )
isinag.g 
|- ( ph -> G e. V )
Assertion isinag 
|- ( ph -> ( X ( inA ` G ) <" A B C "> <-> ( ( A =/= B /\ C =/= B /\ X =/= B ) /\ E. x e. P ( x e. ( A I C ) /\ ( x = B \/ x ( K ` B ) X ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isinag.p 
 |-  P = ( Base ` G )
2 isinag.i 
 |-  I = ( Itv ` G )
3 isinag.k 
 |-  K = ( hlG ` G )
4 isinag.x 
 |-  ( ph -> X e. P )
5 isinag.a 
 |-  ( ph -> A e. P )
6 isinag.b 
 |-  ( ph -> B e. P )
7 isinag.c 
 |-  ( ph -> C e. P )
8 isinag.g 
 |-  ( ph -> G e. V )
9 simpr 
 |-  ( ( p = X /\ t = <" A B C "> ) -> t = <" A B C "> )
10 9 fveq1d 
 |-  ( ( p = X /\ t = <" A B C "> ) -> ( t ` 0 ) = ( <" A B C "> ` 0 ) )
11 9 fveq1d 
 |-  ( ( p = X /\ t = <" A B C "> ) -> ( t ` 1 ) = ( <" A B C "> ` 1 ) )
12 10 11 neeq12d 
 |-  ( ( p = X /\ t = <" A B C "> ) -> ( ( t ` 0 ) =/= ( t ` 1 ) <-> ( <" A B C "> ` 0 ) =/= ( <" A B C "> ` 1 ) ) )
13 9 fveq1d 
 |-  ( ( p = X /\ t = <" A B C "> ) -> ( t ` 2 ) = ( <" A B C "> ` 2 ) )
14 13 11 neeq12d 
 |-  ( ( p = X /\ t = <" A B C "> ) -> ( ( t ` 2 ) =/= ( t ` 1 ) <-> ( <" A B C "> ` 2 ) =/= ( <" A B C "> ` 1 ) ) )
15 simpl 
 |-  ( ( p = X /\ t = <" A B C "> ) -> p = X )
16 15 11 neeq12d 
 |-  ( ( p = X /\ t = <" A B C "> ) -> ( p =/= ( t ` 1 ) <-> X =/= ( <" A B C "> ` 1 ) ) )
17 12 14 16 3anbi123d 
 |-  ( ( p = X /\ t = <" A B C "> ) -> ( ( ( t ` 0 ) =/= ( t ` 1 ) /\ ( t ` 2 ) =/= ( t ` 1 ) /\ p =/= ( t ` 1 ) ) <-> ( ( <" A B C "> ` 0 ) =/= ( <" A B C "> ` 1 ) /\ ( <" A B C "> ` 2 ) =/= ( <" A B C "> ` 1 ) /\ X =/= ( <" A B C "> ` 1 ) ) ) )
18 10 13 oveq12d 
 |-  ( ( p = X /\ t = <" A B C "> ) -> ( ( t ` 0 ) I ( t ` 2 ) ) = ( ( <" A B C "> ` 0 ) I ( <" A B C "> ` 2 ) ) )
19 18 eleq2d 
 |-  ( ( p = X /\ t = <" A B C "> ) -> ( x e. ( ( t ` 0 ) I ( t ` 2 ) ) <-> x e. ( ( <" A B C "> ` 0 ) I ( <" A B C "> ` 2 ) ) ) )
20 11 eqeq2d 
 |-  ( ( p = X /\ t = <" A B C "> ) -> ( x = ( t ` 1 ) <-> x = ( <" A B C "> ` 1 ) ) )
21 eqidd 
 |-  ( ( p = X /\ t = <" A B C "> ) -> x = x )
22 11 fveq2d 
 |-  ( ( p = X /\ t = <" A B C "> ) -> ( K ` ( t ` 1 ) ) = ( K ` ( <" A B C "> ` 1 ) ) )
23 21 22 15 breq123d 
 |-  ( ( p = X /\ t = <" A B C "> ) -> ( x ( K ` ( t ` 1 ) ) p <-> x ( K ` ( <" A B C "> ` 1 ) ) X ) )
24 20 23 orbi12d 
 |-  ( ( p = X /\ t = <" A B C "> ) -> ( ( x = ( t ` 1 ) \/ x ( K ` ( t ` 1 ) ) p ) <-> ( x = ( <" A B C "> ` 1 ) \/ x ( K ` ( <" A B C "> ` 1 ) ) X ) ) )
25 19 24 anbi12d 
 |-  ( ( p = X /\ t = <" A B C "> ) -> ( ( x e. ( ( t ` 0 ) I ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( K ` ( t ` 1 ) ) p ) ) <-> ( x e. ( ( <" A B C "> ` 0 ) I ( <" A B C "> ` 2 ) ) /\ ( x = ( <" A B C "> ` 1 ) \/ x ( K ` ( <" A B C "> ` 1 ) ) X ) ) ) )
26 25 rexbidv 
 |-  ( ( p = X /\ t = <" A B C "> ) -> ( E. x e. P ( x e. ( ( t ` 0 ) I ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( K ` ( t ` 1 ) ) p ) ) <-> E. x e. P ( x e. ( ( <" A B C "> ` 0 ) I ( <" A B C "> ` 2 ) ) /\ ( x = ( <" A B C "> ` 1 ) \/ x ( K ` ( <" A B C "> ` 1 ) ) X ) ) ) )
27 17 26 anbi12d 
 |-  ( ( p = X /\ t = <" A B C "> ) -> ( ( ( ( t ` 0 ) =/= ( t ` 1 ) /\ ( t ` 2 ) =/= ( t ` 1 ) /\ p =/= ( t ` 1 ) ) /\ E. x e. P ( x e. ( ( t ` 0 ) I ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( K ` ( t ` 1 ) ) p ) ) ) <-> ( ( ( <" A B C "> ` 0 ) =/= ( <" A B C "> ` 1 ) /\ ( <" A B C "> ` 2 ) =/= ( <" A B C "> ` 1 ) /\ X =/= ( <" A B C "> ` 1 ) ) /\ E. x e. P ( x e. ( ( <" A B C "> ` 0 ) I ( <" A B C "> ` 2 ) ) /\ ( x = ( <" A B C "> ` 1 ) \/ x ( K ` ( <" A B C "> ` 1 ) ) X ) ) ) ) )
28 eqid 
 |-  { <. p , t >. | ( ( p e. P /\ t e. ( P ^m ( 0 ..^ 3 ) ) ) /\ ( ( ( t ` 0 ) =/= ( t ` 1 ) /\ ( t ` 2 ) =/= ( t ` 1 ) /\ p =/= ( t ` 1 ) ) /\ E. x e. P ( x e. ( ( t ` 0 ) I ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( K ` ( t ` 1 ) ) p ) ) ) ) } = { <. p , t >. | ( ( p e. P /\ t e. ( P ^m ( 0 ..^ 3 ) ) ) /\ ( ( ( t ` 0 ) =/= ( t ` 1 ) /\ ( t ` 2 ) =/= ( t ` 1 ) /\ p =/= ( t ` 1 ) ) /\ E. x e. P ( x e. ( ( t ` 0 ) I ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( K ` ( t ` 1 ) ) p ) ) ) ) }
29 27 28 brab2a 
 |-  ( X { <. p , t >. | ( ( p e. P /\ t e. ( P ^m ( 0 ..^ 3 ) ) ) /\ ( ( ( t ` 0 ) =/= ( t ` 1 ) /\ ( t ` 2 ) =/= ( t ` 1 ) /\ p =/= ( t ` 1 ) ) /\ E. x e. P ( x e. ( ( t ` 0 ) I ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( K ` ( t ` 1 ) ) p ) ) ) ) } <" A B C "> <-> ( ( X e. P /\ <" A B C "> e. ( P ^m ( 0 ..^ 3 ) ) ) /\ ( ( ( <" A B C "> ` 0 ) =/= ( <" A B C "> ` 1 ) /\ ( <" A B C "> ` 2 ) =/= ( <" A B C "> ` 1 ) /\ X =/= ( <" A B C "> ` 1 ) ) /\ E. x e. P ( x e. ( ( <" A B C "> ` 0 ) I ( <" A B C "> ` 2 ) ) /\ ( x = ( <" A B C "> ` 1 ) \/ x ( K ` ( <" A B C "> ` 1 ) ) X ) ) ) ) )
30 s3fv0 
 |-  ( A e. P -> ( <" A B C "> ` 0 ) = A )
31 5 30 syl 
 |-  ( ph -> ( <" A B C "> ` 0 ) = A )
32 s3fv1 
 |-  ( B e. P -> ( <" A B C "> ` 1 ) = B )
33 6 32 syl 
 |-  ( ph -> ( <" A B C "> ` 1 ) = B )
34 31 33 neeq12d 
 |-  ( ph -> ( ( <" A B C "> ` 0 ) =/= ( <" A B C "> ` 1 ) <-> A =/= B ) )
35 s3fv2 
 |-  ( C e. P -> ( <" A B C "> ` 2 ) = C )
36 7 35 syl 
 |-  ( ph -> ( <" A B C "> ` 2 ) = C )
37 36 33 neeq12d 
 |-  ( ph -> ( ( <" A B C "> ` 2 ) =/= ( <" A B C "> ` 1 ) <-> C =/= B ) )
38 33 neeq2d 
 |-  ( ph -> ( X =/= ( <" A B C "> ` 1 ) <-> X =/= B ) )
39 34 37 38 3anbi123d 
 |-  ( ph -> ( ( ( <" A B C "> ` 0 ) =/= ( <" A B C "> ` 1 ) /\ ( <" A B C "> ` 2 ) =/= ( <" A B C "> ` 1 ) /\ X =/= ( <" A B C "> ` 1 ) ) <-> ( A =/= B /\ C =/= B /\ X =/= B ) ) )
40 31 36 oveq12d 
 |-  ( ph -> ( ( <" A B C "> ` 0 ) I ( <" A B C "> ` 2 ) ) = ( A I C ) )
41 40 eleq2d 
 |-  ( ph -> ( x e. ( ( <" A B C "> ` 0 ) I ( <" A B C "> ` 2 ) ) <-> x e. ( A I C ) ) )
42 33 eqeq2d 
 |-  ( ph -> ( x = ( <" A B C "> ` 1 ) <-> x = B ) )
43 33 fveq2d 
 |-  ( ph -> ( K ` ( <" A B C "> ` 1 ) ) = ( K ` B ) )
44 43 breqd 
 |-  ( ph -> ( x ( K ` ( <" A B C "> ` 1 ) ) X <-> x ( K ` B ) X ) )
45 42 44 orbi12d 
 |-  ( ph -> ( ( x = ( <" A B C "> ` 1 ) \/ x ( K ` ( <" A B C "> ` 1 ) ) X ) <-> ( x = B \/ x ( K ` B ) X ) ) )
46 41 45 anbi12d 
 |-  ( ph -> ( ( x e. ( ( <" A B C "> ` 0 ) I ( <" A B C "> ` 2 ) ) /\ ( x = ( <" A B C "> ` 1 ) \/ x ( K ` ( <" A B C "> ` 1 ) ) X ) ) <-> ( x e. ( A I C ) /\ ( x = B \/ x ( K ` B ) X ) ) ) )
47 46 rexbidv 
 |-  ( ph -> ( E. x e. P ( x e. ( ( <" A B C "> ` 0 ) I ( <" A B C "> ` 2 ) ) /\ ( x = ( <" A B C "> ` 1 ) \/ x ( K ` ( <" A B C "> ` 1 ) ) X ) ) <-> E. x e. P ( x e. ( A I C ) /\ ( x = B \/ x ( K ` B ) X ) ) ) )
48 39 47 anbi12d 
 |-  ( ph -> ( ( ( ( <" A B C "> ` 0 ) =/= ( <" A B C "> ` 1 ) /\ ( <" A B C "> ` 2 ) =/= ( <" A B C "> ` 1 ) /\ X =/= ( <" A B C "> ` 1 ) ) /\ E. x e. P ( x e. ( ( <" A B C "> ` 0 ) I ( <" A B C "> ` 2 ) ) /\ ( x = ( <" A B C "> ` 1 ) \/ x ( K ` ( <" A B C "> ` 1 ) ) X ) ) ) <-> ( ( A =/= B /\ C =/= B /\ X =/= B ) /\ E. x e. P ( x e. ( A I C ) /\ ( x = B \/ x ( K ` B ) X ) ) ) ) )
49 48 anbi2d 
 |-  ( ph -> ( ( ( X e. P /\ <" A B C "> e. ( P ^m ( 0 ..^ 3 ) ) ) /\ ( ( ( <" A B C "> ` 0 ) =/= ( <" A B C "> ` 1 ) /\ ( <" A B C "> ` 2 ) =/= ( <" A B C "> ` 1 ) /\ X =/= ( <" A B C "> ` 1 ) ) /\ E. x e. P ( x e. ( ( <" A B C "> ` 0 ) I ( <" A B C "> ` 2 ) ) /\ ( x = ( <" A B C "> ` 1 ) \/ x ( K ` ( <" A B C "> ` 1 ) ) X ) ) ) ) <-> ( ( X e. P /\ <" A B C "> e. ( P ^m ( 0 ..^ 3 ) ) ) /\ ( ( A =/= B /\ C =/= B /\ X =/= B ) /\ E. x e. P ( x e. ( A I C ) /\ ( x = B \/ x ( K ` B ) X ) ) ) ) ) )
50 29 49 syl5bb 
 |-  ( ph -> ( X { <. p , t >. | ( ( p e. P /\ t e. ( P ^m ( 0 ..^ 3 ) ) ) /\ ( ( ( t ` 0 ) =/= ( t ` 1 ) /\ ( t ` 2 ) =/= ( t ` 1 ) /\ p =/= ( t ` 1 ) ) /\ E. x e. P ( x e. ( ( t ` 0 ) I ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( K ` ( t ` 1 ) ) p ) ) ) ) } <" A B C "> <-> ( ( X e. P /\ <" A B C "> e. ( P ^m ( 0 ..^ 3 ) ) ) /\ ( ( A =/= B /\ C =/= B /\ X =/= B ) /\ E. x e. P ( x e. ( A I C ) /\ ( x = B \/ x ( K ` B ) X ) ) ) ) ) )
51 elex 
 |-  ( G e. V -> G e. _V )
52 fveq2 
 |-  ( g = G -> ( Base ` g ) = ( Base ` G ) )
53 52 1 eqtr4di 
 |-  ( g = G -> ( Base ` g ) = P )
54 53 eleq2d 
 |-  ( g = G -> ( p e. ( Base ` g ) <-> p e. P ) )
55 53 oveq1d 
 |-  ( g = G -> ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) = ( P ^m ( 0 ..^ 3 ) ) )
56 55 eleq2d 
 |-  ( g = G -> ( t e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) <-> t e. ( P ^m ( 0 ..^ 3 ) ) ) )
57 54 56 anbi12d 
 |-  ( g = G -> ( ( p e. ( Base ` g ) /\ t e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) ) <-> ( p e. P /\ t e. ( P ^m ( 0 ..^ 3 ) ) ) ) )
58 fveq2 
 |-  ( g = G -> ( Itv ` g ) = ( Itv ` G ) )
59 58 2 eqtr4di 
 |-  ( g = G -> ( Itv ` g ) = I )
60 59 oveqd 
 |-  ( g = G -> ( ( t ` 0 ) ( Itv ` g ) ( t ` 2 ) ) = ( ( t ` 0 ) I ( t ` 2 ) ) )
61 60 eleq2d 
 |-  ( g = G -> ( x e. ( ( t ` 0 ) ( Itv ` g ) ( t ` 2 ) ) <-> x e. ( ( t ` 0 ) I ( t ` 2 ) ) ) )
62 fveq2 
 |-  ( g = G -> ( hlG ` g ) = ( hlG ` G ) )
63 62 3 eqtr4di 
 |-  ( g = G -> ( hlG ` g ) = K )
64 63 fveq1d 
 |-  ( g = G -> ( ( hlG ` g ) ` ( t ` 1 ) ) = ( K ` ( t ` 1 ) ) )
65 64 breqd 
 |-  ( g = G -> ( x ( ( hlG ` g ) ` ( t ` 1 ) ) p <-> x ( K ` ( t ` 1 ) ) p ) )
66 65 orbi2d 
 |-  ( g = G -> ( ( x = ( t ` 1 ) \/ x ( ( hlG ` g ) ` ( t ` 1 ) ) p ) <-> ( x = ( t ` 1 ) \/ x ( K ` ( t ` 1 ) ) p ) ) )
67 61 66 anbi12d 
 |-  ( g = G -> ( ( x e. ( ( t ` 0 ) ( Itv ` g ) ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( ( hlG ` g ) ` ( t ` 1 ) ) p ) ) <-> ( x e. ( ( t ` 0 ) I ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( K ` ( t ` 1 ) ) p ) ) ) )
68 53 67 rexeqbidv 
 |-  ( g = G -> ( E. x e. ( Base ` g ) ( x e. ( ( t ` 0 ) ( Itv ` g ) ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( ( hlG ` g ) ` ( t ` 1 ) ) p ) ) <-> E. x e. P ( x e. ( ( t ` 0 ) I ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( K ` ( t ` 1 ) ) p ) ) ) )
69 68 anbi2d 
 |-  ( g = G -> ( ( ( ( t ` 0 ) =/= ( t ` 1 ) /\ ( t ` 2 ) =/= ( t ` 1 ) /\ p =/= ( t ` 1 ) ) /\ E. x e. ( Base ` g ) ( x e. ( ( t ` 0 ) ( Itv ` g ) ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( ( hlG ` g ) ` ( t ` 1 ) ) p ) ) ) <-> ( ( ( t ` 0 ) =/= ( t ` 1 ) /\ ( t ` 2 ) =/= ( t ` 1 ) /\ p =/= ( t ` 1 ) ) /\ E. x e. P ( x e. ( ( t ` 0 ) I ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( K ` ( t ` 1 ) ) p ) ) ) ) )
70 57 69 anbi12d 
 |-  ( g = G -> ( ( ( p e. ( Base ` g ) /\ t e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) ) /\ ( ( ( t ` 0 ) =/= ( t ` 1 ) /\ ( t ` 2 ) =/= ( t ` 1 ) /\ p =/= ( t ` 1 ) ) /\ E. x e. ( Base ` g ) ( x e. ( ( t ` 0 ) ( Itv ` g ) ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( ( hlG ` g ) ` ( t ` 1 ) ) p ) ) ) ) <-> ( ( p e. P /\ t e. ( P ^m ( 0 ..^ 3 ) ) ) /\ ( ( ( t ` 0 ) =/= ( t ` 1 ) /\ ( t ` 2 ) =/= ( t ` 1 ) /\ p =/= ( t ` 1 ) ) /\ E. x e. P ( x e. ( ( t ` 0 ) I ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( K ` ( t ` 1 ) ) p ) ) ) ) ) )
71 70 opabbidv 
 |-  ( g = G -> { <. p , t >. | ( ( p e. ( Base ` g ) /\ t e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) ) /\ ( ( ( t ` 0 ) =/= ( t ` 1 ) /\ ( t ` 2 ) =/= ( t ` 1 ) /\ p =/= ( t ` 1 ) ) /\ E. x e. ( Base ` g ) ( x e. ( ( t ` 0 ) ( Itv ` g ) ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( ( hlG ` g ) ` ( t ` 1 ) ) p ) ) ) ) } = { <. p , t >. | ( ( p e. P /\ t e. ( P ^m ( 0 ..^ 3 ) ) ) /\ ( ( ( t ` 0 ) =/= ( t ` 1 ) /\ ( t ` 2 ) =/= ( t ` 1 ) /\ p =/= ( t ` 1 ) ) /\ E. x e. P ( x e. ( ( t ` 0 ) I ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( K ` ( t ` 1 ) ) p ) ) ) ) } )
72 df-inag 
 |-  inA = ( g e. _V |-> { <. p , t >. | ( ( p e. ( Base ` g ) /\ t e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) ) /\ ( ( ( t ` 0 ) =/= ( t ` 1 ) /\ ( t ` 2 ) =/= ( t ` 1 ) /\ p =/= ( t ` 1 ) ) /\ E. x e. ( Base ` g ) ( x e. ( ( t ` 0 ) ( Itv ` g ) ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( ( hlG ` g ) ` ( t ` 1 ) ) p ) ) ) ) } )
73 1 fvexi 
 |-  P e. _V
74 ovex 
 |-  ( P ^m ( 0 ..^ 3 ) ) e. _V
75 73 74 xpex 
 |-  ( P X. ( P ^m ( 0 ..^ 3 ) ) ) e. _V
76 opabssxp 
 |-  { <. p , t >. | ( ( p e. P /\ t e. ( P ^m ( 0 ..^ 3 ) ) ) /\ ( ( ( t ` 0 ) =/= ( t ` 1 ) /\ ( t ` 2 ) =/= ( t ` 1 ) /\ p =/= ( t ` 1 ) ) /\ E. x e. P ( x e. ( ( t ` 0 ) I ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( K ` ( t ` 1 ) ) p ) ) ) ) } C_ ( P X. ( P ^m ( 0 ..^ 3 ) ) )
77 75 76 ssexi 
 |-  { <. p , t >. | ( ( p e. P /\ t e. ( P ^m ( 0 ..^ 3 ) ) ) /\ ( ( ( t ` 0 ) =/= ( t ` 1 ) /\ ( t ` 2 ) =/= ( t ` 1 ) /\ p =/= ( t ` 1 ) ) /\ E. x e. P ( x e. ( ( t ` 0 ) I ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( K ` ( t ` 1 ) ) p ) ) ) ) } e. _V
78 71 72 77 fvmpt 
 |-  ( G e. _V -> ( inA ` G ) = { <. p , t >. | ( ( p e. P /\ t e. ( P ^m ( 0 ..^ 3 ) ) ) /\ ( ( ( t ` 0 ) =/= ( t ` 1 ) /\ ( t ` 2 ) =/= ( t ` 1 ) /\ p =/= ( t ` 1 ) ) /\ E. x e. P ( x e. ( ( t ` 0 ) I ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( K ` ( t ` 1 ) ) p ) ) ) ) } )
79 8 51 78 3syl 
 |-  ( ph -> ( inA ` G ) = { <. p , t >. | ( ( p e. P /\ t e. ( P ^m ( 0 ..^ 3 ) ) ) /\ ( ( ( t ` 0 ) =/= ( t ` 1 ) /\ ( t ` 2 ) =/= ( t ` 1 ) /\ p =/= ( t ` 1 ) ) /\ E. x e. P ( x e. ( ( t ` 0 ) I ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( K ` ( t ` 1 ) ) p ) ) ) ) } )
80 79 breqd 
 |-  ( ph -> ( X ( inA ` G ) <" A B C "> <-> X { <. p , t >. | ( ( p e. P /\ t e. ( P ^m ( 0 ..^ 3 ) ) ) /\ ( ( ( t ` 0 ) =/= ( t ` 1 ) /\ ( t ` 2 ) =/= ( t ` 1 ) /\ p =/= ( t ` 1 ) ) /\ E. x e. P ( x e. ( ( t ` 0 ) I ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( K ` ( t ` 1 ) ) p ) ) ) ) } <" A B C "> ) )
81 5 6 7 s3cld 
 |-  ( ph -> <" A B C "> e. Word P )
82 s3len 
 |-  ( # ` <" A B C "> ) = 3
83 3nn0 
 |-  3 e. NN0
84 wrdmap 
 |-  ( ( P e. _V /\ 3 e. NN0 ) -> ( ( <" A B C "> e. Word P /\ ( # ` <" A B C "> ) = 3 ) <-> <" A B C "> e. ( P ^m ( 0 ..^ 3 ) ) ) )
85 73 83 84 mp2an 
 |-  ( ( <" A B C "> e. Word P /\ ( # ` <" A B C "> ) = 3 ) <-> <" A B C "> e. ( P ^m ( 0 ..^ 3 ) ) )
86 81 82 85 sylanblc 
 |-  ( ph -> <" A B C "> e. ( P ^m ( 0 ..^ 3 ) ) )
87 4 86 jca 
 |-  ( ph -> ( X e. P /\ <" A B C "> e. ( P ^m ( 0 ..^ 3 ) ) ) )
88 87 biantrurd 
 |-  ( ph -> ( ( ( A =/= B /\ C =/= B /\ X =/= B ) /\ E. x e. P ( x e. ( A I C ) /\ ( x = B \/ x ( K ` B ) X ) ) ) <-> ( ( X e. P /\ <" A B C "> e. ( P ^m ( 0 ..^ 3 ) ) ) /\ ( ( A =/= B /\ C =/= B /\ X =/= B ) /\ E. x e. P ( x e. ( A I C ) /\ ( x = B \/ x ( K ` B ) X ) ) ) ) ) )
89 50 80 88 3bitr4d 
 |-  ( ph -> ( X ( inA ` G ) <" A B C "> <-> ( ( A =/= B /\ C =/= B /\ X =/= B ) /\ E. x e. P ( x e. ( A I C ) /\ ( x = B \/ x ( K ` B ) X ) ) ) ) )