Metamath Proof Explorer

Theorem ishlg

Description: Rays : Definition 6.1 of Schwabhauser p. 43. With this definition, A ( KC ) B means that A and B are on the same ray with initial point C . This follows the same notation as Schwabhauser where rays are first defined as a relation. It is possible to recover the ray itself using e.g., ( ( KC ) " { A } ) . (Contributed by Thierry Arnoux, 21-Dec-2019)

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

Proof

Step Hyp Ref Expression
1 ishlg.p 
 |-  P = ( Base ` G )
2 ishlg.i 
 |-  I = ( Itv ` G )
3 ishlg.k 
 |-  K = ( hlG ` G )
4 ishlg.a 
 |-  ( ph -> A e. P )
5 ishlg.b 
 |-  ( ph -> B e. P )
6 ishlg.c 
 |-  ( ph -> C e. P )
7 ishlg.g 
 |-  ( ph -> G e. V )
8 simpl 
 |-  ( ( a = A /\ b = B ) -> a = A )
9 8 neeq1d 
 |-  ( ( a = A /\ b = B ) -> ( a =/= C <-> A =/= C ) )
10 simpr 
 |-  ( ( a = A /\ b = B ) -> b = B )
11 10 neeq1d 
 |-  ( ( a = A /\ b = B ) -> ( b =/= C <-> B =/= C ) )
12 10 oveq2d 
 |-  ( ( a = A /\ b = B ) -> ( C I b ) = ( C I B ) )
13 8 12 eleq12d 
 |-  ( ( a = A /\ b = B ) -> ( a e. ( C I b ) <-> A e. ( C I B ) ) )
14 8 oveq2d 
 |-  ( ( a = A /\ b = B ) -> ( C I a ) = ( C I A ) )
15 10 14 eleq12d 
 |-  ( ( a = A /\ b = B ) -> ( b e. ( C I a ) <-> B e. ( C I A ) ) )
16 13 15 orbi12d 
 |-  ( ( a = A /\ b = B ) -> ( ( a e. ( C I b ) \/ b e. ( C I a ) ) <-> ( A e. ( C I B ) \/ B e. ( C I A ) ) ) )
17 9 11 16 3anbi123d 
 |-  ( ( a = A /\ b = B ) -> ( ( a =/= C /\ b =/= C /\ ( a e. ( C I b ) \/ b e. ( C I a ) ) ) <-> ( A =/= C /\ B =/= C /\ ( A e. ( C I B ) \/ B e. ( C I A ) ) ) ) )
18 eqid 
 |-  { <. a , b >. | ( ( a e. P /\ b e. P ) /\ ( a =/= C /\ b =/= C /\ ( a e. ( C I b ) \/ b e. ( C I a ) ) ) ) } = { <. a , b >. | ( ( a e. P /\ b e. P ) /\ ( a =/= C /\ b =/= C /\ ( a e. ( C I b ) \/ b e. ( C I a ) ) ) ) }
19 17 18 brab2a 
 |-  ( A { <. a , b >. | ( ( a e. P /\ b e. P ) /\ ( a =/= C /\ b =/= C /\ ( a e. ( C I b ) \/ b e. ( C I a ) ) ) ) } B <-> ( ( A e. P /\ B e. P ) /\ ( A =/= C /\ B =/= C /\ ( A e. ( C I B ) \/ B e. ( C I A ) ) ) ) )
20 19 a1i 
 |-  ( ph -> ( A { <. a , b >. | ( ( a e. P /\ b e. P ) /\ ( a =/= C /\ b =/= C /\ ( a e. ( C I b ) \/ b e. ( C I a ) ) ) ) } B <-> ( ( A e. P /\ B e. P ) /\ ( A =/= C /\ B =/= C /\ ( A e. ( C I B ) \/ B e. ( C I A ) ) ) ) ) )
21 elex 
 |-  ( G e. V -> G e. _V )
22 fveq2 
 |-  ( g = G -> ( Base ` g ) = ( Base ` G ) )
23 22 1 eqtr4di 
 |-  ( g = G -> ( Base ` g ) = P )
24 23 eleq2d 
 |-  ( g = G -> ( a e. ( Base ` g ) <-> a e. P ) )
25 23 eleq2d 
 |-  ( g = G -> ( b e. ( Base ` g ) <-> b e. P ) )
26 24 25 anbi12d 
 |-  ( g = G -> ( ( a e. ( Base ` g ) /\ b e. ( Base ` g ) ) <-> ( a e. P /\ b e. P ) ) )
