Metamath Proof Explorer

Theorem ttgval

Description: Define a function to augment a subcomplex Hilbert space with betweenness and a line definition. (Contributed by Thierry Arnoux, 25-Mar-2019) (Proof shortened by AV, 9-Nov-2024)

Ref Expression
Hypotheses ttgval.n 
|- G = ( toTG ` H )
ttgval.b 
|- B = ( Base ` H )
ttgval.m 
|- .- = ( -g ` H )
ttgval.s 
|- .x. = ( .s ` H )
ttgval.i 
|- I = ( Itv ` G )
Assertion ttgval 
|- ( H e. V -> ( G = ( ( H sSet <. ( Itv ` ndx ) , ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) >. ) sSet <. ( LineG ` ndx ) , ( x e. B , y e. B |-> { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) >. ) /\ I = ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) ) )

Proof

Step Hyp Ref Expression
1 ttgval.n 
 |-  G = ( toTG ` H )
2 ttgval.b 
 |-  B = ( Base ` H )
3 ttgval.m 
 |-  .- = ( -g ` H )
4 ttgval.s 
 |-  .x. = ( .s ` H )
5 ttgval.i 
 |-  I = ( Itv ` G )
6 1 a1i 
 |-  ( H e. V -> G = ( toTG ` H ) )
7 elex 
 |-  ( H e. V -> H e. _V )
8 fveq2 
 |-  ( w = H -> ( Base ` w ) = ( Base ` H ) )
9 8 2 eqtr4di 
 |-  ( w = H -> ( Base ` w ) = B )
10 fveq2 
 |-  ( w = H -> ( -g ` w ) = ( -g ` H ) )
11 10 3 eqtr4di 
 |-  ( w = H -> ( -g ` w ) = .- )
12 11 oveqd 
 |-  ( w = H -> ( z ( -g ` w ) x ) = ( z .- x ) )
13 fveq2 
 |-  ( w = H -> ( .s ` w ) = ( .s ` H ) )
14 13 4 eqtr4di 
 |-  ( w = H -> ( .s ` w ) = .x. )
15 eqidd 
 |-  ( w = H -> k = k )
16 11 oveqd 
 |-  ( w = H -> ( y ( -g ` w ) x ) = ( y .- x ) )
17 14 15 16 oveq123d 
 |-  ( w = H -> ( k ( .s ` w ) ( y ( -g ` w ) x ) ) = ( k .x. ( y .- x ) ) )
18 12 17 eqeq12d 
 |-  ( w = H -> ( ( z ( -g ` w ) x ) = ( k ( .s ` w ) ( y ( -g ` w ) x ) ) <-> ( z .- x ) = ( k .x. ( y .- x ) ) ) )
19 18 rexbidv 
 |-  ( w = H -> ( E. k e. ( 0 [,] 1 ) ( z ( -g ` w ) x ) = ( k ( .s ` w ) ( y ( -g ` w ) x ) ) <-> E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) ) )
20 9 19 rabeqbidv 
 |-  ( w = H -> { z e. ( Base ` w ) | E. k e. ( 0 [,] 1 ) ( z ( -g ` w ) x ) = ( k ( .s ` w ) ( y ( -g ` w ) x ) ) } = { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } )
21 9 9 20 mpoeq123dv 
 |-  ( w = H -> ( x e. ( Base ` w ) , y e. ( Base ` w ) |-> { z e. ( Base ` w ) | E. k e. ( 0 [,] 1 ) ( z ( -g ` w ) x ) = ( k ( .s ` w ) ( y ( -g ` w ) x ) ) } ) = ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) )
22 oveq1 
 |-  ( w = H -> ( w sSet <. ( Itv ` ndx ) , i >. ) = ( H sSet <. ( Itv ` ndx ) , i >. ) )
