Metamath Proof Explorer

Theorem isleag

Description: Geometrical "less than" property for angles. Definition 11.27 of Schwabhauser p. 102. (Contributed by Thierry Arnoux, 7-Oct-2020)

Ref Expression
Hypotheses isleag.p 
|- P = ( Base ` G )
isleag.g 
|- ( ph -> G e. TarskiG )
isleag.a 
|- ( ph -> A e. P )
isleag.b 
|- ( ph -> B e. P )
isleag.c 
|- ( ph -> C e. P )
isleag.d 
|- ( ph -> D e. P )
isleag.e 
|- ( ph -> E e. P )
isleag.f 
|- ( ph -> F e. P )
Assertion isleag 
|- ( ph -> ( <" A B C "> ( leA ` G ) <" D E F "> <-> E. x e. P ( x ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E x "> ) ) )

Proof

Step Hyp Ref Expression
1 isleag.p 
 |-  P = ( Base ` G )
2 isleag.g 
 |-  ( ph -> G e. TarskiG )
3 isleag.a 
 |-  ( ph -> A e. P )
4 isleag.b 
 |-  ( ph -> B e. P )
5 isleag.c 
 |-  ( ph -> C e. P )
6 isleag.d 
 |-  ( ph -> D e. P )
7 isleag.e 
 |-  ( ph -> E e. P )
8 isleag.f 
 |-  ( ph -> F e. P )
9 3 4 5 s3cld 
 |-  ( ph -> <" A B C "> e. Word P )
10 s3len 
 |-  ( # ` <" A B C "> ) = 3
11 1 fvexi 
 |-  P e. _V
12 3nn0 
 |-  3 e. NN0
13 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 ) ) ) )
14 11 12 13 mp2an 
 |-  ( ( <" A B C "> e. Word P /\ ( # ` <" A B C "> ) = 3 ) <-> <" A B C "> e. ( P ^m ( 0 ..^ 3 ) ) )
15 9 10 14 sylanblc 
 |-  ( ph -> <" A B C "> e. ( P ^m ( 0 ..^ 3 ) ) )
16 6 7 8 s3cld 
 |-  ( ph -> <" D E F "> e. Word P )
17 s3len 
 |-  ( # ` <" D E F "> ) = 3
18 wrdmap 
 |-  ( ( P e. _V /\ 3 e. NN0 ) -> ( ( <" D E F "> e. Word P /\ ( # ` <" D E F "> ) = 3 ) <-> <" D E F "> e. ( P ^m ( 0 ..^ 3 ) ) ) )
19 11 12 18 mp2an 
 |-  ( ( <" D E F "> e. Word P /\ ( # ` <" D E F "> ) = 3 ) <-> <" D E F "> e. ( P ^m ( 0 ..^ 3 ) ) )
20 16 17 19 sylanblc 
 |-  ( ph -> <" D E F "> e. ( P ^m ( 0 ..^ 3 ) ) )
21 15 20 jca 
 |-  ( ph -> ( <" A B C "> e. ( P ^m ( 0 ..^ 3 ) ) /\ <" D E F "> e. ( P ^m ( 0 ..^ 3 ) ) ) )
22 elex 
 |-  ( G e. TarskiG -> G e. _V )
23 fveq2 
 |-  ( g = G -> ( Base ` g ) = ( Base ` G ) )
24 23 1 eqtr4di 
 |-  ( g = G -> ( Base ` g ) = P )
25 24 oveq1d 
 |-  ( g = G -> ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) = ( P ^m ( 0 ..^ 3 ) ) )
26 25 eleq2d 
 |-  ( g = G -> ( a e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) <-> a e. ( P ^m ( 0 ..^ 3 ) ) ) )
27 25 eleq2d 
 |-  ( g = G -> ( b e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) <-> b e. ( P ^m ( 0 ..^ 3 ) ) ) )
28 26 27 anbi12d 
 |-  ( g = G -> ( ( a e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) /\ b e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) ) <-> ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ b e. ( P ^m ( 0 ..^ 3 ) ) ) ) )
29 fveq2 
 |-  ( g = G -> ( inA ` g ) = ( inA ` G ) )
30 29 breqd 
 |-  ( g = G -> ( x ( inA ` g ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> <-> x ( inA ` G ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> ) )
31 fveq2 
 |-  ( g = G -> ( cgrA ` g ) = ( cgrA ` G ) )
32 31 breqd 
 |-  ( g = G -> ( <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> ( cgrA ` g ) <" ( b ` 0 ) ( b ` 1 ) x "> <-> <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> ( cgrA ` G ) <" ( b ` 0 ) ( b ` 1 ) x "> ) )
33 30 32 anbi12d 
 |-  ( g = G -> ( ( x ( inA ` g ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> ( cgrA ` g ) <" ( b ` 0 ) ( b ` 1 ) x "> ) <-> ( x ( inA ` G ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> ( cgrA ` G ) <" ( b ` 0 ) ( b ` 1 ) x "> ) ) )
34 24 33 rexeqbidv 
 |-  ( g = G -> ( E. x e. ( Base ` g ) ( x ( inA ` g ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> ( cgrA ` g ) <" ( b ` 0 ) ( b ` 1 ) x "> ) <-> E. x e. P ( x ( inA ` G ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> ( cgrA ` G ) <" ( b ` 0 ) ( b ` 1 ) x "> ) ) )
35 28 34 anbi12d 
 |-  ( g = G -> ( ( ( a e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) /\ b e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) ) /\ E. x e. ( Base ` g ) ( x ( inA ` g ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> ( cgrA ` g ) <" ( b ` 0 ) ( b ` 1 ) x "> ) ) <-> ( ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ b e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P ( x ( inA ` G ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> ( cgrA ` G ) <" ( b ` 0 ) ( b ` 1 ) x "> ) ) ) )
36 35 opabbidv 
 |-  ( g = G -> { <. a , b >. | ( ( a e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) /\ b e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) ) /\ E. x e. ( Base ` g ) ( x ( inA ` g ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> ( cgrA ` g ) <" ( b ` 0 ) ( b ` 1 ) x "> ) ) } = { <. a , b >. | ( ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ b e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P ( x ( inA ` G ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> ( cgrA ` G ) <" ( b ` 0 ) ( b ` 1 ) x "> ) ) } )
37 df-leag 
 |-  leA = ( g e. _V |-> { <. a , b >. | ( ( a e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) /\ b e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) ) /\ E. x e. ( Base ` g ) ( x ( inA ` g ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> ( cgrA ` g ) <" ( b ` 0 ) ( b ` 1 ) x "> ) ) } )
38 ovex 
 |-  ( P ^m ( 0 ..^ 3 ) ) e. _V
39 38 38 xpex 
 |-  ( ( P ^m ( 0 ..^ 3 ) ) X. ( P ^m ( 0 ..^ 3 ) ) ) e. _V
40 opabssxp 
 |-  { <. a , b >. | ( ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ b e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P ( x ( inA ` G ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> ( cgrA ` G ) <" ( b ` 0 ) ( b ` 1 ) x "> ) ) } C_ ( ( P ^m ( 0 ..^ 3 ) ) X. ( P ^m ( 0 ..^ 3 ) ) )
41 39 40 ssexi 
 |-  { <. a , b >. | ( ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ b e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P ( x ( inA ` G ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> ( cgrA ` G ) <" ( b ` 0 ) ( b ` 1 ) x "> ) ) } e. _V
42 36 37 41 fvmpt 
 |-  ( G e. _V -> ( leA ` G ) = { <. a , b >. | ( ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ b e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P ( x ( inA ` G ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> ( cgrA ` G ) <" ( b ` 0 ) ( b ` 1 ) x "> ) ) } )
43 2 22 42 3syl 
 |-  ( ph -> ( leA ` G ) = { <. a , b >. | ( ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ b e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P ( x ( inA ` G ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> ( cgrA ` G ) <" ( b ` 0 ) ( b ` 1 ) x "> ) ) } )
44 43 breqd 
 |-  ( ph -> ( <" A B C "> ( leA ` G ) <" D E F "> <-> <" A B C "> { <. a , b >. | ( ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ b e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P ( x ( inA ` G ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> ( cgrA ` G ) <" ( b ` 0 ) ( b ` 1 ) x "> ) ) } <" D E F "> ) )
45 simpr 
 |-  ( ( a = <" A B C "> /\ b = <" D E F "> ) -> b = <" D E F "> )
46 45 fveq1d 
 |-  ( ( a = <" A B C "> /\ b = <" D E F "> ) -> ( b ` 0 ) = ( <" D E F "> ` 0 ) )
47 45 fveq1d 
 |-  ( ( a = <" A B C "> /\ b = <" D E F "> ) -> ( b ` 1 ) = ( <" D E F "> ` 1 ) )
48 45 fveq1d 
 |-  ( ( a = <" A B C "> /\ b = <" D E F "> ) -> ( b ` 2 ) = ( <" D E F "> ` 2 ) )
49 46 47 48 s3eqd 
 |-  ( ( a = <" A B C "> /\ b = <" D E F "> ) -> <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> = <" ( <" D E F "> ` 0 ) ( <" D E F "> ` 1 ) ( <" D E F "> ` 2 ) "> )
50 49 breq2d 
 |-  ( ( a = <" A B C "> /\ b = <" D E F "> ) -> ( x ( inA ` G ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> <-> x ( inA ` G ) <" ( <" D E F "> ` 0 ) ( <" D E F "> ` 1 ) ( <" D E F "> ` 2 ) "> ) )
51 simpl 
 |-  ( ( a = <" A B C "> /\ b = <" D E F "> ) -> a = <" A B C "> )
52 51 fveq1d 
 |-  ( ( a = <" A B C "> /\ b = <" D E F "> ) -> ( a ` 0 ) = ( <" A B C "> ` 0 ) )
53 51 fveq1d 
 |-  ( ( a = <" A B C "> /\ b = <" D E F "> ) -> ( a ` 1 ) = ( <" A B C "> ` 1 ) )
54 51 fveq1d 
 |-  ( ( a = <" A B C "> /\ b = <" D E F "> ) -> ( a ` 2 ) = ( <" A B C "> ` 2 ) )
55 52 53 54 s3eqd 
 |-  ( ( a = <" A B C "> /\ b = <" D E F "> ) -> <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> = <" ( <" A B C "> ` 0 ) ( <" A B C "> ` 1 ) ( <" A B C "> ` 2 ) "> )
56 eqidd 
 |-  ( ( a = <" A B C "> /\ b = <" D E F "> ) -> x = x )
57 46 47 56 s3eqd 
 |-  ( ( a = <" A B C "> /\ b = <" D E F "> ) -> <" ( b ` 0 ) ( b ` 1 ) x "> = <" ( <" D E F "> ` 0 ) ( <" D E F "> ` 1 ) x "> )
58 55 57 breq12d 
 |-  ( ( a = <" A B C "> /\ b = <" D E F "> ) -> ( <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> ( cgrA ` G ) <" ( b ` 0 ) ( b ` 1 ) x "> <-> <" ( <" A B C "> ` 0 ) ( <" A B C "> ` 1 ) ( <" A B C "> ` 2 ) "> ( cgrA ` G ) <" ( <" D E F "> ` 0 ) ( <" D E F "> ` 1 ) x "> ) )
59 50 58 anbi12d 
 |-  ( ( a = <" A B C "> /\ b = <" D E F "> ) -> ( ( x ( inA ` G ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> ( cgrA ` G ) <" ( b ` 0 ) ( b ` 1 ) x "> ) <-> ( x ( inA ` G ) <" ( <" D E F "> ` 0 ) ( <" D E F "> ` 1 ) ( <" D E F "> ` 2 ) "> /\ <" ( <" A B C "> ` 0 ) ( <" A B C "> ` 1 ) ( <" A B C "> ` 2 ) "> ( cgrA ` G ) <" ( <" D E F "> ` 0 ) ( <" D E F "> ` 1 ) x "> ) ) )
60 59 rexbidv 
 |-  ( ( a = <" A B C "> /\ b = <" D E F "> ) -> ( E. x e. P ( x ( inA ` G ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> ( cgrA ` G ) <" ( b ` 0 ) ( b ` 1 ) x "> ) <-> E. x e. P ( x ( inA ` G ) <" ( <" D E F "> ` 0 ) ( <" D E F "> ` 1 ) ( <" D E F "> ` 2 ) "> /\ <" ( <" A B C "> ` 0 ) ( <" A B C "> ` 1 ) ( <" A B C "> ` 2 ) "> ( cgrA ` G ) <" ( <" D E F "> ` 0 ) ( <" D E F "> ` 1 ) x "> ) ) )
61 eqid 
 |-  { <. a , b >. | ( ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ b e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P ( x ( inA ` G ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> ( cgrA ` G ) <" ( b ` 0 ) ( b ` 1 ) x "> ) ) } = { <. a , b >. | ( ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ b e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P ( x ( inA ` G ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> ( cgrA ` G ) <" ( b ` 0 ) ( b ` 1 ) x "> ) ) }
62 60 61 brab2a 
 |-  ( <" A B C "> { <. a , b >. | ( ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ b e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P ( x ( inA ` G ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> ( cgrA ` G ) <" ( b ` 0 ) ( b ` 1 ) x "> ) ) } <" D E F "> <-> ( ( <" A B C "> e. ( P ^m ( 0 ..^ 3 ) ) /\ <" D E F "> e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P ( x ( inA ` G ) <" ( <" D E F "> ` 0 ) ( <" D E F "> ` 1 ) ( <" D E F "> ` 2 ) "> /\ <" ( <" A B C "> ` 0 ) ( <" A B C "> ` 1 ) ( <" A B C "> ` 2 ) "> ( cgrA ` G ) <" ( <" D E F "> ` 0 ) ( <" D E F "> ` 1 ) x "> ) ) )
63 62 a1i 
 |-  ( ph -> ( <" A B C "> { <. a , b >. | ( ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ b e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P ( x ( inA ` G ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> ( cgrA ` G ) <" ( b ` 0 ) ( b ` 1 ) x "> ) ) } <" D E F "> <-> ( ( <" A B C "> e. ( P ^m ( 0 ..^ 3 ) ) /\ <" D E F "> e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P ( x ( inA ` G ) <" ( <" D E F "> ` 0 ) ( <" D E F "> ` 1 ) ( <" D E F "> ` 2 ) "> /\ <" ( <" A B C "> ` 0 ) ( <" A B C "> ` 1 ) ( <" A B C "> ` 2 ) "> ( cgrA ` G ) <" ( <" D E F "> ` 0 ) ( <" D E F "> ` 1 ) x "> ) ) ) )
64 s3fv0 
 |-  ( D e. P -> ( <" D E F "> ` 0 ) = D )
65 6 64 syl 
 |-  ( ph -> ( <" D E F "> ` 0 ) = D )
66 s3fv1 
 |-  ( E e. P -> ( <" D E F "> ` 1 ) = E )
67 7 66 syl 
 |-  ( ph -> ( <" D E F "> ` 1 ) = E )
68 s3fv2 
 |-  ( F e. P -> ( <" D E F "> ` 2 ) = F )
69 8 68 syl 
 |-  ( ph -> ( <" D E F "> ` 2 ) = F )
70 65 67 69 s3eqd 
 |-  ( ph -> <" ( <" D E F "> ` 0 ) ( <" D E F "> ` 1 ) ( <" D E F "> ` 2 ) "> = <" D E F "> )
71 70 breq2d 
 |-  ( ph -> ( x ( inA ` G ) <" ( <" D E F "> ` 0 ) ( <" D E F "> ` 1 ) ( <" D E F "> ` 2 ) "> <-> x ( inA ` G ) <" D E F "> ) )
72 s3fv0 
 |-  ( A e. P -> ( <" A B C "> ` 0 ) = A )
73 3 72 syl 
 |-  ( ph -> ( <" A B C "> ` 0 ) = A )
74 s3fv1 
 |-  ( B e. P -> ( <" A B C "> ` 1 ) = B )
75 4 74 syl 
 |-  ( ph -> ( <" A B C "> ` 1 ) = B )
76 s3fv2 
 |-  ( C e. P -> ( <" A B C "> ` 2 ) = C )
77 5 76 syl 
 |-  ( ph -> ( <" A B C "> ` 2 ) = C )
78 73 75 77 s3eqd 
 |-  ( ph -> <" ( <" A B C "> ` 0 ) ( <" A B C "> ` 1 ) ( <" A B C "> ` 2 ) "> = <" A B C "> )
79 eqidd 
 |-  ( ph -> x = x )
80 65 67 79 s3eqd 
 |-  ( ph -> <" ( <" D E F "> ` 0 ) ( <" D E F "> ` 1 ) x "> = <" D E x "> )
81 78 80 breq12d 
 |-  ( ph -> ( <" ( <" A B C "> ` 0 ) ( <" A B C "> ` 1 ) ( <" A B C "> ` 2 ) "> ( cgrA ` G ) <" ( <" D E F "> ` 0 ) ( <" D E F "> ` 1 ) x "> <-> <" A B C "> ( cgrA ` G ) <" D E x "> ) )
82 71 81 anbi12d 
 |-  ( ph -> ( ( x ( inA ` G ) <" ( <" D E F "> ` 0 ) ( <" D E F "> ` 1 ) ( <" D E F "> ` 2 ) "> /\ <" ( <" A B C "> ` 0 ) ( <" A B C "> ` 1 ) ( <" A B C "> ` 2 ) "> ( cgrA ` G ) <" ( <" D E F "> ` 0 ) ( <" D E F "> ` 1 ) x "> ) <-> ( x ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E x "> ) ) )
83 82 rexbidv 
 |-  ( ph -> ( E. x e. P ( x ( inA ` G ) <" ( <" D E F "> ` 0 ) ( <" D E F "> ` 1 ) ( <" D E F "> ` 2 ) "> /\ <" ( <" A B C "> ` 0 ) ( <" A B C "> ` 1 ) ( <" A B C "> ` 2 ) "> ( cgrA ` G ) <" ( <" D E F "> ` 0 ) ( <" D E F "> ` 1 ) x "> ) <-> E. x e. P ( x ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E x "> ) ) )
84 83 anbi2d 
 |-  ( ph -> ( ( ( <" A B C "> e. ( P ^m ( 0 ..^ 3 ) ) /\ <" D E F "> e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P ( x ( inA ` G ) <" ( <" D E F "> ` 0 ) ( <" D E F "> ` 1 ) ( <" D E F "> ` 2 ) "> /\ <" ( <" A B C "> ` 0 ) ( <" A B C "> ` 1 ) ( <" A B C "> ` 2 ) "> ( cgrA ` G ) <" ( <" D E F "> ` 0 ) ( <" D E F "> ` 1 ) x "> ) ) <-> ( ( <" A B C "> e. ( P ^m ( 0 ..^ 3 ) ) /\ <" D E F "> e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P ( x ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E x "> ) ) ) )
85 44 63 84 3bitrd 
 |-  ( ph -> ( <" A B C "> ( leA ` G ) <" D E F "> <-> ( ( <" A B C "> e. ( P ^m ( 0 ..^ 3 ) ) /\ <" D E F "> e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P ( x ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E x "> ) ) ) )
86 21 85 mpbirand 
 |-  ( ph -> ( <" A B C "> ( leA ` G ) <" D E F "> <-> E. x e. P ( x ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E x "> ) ) )