Metamath Proof Explorer

Theorem ttglem

Description: Lemma for ttgbas and ttgvsca . (Contributed by Thierry Arnoux, 15-Apr-2019)

Ref Expression
Hypotheses ttgval.n 
|- G = ( toTG ` H )
ttglem.2 
|- E = Slot N
ttglem.3 
|- N e. NN
ttglem.4 
|- N < ; 1 6
Assertion ttglem 
|- ( E ` H ) = ( E ` G )

Proof

Step Hyp Ref Expression
1 ttgval.n 
 |-  G = ( toTG ` H )
2 ttglem.2 
 |-  E = Slot N
3 ttglem.3 
 |-  N e. NN
4 ttglem.4 
 |-  N < ; 1 6
5 2 3 ndxid 
 |-  E = Slot ( E ` ndx )
6 3 nnrei 
 |-  N e. RR
7 6 4 ltneii 
 |-  N =/= ; 1 6
8 2 3 ndxarg 
 |-  ( E ` ndx ) = N
9 itvndx 
 |-  ( Itv ` ndx ) = ; 1 6
10 8 9 neeq12i 
 |-  ( ( E ` ndx ) =/= ( Itv ` ndx ) <-> N =/= ; 1 6 )
11 7 10 mpbir 
 |-  ( E ` ndx ) =/= ( Itv ` ndx )
12 5 11 setsnid 
 |-  ( E ` H ) = ( E ` ( H sSet <. ( Itv ` ndx ) , ( x e. ( Base ` H ) , y e. ( Base ` H ) |-> { z e. ( Base ` H ) | E. k e. ( 0 [,] 1 ) ( z ( -g ` H ) x ) = ( k ( .s ` H ) ( y ( -g ` H ) x ) ) } ) >. ) )
13 1nn0 
 |-  1 e. NN0
14 6nn0 
 |-  6 e. NN0
15 7nn 
 |-  7 e. NN
16 6lt7 
 |-  6 < 7
17 13 14 15 16 declt 
 |-  ; 1 6 < ; 1 7
18 6nn 
 |-  6 e. NN
19 13 18 decnncl 
 |-  ; 1 6 e. NN
20 19 nnrei 
 |-  ; 1 6 e. RR
21 13 15 decnncl 
 |-  ; 1 7 e. NN
22 21 nnrei 
 |-  ; 1 7 e. RR
23 6 20 22 lttri 
 |-  ( ( N < ; 1 6 /\ ; 1 6 < ; 1 7 ) -> N < ; 1 7 )
24 4 17 23 mp2an 
 |-  N < ; 1 7
25 6 24 ltneii 
 |-  N =/= ; 1 7