27 fveq2 
 |-  ( g = G -> ( Itv ` g ) = ( Itv ` G ) )
28 27 2 eqtr4di 
 |-  ( g = G -> ( Itv ` g ) = I )
29 28 oveqd 
 |-  ( g = G -> ( c ( Itv ` g ) b ) = ( c I b ) )
30 29 eleq2d 
 |-  ( g = G -> ( a e. ( c ( Itv ` g ) b ) <-> a e. ( c I b ) ) )
31 28 oveqd 
 |-  ( g = G -> ( c ( Itv ` g ) a ) = ( c I a ) )
32 31 eleq2d 
 |-  ( g = G -> ( b e. ( c ( Itv ` g ) a ) <-> b e. ( c I a ) ) )
33 30 32 orbi12d 
 |-  ( g = G -> ( ( a e. ( c ( Itv ` g ) b ) \/ b e. ( c ( Itv ` g ) a ) ) <-> ( a e. ( c I b ) \/ b e. ( c I a ) ) ) )
34 33 3anbi3d 
 |-  ( g = G -> ( ( a =/= c /\ b =/= c /\ ( a e. ( c ( Itv ` g ) b ) \/ b e. ( c ( Itv ` g ) a ) ) ) <-> ( a =/= c /\ b =/= c /\ ( a e. ( c I b ) \/ b e. ( c I a ) ) ) ) )
35 26 34 anbi12d 
 |-  ( g = G -> ( ( ( a e. ( Base ` g ) /\ b e. ( Base ` g ) ) /\ ( a =/= c /\ b =/= c /\ ( a e. ( c ( Itv ` g ) b ) \/ b e. ( c ( Itv ` g ) a ) ) ) ) <-> ( ( a e. P /\ b e. P ) /\ ( a =/= c /\ b =/= c /\ ( a e. ( c I b ) \/ b e. ( c I a ) ) ) ) ) )
36 35 opabbidv 
 |-  ( g = G -> { <. a , b >. | ( ( a e. ( Base ` g ) /\ b e. ( Base ` g ) ) /\ ( a =/= c /\ b =/= c /\ ( a e. ( c ( Itv ` g ) b ) \/ b e. ( c ( Itv ` g ) a ) ) ) ) } = { <. a , b >. | ( ( a e. P /\ b e. P ) /\ ( a =/= c /\ b =/= c /\ ( a e. ( c I b ) \/ b e. ( c I a ) ) ) ) } )
37 23 36 mpteq12dv 
 |-  ( g = G -> ( c e. ( Base ` g ) |-> { <. a , b >. | ( ( a e. ( Base ` g ) /\ b e. ( Base ` g ) ) /\ ( a =/= c /\ b =/= c /\ ( a e. ( c ( Itv ` g ) b ) \/ b e. ( c ( Itv ` g ) a ) ) ) ) } ) = ( c e. P |-> { <. a , b >. | ( ( a e. P /\ b e. P ) /\ ( a =/= c /\ b =/= c /\ ( a e. ( c I b ) \/ b e. ( c I a ) ) ) ) } ) )
38 df-hlg 
 |-  hlG = ( g e. _V |-> ( c e. ( Base ` g ) |-> { <. a , b >. | ( ( a e. ( Base ` g ) /\ b e. ( Base ` g ) ) /\ ( a =/= c /\ b =/= c /\ ( a e. ( c ( Itv ` g ) b ) \/ b e. ( c ( Itv ` g ) a ) ) ) ) } ) )
39 37 38 1 mptfvmpt 
 |-  ( G e. _V -> ( hlG ` G ) = ( c e. P |-> { <. a , b >. | ( ( a e. P /\ b e. P ) /\ ( a =/= c /\ b =/= c /\ ( a e. ( c I b ) \/ b e. ( c I a ) ) ) ) } ) )
40 7 21 39 3syl 
 |-  ( ph -> ( hlG ` G ) = ( c e. P |-> { <. a , b >. | ( ( a e. P /\ b e. P ) /\ ( a =/= c /\ b =/= c /\ ( a e. ( c I b ) \/ b e. ( c I a ) ) ) ) } ) )
41 3 40 syl5eq 
 |-  ( ph -> K = ( c e. P |-> { <. a , b >. | ( ( a e. P /\ b e. P ) /\ ( a =/= c /\ b =/= c /\ ( a e. ( c I b ) \/ b e. ( c I a ) ) ) ) } ) )
42 neeq2 
 |-  ( c = C -> ( a =/= c <-> a =/= C ) )
43 neeq2 
 |-  ( c = C -> ( b =/= c <-> b =/= C ) )
44 oveq1 
 |-  ( c = C -> ( c I b ) = ( C I b ) )
45 44 eleq2d 
 |-  ( c = C -> ( a e. ( c I b ) <-> a e. ( C I b ) ) )
46 oveq1 
 |-  ( c = C -> ( c I a ) = ( C I a ) )
47 46 eleq2d 
 |-  ( c = C -> ( b e. ( c I a ) <-> b e. ( C I a ) ) )
48 45 47 orbi12d 
 |-  ( c = C -> ( ( a e. ( c I b ) \/ b e. ( c I a ) ) <-> ( a e. ( C I b ) \/ b e. ( C I a ) ) ) )
49 42 43 48 3anbi123d 
 |-  ( c = C -> ( ( a =/= c /\ b =/= c /\ ( a e. ( c I b ) \/ b e. ( c I a ) ) ) <-> ( a =/= C /\ b =/= C /\ ( a e. ( C I b ) \/ b e. ( C I a ) ) ) ) )
50 49 anbi2d 
 |-  ( c = C -> ( ( ( a e. P /\ b e. P ) /\ ( a =/= c /\ b =/= c /\ ( a e. ( c I b ) \/ b e. ( c I a ) ) ) ) <-> ( ( a e. P /\ b e. P ) /\ ( a =/= C /\ b =/= C /\ ( a e. ( C I b ) \/ b e. ( C I a ) ) ) ) ) )
51 50 opabbidv 
 |-  ( c = C -> { <. a , b >. | ( ( a e. P /\ b e. P ) /\ ( a =/= c /\ b =/= c /\ ( a e. ( c I b ) \/ b e. ( c I a ) ) ) ) } = { <. a , b >. | ( ( a e. P /\ b e. P ) /\ ( a =/= C /\ b =/= C /\ ( a e. ( C I b ) \/ b e. ( C I a ) ) ) ) } )
52 51 adantl 
 |-  ( ( ph /\ c = C ) -> { <. a , b >. | ( ( a e. P /\ b e. P ) /\ ( a =/= c /\ b =/= c /\ ( a e. ( c I b ) \/ b e. ( c I a ) ) ) ) } = { <. a , b >. | ( ( a e. P /\ b e. P ) /\ ( a =/= C /\ b =/= C /\ ( a e. ( C I b ) \/ b e. ( C I a ) ) ) ) } )
53 1 fvexi 
 |-  P e. _V
54 53 53 xpex 
 |-  ( P X. P ) e. _V
55 opabssxp 
 |-  { <. a , b >. | ( ( a e. P /\ b e. P ) /\ ( a =/= C /\ b =/= C /\ ( a e. ( C I b ) \/ b e. ( C I a ) ) ) ) } C_ ( P X. P )
56 54 55 ssexi 
 |-  { <. a , b >. | ( ( a e. P /\ b e. P ) /\ ( a =/= C /\ b =/= C /\ ( a e. ( C I b ) \/ b e. ( C I a ) ) ) ) } e. _V
57 56 a1i 
 |-  ( ph -> { <. a , b >. | ( ( a e. P /\ b e. P ) /\ ( a =/= C /\ b =/= C /\ ( a e. ( C I b ) \/ b e. ( C I a ) ) ) ) } e. _V )
58 41 52 6 57 fvmptd 
 |-  ( ph -> ( K ` C ) = { <. a , b >. | ( ( a e. P /\ b e. P ) /\ ( a =/= C /\ b =/= C /\ ( a e. ( C I b ) \/ b e. ( C I a ) ) ) ) } )
59 58 breqd 
 |-  ( ph -> ( A ( K ` C ) B <-> A { <. a , b >. | ( ( a e. P /\ b e. P ) /\ ( a =/= C /\ b =/= C /\ ( a e. ( C I b ) \/ b e. ( C I a ) ) ) ) } B ) )
60 4 5 jca 
 |-  ( ph -> ( A e. P /\ B e. P ) )
61 60 biantrurd 
 |-  ( ph -> ( ( A =/= C /\ B =/= C /\ ( A e. ( C I B ) \/ B e. ( C I A ) ) ) <-> ( ( A e. P /\ B e. P ) /\ ( A =/= C /\ B =/= C /\ ( A e. ( C I B ) \/ B e. ( C I A ) ) ) ) ) )
62 20 59 61 3bitr4d 
 |-  ( ph -> ( A ( K ` C ) B <-> ( A =/= C /\ B =/= C /\ ( A e. ( C I B ) \/ B e. ( C I A ) ) ) ) )