23 9 rabeqdv 
 |-  ( w = H -> { z e. ( Base ` w ) | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } = { z e. B | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } )
24 9 9 23 mpoeq123dv 
 |-  ( w = H -> ( x e. ( Base ` w ) , y e. ( Base ` w ) |-> { z e. ( Base ` w ) | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) = ( x e. B , y e. B |-> { z e. B | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) )
25 24 opeq2d 
 |-  ( w = H -> <. ( LineG ` ndx ) , ( x e. ( Base ` w ) , y e. ( Base ` w ) |-> { z e. ( Base ` w ) | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) >. = <. ( LineG ` ndx ) , ( x e. B , y e. B |-> { z e. B | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) >. )
26 22 25 oveq12d 
 |-  ( w = H -> ( ( w sSet <. ( Itv ` ndx ) , i >. ) sSet <. ( LineG ` ndx ) , ( x e. ( Base ` w ) , y e. ( Base ` w ) |-> { z e. ( Base ` w ) | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) >. ) = ( ( H sSet <. ( Itv ` ndx ) , i >. ) sSet <. ( LineG ` ndx ) , ( x e. B , y e. B |-> { z e. B | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) >. ) )
27 21 26 csbeq12dv 
 |-  ( w = H -> [_ ( x e. ( Base ` w ) , y e. ( Base ` w ) |-> { z e. ( Base ` w ) | E. k e. ( 0 [,] 1 ) ( z ( -g ` w ) x ) = ( k ( .s ` w ) ( y ( -g ` w ) x ) ) } ) / i ]_ ( ( w sSet <. ( Itv ` ndx ) , i >. ) sSet <. ( LineG ` ndx ) , ( x e. ( Base ` w ) , y e. ( Base ` w ) |-> { z e. ( Base ` w ) | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) >. ) = [_ ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) / i ]_ ( ( H sSet <. ( Itv ` ndx ) , i >. ) sSet <. ( LineG ` ndx ) , ( x e. B , y e. B |-> { z e. B | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) >. ) )
28 df-ttg 
 |-  toTG = ( w e. _V |-> [_ ( x e. ( Base ` w ) , y e. ( Base ` w ) |-> { z e. ( Base ` w ) | E. k e. ( 0 [,] 1 ) ( z ( -g ` w ) x ) = ( k ( .s ` w ) ( y ( -g ` w ) x ) ) } ) / i ]_ ( ( w sSet <. ( Itv ` ndx ) , i >. ) sSet <. ( LineG ` ndx ) , ( x e. ( Base ` w ) , y e. ( Base ` w ) |-> { z e. ( Base ` w ) | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) >. ) )
29 ovex 
 |-  ( ( H sSet <. ( Itv ` ndx ) , i >. ) sSet <. ( LineG ` ndx ) , ( x e. B , y e. B |-> { z e. B | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) >. ) e. _V
30 29 csbex 
 |-  [_ ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) / i ]_ ( ( H sSet <. ( Itv ` ndx ) , i >. ) sSet <. ( LineG ` ndx ) , ( x e. B , y e. B |-> { z e. B | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) >. ) e. _V
31 27 28 30 fvmpt 
 |-  ( H e. _V -> ( toTG ` H ) = [_ ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) / i ]_ ( ( H sSet <. ( Itv ` ndx ) , i >. ) sSet <. ( LineG ` ndx ) , ( x e. B , y e. B |-> { z e. B | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) >. ) )
32 7 31 syl 
 |-  ( H e. V -> ( toTG ` H ) = [_ ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) / i ]_ ( ( H sSet <. ( Itv ` ndx ) , i >. ) sSet <. ( LineG ` ndx ) , ( x e. B , y e. B |-> { z e. B | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) >. ) )
33 2 fvexi 
 |-  B e. _V
34 33 33 mpoex 
 |-  ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) e. _V
35 34 a1i 
 |-  ( H e. V -> ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) e. _V )
36 simpr 
 |-  ( ( H e. V /\ i = ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) ) -> i = ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) )
37 oveq2 
 |-  ( a = x -> ( c .- a ) = ( c .- x ) )
38 oveq2 
 |-  ( a = x -> ( b .- a ) = ( b .- x ) )
39 38 oveq2d 
 |-  ( a = x -> ( k .x. ( b .- a ) ) = ( k .x. ( b .- x ) ) )
40 37 39 eqeq12d 
 |-  ( a = x -> ( ( c .- a ) = ( k .x. ( b .- a ) ) <-> ( c .- x ) = ( k .x. ( b .- x ) ) ) )
41 40 rexbidv 
 |-  ( a = x -> ( E. k e. ( 0 [,] 1 ) ( c .- a ) = ( k .x. ( b .- a ) ) <-> E. k e. ( 0 [,] 1 ) ( c .- x ) = ( k .x. ( b .- x ) ) ) )
42 41 rabbidv 
 |-  ( a = x -> { c e. B | E. k e. ( 0 [,] 1 ) ( c .- a ) = ( k .x. ( b .- a ) ) } = { c e. B | E. k e. ( 0 [,] 1 ) ( c .- x ) = ( k .x. ( b .- x ) ) } )
43 oveq1 
 |-  ( b = y -> ( b .- x ) = ( y .- x ) )
44 43 oveq2d 
 |-  ( b = y -> ( k .x. ( b .- x ) ) = ( k .x. ( y .- x ) ) )