26 lngndx 
 |-  ( LineG ` ndx ) = ; 1 7
27 8 26 neeq12i 
 |-  ( ( E ` ndx ) =/= ( LineG ` ndx ) <-> N =/= ; 1 7 )
28 25 27 mpbir 
 |-  ( E ` ndx ) =/= ( LineG ` ndx )
29 5 28 setsnid 
 |-  ( E ` ( H sSet <. ( Itv ` ndx ) , ( x e. ( Base ` H ) , y e. ( Base ` H ) |-> { z e. ( Base ` H ) | E. k e. ( 0 [,] 1 ) ( z ( -g ` H ) x ) = ( k ( .s ` H ) ( y ( -g ` H ) x ) ) } ) >. ) ) = ( E ` ( ( H sSet <. ( Itv ` ndx ) , ( x e. ( Base ` H ) , y e. ( Base ` H ) |-> { z e. ( Base ` H ) | E. k e. ( 0 [,] 1 ) ( z ( -g ` H ) x ) = ( k ( .s ` H ) ( y ( -g ` H ) x ) ) } ) >. ) sSet <. ( LineG ` ndx ) , ( x e. ( Base ` H ) , y e. ( Base ` H ) |-> { z e. ( Base ` H ) | ( z e. ( x ( Itv ` G ) y ) \/ x e. ( z ( Itv ` G ) y ) \/ y e. ( x ( Itv ` G ) z ) ) } ) >. ) )
30 12 29 eqtri 
 |-  ( E ` H ) = ( E ` ( ( H sSet <. ( Itv ` ndx ) , ( x e. ( Base ` H ) , y e. ( Base ` H ) |-> { z e. ( Base ` H ) | E. k e. ( 0 [,] 1 ) ( z ( -g ` H ) x ) = ( k ( .s ` H ) ( y ( -g ` H ) x ) ) } ) >. ) sSet <. ( LineG ` ndx ) , ( x e. ( Base ` H ) , y e. ( Base ` H ) |-> { z e. ( Base ` H ) | ( z e. ( x ( Itv ` G ) y ) \/ x e. ( z ( Itv ` G ) y ) \/ y e. ( x ( Itv ` G ) z ) ) } ) >. ) )
31 eqid 
 |-  ( Base ` H ) = ( Base ` H )
32 eqid 
 |-  ( -g ` H ) = ( -g ` H )
33 eqid 
 |-  ( .s ` H ) = ( .s ` H )
34 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
35 1 31 32 33 34 ttgval 
 |-  ( H e. _V -> ( G = ( ( H sSet <. ( Itv ` ndx ) , ( x e. ( Base ` H ) , y e. ( Base ` H ) |-> { z e. ( Base ` H ) | E. k e. ( 0 [,] 1 ) ( z ( -g ` H ) x ) = ( k ( .s ` H ) ( y ( -g ` H ) x ) ) } ) >. ) sSet <. ( LineG ` ndx ) , ( x e. ( Base ` H ) , y e. ( Base ` H ) |-> { z e. ( Base ` H ) | ( z e. ( x ( Itv ` G ) y ) \/ x e. ( z ( Itv ` G ) y ) \/ y e. ( x ( Itv ` G ) z ) ) } ) >. ) /\ ( Itv ` G ) = ( x e. ( Base ` H ) , y e. ( Base ` H ) |-> { z e. ( Base ` H ) | E. k e. ( 0 [,] 1 ) ( z ( -g ` H ) x ) = ( k ( .s ` H ) ( y ( -g ` H ) x ) ) } ) ) )
36 35 simpld 
 |-  ( H e. _V -> G = ( ( H sSet <. ( Itv ` ndx ) , ( x e. ( Base ` H ) , y e. ( Base ` H ) |-> { z e. ( Base ` H ) | E. k e. ( 0 [,] 1 ) ( z ( -g ` H ) x ) = ( k ( .s ` H ) ( y ( -g ` H ) x ) ) } ) >. ) sSet <. ( LineG ` ndx ) , ( x e. ( Base ` H ) , y e. ( Base ` H ) |-> { z e. ( Base ` H ) | ( z e. ( x ( Itv ` G ) y ) \/ x e. ( z ( Itv ` G ) y ) \/ y e. ( x ( Itv ` G ) z ) ) } ) >. ) )
37 36 fveq2d 
 |-  ( H e. _V -> ( E ` G ) = ( E ` ( ( H sSet <. ( Itv ` ndx ) , ( x e. ( Base ` H ) , y e. ( Base ` H ) |-> { z e. ( Base ` H ) | E. k e. ( 0 [,] 1 ) ( z ( -g ` H ) x ) = ( k ( .s ` H ) ( y ( -g ` H ) x ) ) } ) >. ) sSet <. ( LineG ` ndx ) , ( x e. ( Base ` H ) , y e. ( Base ` H ) |-> { z e. ( Base ` H ) | ( z e. ( x ( Itv ` G ) y ) \/ x e. ( z ( Itv ` G ) y ) \/ y e. ( x ( Itv ` G ) z ) ) } ) >. ) ) )
38 30 37 eqtr4id 
 |-  ( H e. _V -> ( E ` H ) = ( E ` G ) )
39 2 str0 
 |-  (/) = ( E ` (/) )
40 fvprc 
 |-  ( -. H e. _V -> ( E ` H ) = (/) )
41 fvprc 
 |-  ( -. H e. _V -> ( toTG ` H ) = (/) )
42 1 41 syl5eq 
 |-  ( -. H e. _V -> G = (/) )
43 42 fveq2d 
 |-  ( -. H e. _V -> ( E ` G ) = ( E ` (/) ) )
44 39 40 43 3eqtr4a 
 |-  ( -. H e. _V -> ( E ` H ) = ( E ` G ) )
45 38 44 pm2.61i 
 |-  ( E ` H ) = ( E ` G )