Metamath Proof Explorer

Theorem ttglem

Description: Lemma for ttgbas , ttgvsca etc. (Contributed by Thierry Arnoux, 15-Apr-2019) (Revised by AV, 29-Oct-2024)

Ref Expression
Hypotheses ttgval.n 
|- G = ( toTG ` H )
ttglem.e 
|- E = Slot ( E ` ndx )
ttglem.l 
|- ( E ` ndx ) =/= ( LineG ` ndx )
ttglem.i 
|- ( E ` ndx ) =/= ( Itv ` ndx )
Assertion ttglem 
|- ( E ` H ) = ( E ` G )

Proof

Step Hyp Ref Expression
1 ttgval.n 
 |-  G = ( toTG ` H )
2 ttglem.e 
 |-  E = Slot ( E ` ndx )
3 ttglem.l 
 |-  ( E ` ndx ) =/= ( LineG ` ndx )
4 ttglem.i 
 |-  ( E ` ndx ) =/= ( Itv ` ndx )
5 2 4 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 ) ) } ) >. ) )
6 2 3 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 ) ) } ) >. ) )
7 5 6 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 ) ) } ) >. ) )
8 eqid 
 |-  ( Base ` H ) = ( Base ` H )
9 eqid 
 |-  ( -g ` H ) = ( -g ` H )
10 eqid 
 |-  ( .s ` H ) = ( .s ` H )
11 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
12 1 8 9 10 11 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 ) ) } ) ) )
13 12 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 ) ) } ) >. ) )
14 13 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 ) ) } ) >. ) ) )
15 7 14 eqtr4id 
 |-  ( H e. _V -> ( E ` H ) = ( E ` G ) )
16 2 str0 
 |-  (/) = ( E ` (/) )
17 16 eqcomi 
 |-  ( E ` (/) ) = (/)
18 17 1 fveqprc 
 |-  ( -. H e. _V -> ( E ` H ) = ( E ` G ) )
19 15 18 pm2.61i 
 |-  ( E ` H ) = ( E ` G )