45 44 eqeq2d 
 |-  ( b = y -> ( ( c .- x ) = ( k .x. ( b .- x ) ) <-> ( c .- x ) = ( k .x. ( y .- x ) ) ) )
46 45 rexbidv 
 |-  ( b = y -> ( E. k e. ( 0 [,] 1 ) ( c .- x ) = ( k .x. ( b .- x ) ) <-> E. k e. ( 0 [,] 1 ) ( c .- x ) = ( k .x. ( y .- x ) ) ) )
47 46 rabbidv 
 |-  ( b = y -> { c e. B | E. k e. ( 0 [,] 1 ) ( c .- x ) = ( k .x. ( b .- x ) ) } = { c e. B | E. k e. ( 0 [,] 1 ) ( c .- x ) = ( k .x. ( y .- x ) ) } )
48 oveq1 
 |-  ( c = z -> ( c .- x ) = ( z .- x ) )
49 48 eqeq1d 
 |-  ( c = z -> ( ( c .- x ) = ( k .x. ( y .- x ) ) <-> ( z .- x ) = ( k .x. ( y .- x ) ) ) )
50 49 rexbidv 
 |-  ( c = z -> ( E. k e. ( 0 [,] 1 ) ( c .- x ) = ( k .x. ( y .- x ) ) <-> E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) ) )
51 50 cbvrabv 
 |-  { c e. B | E. k e. ( 0 [,] 1 ) ( c .- x ) = ( k .x. ( y .- x ) ) } = { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) }
52 47 51 eqtrdi 
 |-  ( b = y -> { c e. B | E. k e. ( 0 [,] 1 ) ( c .- x ) = ( k .x. ( b .- x ) ) } = { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } )
53 42 52 cbvmpov 
 |-  ( a e. B , b e. B |-> { c e. B | E. k e. ( 0 [,] 1 ) ( c .- a ) = ( k .x. ( b .- a ) ) } ) = ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } )
54 36 53 eqtr4di 
 |-  ( ( H e. V /\ i = ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) ) -> i = ( a e. B , b e. B |-> { c e. B | E. k e. ( 0 [,] 1 ) ( c .- a ) = ( k .x. ( b .- a ) ) } ) )
55 simpr 
 |-  ( ( H e. V /\ i = ( a e. B , b e. B |-> { c e. B | E. k e. ( 0 [,] 1 ) ( c .- a ) = ( k .x. ( b .- a ) ) } ) ) -> i = ( a e. B , b e. B |-> { c e. B | E. k e. ( 0 [,] 1 ) ( c .- a ) = ( k .x. ( b .- a ) ) } ) )
56 55 53 eqtrdi 
 |-  ( ( H e. V /\ i = ( a e. B , b e. B |-> { c e. B | E. k e. ( 0 [,] 1 ) ( c .- a ) = ( k .x. ( b .- a ) ) } ) ) -> i = ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) )
57 56 opeq2d 
 |-  ( ( H e. V /\ i = ( a e. B , b e. B |-> { c e. B | E. k e. ( 0 [,] 1 ) ( c .- a ) = ( k .x. ( b .- a ) ) } ) ) -> <. ( Itv ` ndx ) , i >. = <. ( Itv ` ndx ) , ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) >. )
58 57 oveq2d 
 |-  ( ( H e. V /\ i = ( a e. B , b e. B |-> { c e. B | E. k e. ( 0 [,] 1 ) ( c .- a ) = ( k .x. ( b .- a ) ) } ) ) -> ( H sSet <. ( Itv ` ndx ) , i >. ) = ( H sSet <. ( Itv ` ndx ) , ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) >. ) )
59 56 oveqd 
 |-  ( ( H e. V /\ i = ( a e. B , b e. B |-> { c e. B | E. k e. ( 0 [,] 1 ) ( c .- a ) = ( k .x. ( b .- a ) ) } ) ) -> ( x i y ) = ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) )
60 59 eleq2d 
 |-  ( ( H e. V /\ i = ( a e. B , b e. B |-> { c e. B | E. k e. ( 0 [,] 1 ) ( c .- a ) = ( k .x. ( b .- a ) ) } ) ) -> ( z e. ( x i y ) <-> z e. ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) ) )
61 56 oveqd 
 |-  ( ( H e. V /\ i = ( a e. B , b e. B |-> { c e. B | E. k e. ( 0 [,] 1 ) ( c .- a ) = ( k .x. ( b .- a ) ) } ) ) -> ( z i y ) = ( z ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) )
