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)

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 21 csbeq1d 
 |-  ( 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 ]_ ( ( 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 ) ) } ) >. ) )
23 oveq1 
 |-  ( w = H -> ( w sSet <. ( Itv ` ndx ) , i >. ) = ( H sSet <. ( Itv ` ndx ) , i >. ) )
24 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 ) ) } )
25 9 9 24 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 ) ) } ) )
26 25 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 ) ) } ) >. )
27 23 26 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 ) ) } ) >. ) )
28 27 csbeq2dv 
 |-  ( w = H -> [_ ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- 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 ) ) } ) >. ) )
29 22 28 eqtrd 
 |-  ( 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 ) ) } ) >. ) )
30 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 ) ) } ) >. ) )
31 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
32 31 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
33 29 30 32 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 ) ) } ) >. ) )
34 7 33 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 ) ) } ) >. ) )
35 2 fvexi 
 |-  B e. _V
36 35 35 mpoex 
 |-  ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) e. _V
37 36 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 )
38 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 ) ) } ) )
39 oveq2 
 |-  ( a = x -> ( c .- a ) = ( c .- x ) )
40 oveq2 
 |-  ( a = x -> ( b .- a ) = ( b .- x ) )
41 40 oveq2d 
 |-  ( a = x -> ( k .x. ( b .- a ) ) = ( k .x. ( b .- x ) ) )
42 39 41 eqeq12d 
 |-  ( a = x -> ( ( c .- a ) = ( k .x. ( b .- a ) ) <-> ( c .- x ) = ( k .x. ( b .- x ) ) ) )
43 42 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 ) ) ) )
44 43 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 ) ) } )
45 oveq1 
 |-  ( b = y -> ( b .- x ) = ( y .- x ) )
46 45 oveq2d 
 |-  ( b = y -> ( k .x. ( b .- x ) ) = ( k .x. ( y .- x ) ) )
47 46 eqeq2d 
 |-  ( b = y -> ( ( c .- x ) = ( k .x. ( b .- x ) ) <-> ( c .- x ) = ( k .x. ( y .- x ) ) ) )
48 47 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 ) ) ) )
49 48 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 ) ) } )
50 oveq1 
 |-  ( c = z -> ( c .- x ) = ( z .- x ) )
51 50 eqeq1d 
 |-  ( c = z -> ( ( c .- x ) = ( k .x. ( y .- x ) ) <-> ( z .- x ) = ( k .x. ( y .- x ) ) ) )
52 51 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 ) ) ) )
53 52 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 ) ) }
54 49 53 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 ) ) } )
55 44 54 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 ) ) } )
56 38 55 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 ) ) } ) )
57 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 ) ) } ) )
58 57 55 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 ) ) } ) )
59 58 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 ) ) } ) >. )
60 59 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 ) ) } ) >. ) )
61 58 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 ) )
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 ) ) } ) ) -> ( 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 ) ) )
63 58 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 ) )
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 ) ) } ) ) -> ( 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 ) ) )
65 58 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 ) )
66 65 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 ) ) )
67 62 64 66 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 ) ) ) )
68 67 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 ) ) } )
69 68 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 ) ) } ) )
70 69 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 ) ) } ) >. )
71 60 70 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 ) ) } ) >. ) )
72 56 71 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 ) ) } ) >. ) )
73 37 72 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 ) ) } ) >. ) )
74 6 34 73 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 ) ) } ) >. ) )
75 74 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 ) ) } ) >. ) ) )
76 itvid 
 |-  Itv = Slot ( Itv ` ndx )
77 1nn0 
 |-  1 e. NN0
78 6nn 
 |-  6 e. NN
79 77 78 decnncl 
 |-  ; 1 6 e. NN
80 79 nnrei 
 |-  ; 1 6 e. RR
81 6nn0 
 |-  6 e. NN0
82 7nn 
 |-  7 e. NN
83 6lt7 
 |-  6 < 7
84 77 81 82 83 declt 
 |-  ; 1 6 < ; 1 7
85 80 84 ltneii 
 |-  ; 1 6 =/= ; 1 7
86 itvndx 
 |-  ( Itv ` ndx ) = ; 1 6
87 lngndx 
 |-  ( LineG ` ndx ) = ; 1 7
88 86 87 neeq12i 
 |-  ( ( Itv ` ndx ) =/= ( LineG ` ndx ) <-> ; 1 6 =/= ; 1 7 )
89 85 88 mpbir 
 |-  ( Itv ` ndx ) =/= ( LineG ` ndx )
90 76 89 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 ) ) } ) >. ) )
91 75 90 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 ) ) } ) >. ) ) )
92 5 a1i 
 |-  ( H e. V -> I = ( Itv ` G ) )
93 76 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 ) ) } ) >. ) ) )
94 36 93 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 ) ) } ) >. ) ) )
95 91 92 94 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 ) ) } ) )
96 95 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 ) )
97 96 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 ) ) )
98 95 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 ) )
99 98 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 ) ) )
100 95 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 ) )
101 100 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 ) ) )
102 97 99 101 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 ) ) ) )
103 102 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 ) ) } )
104 103 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 ) ) } ) )
105 104 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 ) ) } ) >. )
106 105 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 ) ) } ) >. ) )
107 74 106 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 ) ) } ) >. ) )
108 107 95 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 ) ) } ) ) )