62 61 eleq2d 
 |-  ( ( H e. V /\ i = ( a e. B , b e. B |-> { c e. B | E. k e. ( 0 [,] 1 ) ( c .- a ) = ( k .x. ( b .- a ) ) } ) ) -> ( x e. ( z i y ) <-> x e. ( z ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) ) )
63 56 oveqd 
 |-  ( ( H e. V /\ i = ( a e. B , b e. B |-> { c e. B | E. k e. ( 0 [,] 1 ) ( c .- a ) = ( k .x. ( b .- a ) ) } ) ) -> ( x i z ) = ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) z ) )
64 63 eleq2d 
 |-  ( ( H e. V /\ i = ( a e. B , b e. B |-> { c e. B | E. k e. ( 0 [,] 1 ) ( c .- a ) = ( k .x. ( b .- a ) ) } ) ) -> ( y e. ( x i z ) <-> y e. ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) z ) ) )
65 60 62 64 3orbi123d 
 |-  ( ( H e. V /\ i = ( a e. B , b e. B |-> { c e. B | E. k e. ( 0 [,] 1 ) ( c .- a ) = ( k .x. ( b .- a ) ) } ) ) -> ( ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) <-> ( z e. ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) \/ x e. ( z ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) \/ y e. ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) z ) ) ) )
66 65 rabbidv 
 |-  ( ( H e. V /\ i = ( a e. B , b e. B |-> { c e. B | E. k e. ( 0 [,] 1 ) ( c .- a ) = ( k .x. ( b .- a ) ) } ) ) -> { z e. B | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } = { z e. B | ( z e. ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) \/ x e. ( z ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) \/ y e. ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) z ) ) } )
67 66 mpoeq3dv 
 |-  ( ( H e. V /\ i = ( a e. B , b e. B |-> { c e. B | E. k e. ( 0 [,] 1 ) ( c .- a ) = ( k .x. ( b .- a ) ) } ) ) -> ( x e. B , y e. B |-> { z e. B | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) = ( x e. B , y e. B |-> { z e. B | ( z e. ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) \/ x e. ( z ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) \/ y e. ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) z ) ) } ) )
68 67 opeq2d 
 |-  ( ( H e. V /\ i = ( a e. B , b e. B |-> { c e. B | E. k e. ( 0 [,] 1 ) ( c .- a ) = ( k .x. ( b .- a ) ) } ) ) -> <. ( LineG ` ndx ) , ( x e. B , y e. B |-> { z e. B | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) >. = <. ( LineG ` ndx ) , ( x e. B , y e. B |-> { z e. B | ( z e. ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) \/ x e. ( z ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) \/ y e. ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) z ) ) } ) >. )
69 58 68 oveq12d 
 |-  ( ( H e. V /\ i = ( a e. B , b e. B |-> { c e. B | E. k e. ( 0 [,] 1 ) ( c .- a ) = ( k .x. ( b .- a ) ) } ) ) -> ( ( H sSet <. ( Itv ` ndx ) , i >. ) sSet <. ( LineG ` ndx ) , ( x e. B , y e. B |-> { z e. B | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) >. ) = ( ( H sSet <. ( Itv ` ndx ) , ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) >. ) sSet <. ( LineG ` ndx ) , ( x e. B , y e. B |-> { z e. B | ( z e. ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) \/ x e. ( z ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) \/ y e. ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) z ) ) } ) >. ) )
70 54 69 syldan 
 |-  ( ( H e. V /\ i = ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) ) -> ( ( H sSet <. ( Itv ` ndx ) , i >. ) sSet <. ( LineG ` ndx ) , ( x e. B , y e. B |-> { z e. B | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) >. ) = ( ( H sSet <. ( Itv ` ndx ) , ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) >. ) sSet <. ( LineG ` ndx ) , ( x e. B , y e. B |-> { z e. B | ( z e. ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) \/ x e. ( z ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) \/ y e. ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) z ) ) } ) >. ) )
71 35 70 csbied 
 |-  ( H e. V -> [_ ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) / i ]_ ( ( H sSet <. ( Itv ` ndx ) , i >. ) sSet <. ( LineG ` ndx ) , ( x e. B , y e. B |-> { z e. B | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) >. ) = ( ( H sSet <. ( Itv ` ndx ) , ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) >. ) sSet <. ( LineG ` ndx ) , ( x e. B , y e. B |-> { z e. B | ( z e. ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) \/ x e. ( z ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) \/ y e. ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) z ) ) } ) >. ) )
72 6 32 71 3eqtrd 
 |-  ( H e. V -> G = ( ( H sSet <. ( Itv ` ndx ) , ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) >. ) sSet <. ( LineG ` ndx ) , ( x e. B , y e. B |-> { z e. B | ( z e. ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) \/ x e. ( z ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) \/ y e. ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) z ) ) } ) >. ) )
73 72 fveq2d 
 |-  ( H e. V -> ( Itv ` G ) = ( Itv ` ( ( H sSet <. ( Itv ` ndx ) , ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) >. ) sSet <. ( LineG ` ndx ) , ( x e. B , y e. B |-> { z e. B | ( z e. ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) \/ x e. ( z ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) \/ y e. ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) z ) ) } ) >. ) ) )
74 itvid 
 |-  Itv = Slot ( Itv ` ndx )
75 lngndxnitvndx 
 |-  ( LineG ` ndx ) =/= ( Itv ` ndx )
76 75 necomi 
 |-  ( Itv ` ndx ) =/= ( LineG ` ndx )
77 74 76 setsnid 
 |-  ( Itv ` ( H sSet <. ( Itv ` ndx ) , ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) >. ) ) = ( Itv ` ( ( H sSet <. ( Itv ` ndx ) , ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) >. ) sSet <. ( LineG ` ndx ) , ( x e. B , y e. B |-> { z e. B | ( z e. ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) \/ x e. ( z ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) \/ y e. ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) z ) ) } ) >. ) )
78 73 77 eqtr4di 
 |-  ( H e. V -> ( Itv ` G ) = ( Itv ` ( H sSet <. ( Itv ` ndx ) , ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) >. ) ) )
79 5 a1i 
 |-  ( H e. V -> I = ( Itv ` G ) )
80 74 setsid 
 |-  ( ( H e. V /\ ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) e. _V ) -> ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) = ( Itv ` ( H sSet <. ( Itv ` ndx ) , ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) >. ) ) )
81 34 80 mpan2 
 |-  ( H e. V -> ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) = ( Itv ` ( H sSet <. ( Itv ` ndx ) , ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) >. ) ) )
82 78 79 81 3eqtr4d 
 |-  ( H e. V -> I = ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) )
83 82 oveqd 
 |-  ( H e. V -> ( x I y ) = ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) )
84 83 eleq2d 
 |-  ( H e. V -> ( z e. ( x I y ) <-> z e. ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) ) )
85 82 oveqd 
 |-  ( H e. V -> ( z I y ) = ( z ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) )
86 85 eleq2d 
 |-  ( H e. V -> ( x e. ( z I y ) <-> x e. ( z ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) ) )
87 82 oveqd 
 |-  ( H e. V -> ( x I z ) = ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) z ) )
88 87 eleq2d 
 |-  ( H e. V -> ( y e. ( x I z ) <-> y e. ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) z ) ) )
89 84 86 88 3orbi123d 
 |-  ( H e. V -> ( ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) <-> ( z e. ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) \/ x e. ( z ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) \/ y e. ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) z ) ) ) )
90 89 rabbidv 
 |-  ( H e. V -> { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } = { z e. B | ( z e. ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) \/ x e. ( z ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) \/ y e. ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) z ) ) } )
91 90 mpoeq3dv 
 |-  ( H e. V -> ( x e. B , y e. B |-> { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) = ( x e. B , y e. B |-> { z e. B | ( z e. ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) \/ x e. ( z ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) \/ y e. ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) z ) ) } ) )
92 91 opeq2d 
 |-  ( H e. V -> <. ( LineG ` ndx ) , ( x e. B , y e. B |-> { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) >. = <. ( LineG ` ndx ) , ( x e. B , y e. B |-> { z e. B | ( z e. ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) \/ x e. ( z ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) \/ y e. ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) z ) ) } ) >. )
93 92 oveq2d 
 |-  ( H e. V -> ( ( H sSet <. ( Itv ` ndx ) , ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) >. ) sSet <. ( LineG ` ndx ) , ( x e. B , y e. B |-> { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) >. ) = ( ( H sSet <. ( Itv ` ndx ) , ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) >. ) sSet <. ( LineG ` ndx ) , ( x e. B , y e. B |-> { z e. B | ( z e. ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) \/ x e. ( z ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) y ) \/ y e. ( x ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) z ) ) } ) >. ) )
94 72 93 eqtr4d 
 |-  ( H e. V -> G = ( ( H sSet <. ( Itv ` ndx ) , ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) >. ) sSet <. ( LineG ` ndx ) , ( x e. B , y e. B |-> { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) >. ) )
95 94 82 jca 
 |-  ( H e. V -> ( G = ( ( H sSet <. ( Itv ` ndx ) , ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) >. ) sSet <. ( LineG ` ndx ) , ( x e. B , y e. B |-> { z e. B | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) >. ) /\ I = ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) ) )