Metamath Proof Explorer


Theorem ttgitvval

Description: Betweenness for a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019)

Ref Expression
Hypotheses ttgval.n โŠข ๐บ = ( toTG โ€˜ ๐ป )
ttgitvval.i โŠข ๐ผ = ( Itv โ€˜ ๐บ )
ttgitvval.b โŠข ๐‘ƒ = ( Base โ€˜ ๐ป )
ttgitvval.m โŠข โˆ’ = ( -g โ€˜ ๐ป )
ttgitvval.s โŠข ยท = ( ยท๐‘  โ€˜ ๐ป )
Assertion ttgitvval ( ( ๐ป โˆˆ ๐‘‰ โˆง ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ ) โ†’ ( ๐‘‹ ๐ผ ๐‘Œ ) = { ๐‘ง โˆˆ ๐‘ƒ โˆฃ โˆƒ ๐‘˜ โˆˆ ( 0 [,] 1 ) ( ๐‘ง โˆ’ ๐‘‹ ) = ( ๐‘˜ ยท ( ๐‘Œ โˆ’ ๐‘‹ ) ) } )

Proof

Step Hyp Ref Expression
1 ttgval.n โŠข ๐บ = ( toTG โ€˜ ๐ป )
2 ttgitvval.i โŠข ๐ผ = ( Itv โ€˜ ๐บ )
3 ttgitvval.b โŠข ๐‘ƒ = ( Base โ€˜ ๐ป )
4 ttgitvval.m โŠข โˆ’ = ( -g โ€˜ ๐ป )
5 ttgitvval.s โŠข ยท = ( ยท๐‘  โ€˜ ๐ป )
6 1 3 4 5 2 ttgval โŠข ( ๐ป โˆˆ ๐‘‰ โ†’ ( ๐บ = ( ( ๐ป sSet โŸจ ( Itv โ€˜ ndx ) , ( ๐‘ฅ โˆˆ ๐‘ƒ , ๐‘ฆ โˆˆ ๐‘ƒ โ†ฆ { ๐‘ง โˆˆ ๐‘ƒ โˆฃ โˆƒ ๐‘˜ โˆˆ ( 0 [,] 1 ) ( ๐‘ง โˆ’ ๐‘ฅ ) = ( ๐‘˜ ยท ( ๐‘ฆ โˆ’ ๐‘ฅ ) ) } ) โŸฉ ) sSet โŸจ ( LineG โ€˜ ndx ) , ( ๐‘ฅ โˆˆ ๐‘ƒ , ๐‘ฆ โˆˆ ๐‘ƒ โ†ฆ { ๐‘ง โˆˆ ๐‘ƒ โˆฃ ( ๐‘ง โˆˆ ( ๐‘ฅ ๐ผ ๐‘ฆ ) โˆจ ๐‘ฅ โˆˆ ( ๐‘ง ๐ผ ๐‘ฆ ) โˆจ ๐‘ฆ โˆˆ ( ๐‘ฅ ๐ผ ๐‘ง ) ) } ) โŸฉ ) โˆง ๐ผ = ( ๐‘ฅ โˆˆ ๐‘ƒ , ๐‘ฆ โˆˆ ๐‘ƒ โ†ฆ { ๐‘ง โˆˆ ๐‘ƒ โˆฃ โˆƒ ๐‘˜ โˆˆ ( 0 [,] 1 ) ( ๐‘ง โˆ’ ๐‘ฅ ) = ( ๐‘˜ ยท ( ๐‘ฆ โˆ’ ๐‘ฅ ) ) } ) ) )
7 6 simprd โŠข ( ๐ป โˆˆ ๐‘‰ โ†’ ๐ผ = ( ๐‘ฅ โˆˆ ๐‘ƒ , ๐‘ฆ โˆˆ ๐‘ƒ โ†ฆ { ๐‘ง โˆˆ ๐‘ƒ โˆฃ โˆƒ ๐‘˜ โˆˆ ( 0 [,] 1 ) ( ๐‘ง โˆ’ ๐‘ฅ ) = ( ๐‘˜ ยท ( ๐‘ฆ โˆ’ ๐‘ฅ ) ) } ) )
8 7 3ad2ant1 โŠข ( ( ๐ป โˆˆ ๐‘‰ โˆง ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ ) โ†’ ๐ผ = ( ๐‘ฅ โˆˆ ๐‘ƒ , ๐‘ฆ โˆˆ ๐‘ƒ โ†ฆ { ๐‘ง โˆˆ ๐‘ƒ โˆฃ โˆƒ ๐‘˜ โˆˆ ( 0 [,] 1 ) ( ๐‘ง โˆ’ ๐‘ฅ ) = ( ๐‘˜ ยท ( ๐‘ฆ โˆ’ ๐‘ฅ ) ) } ) )
9 simprl โŠข ( ( ( ๐ป โˆˆ ๐‘‰ โˆง ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ ) โˆง ( ๐‘ฅ = ๐‘‹ โˆง ๐‘ฆ = ๐‘Œ ) ) โ†’ ๐‘ฅ = ๐‘‹ )
10 9 oveq2d โŠข ( ( ( ๐ป โˆˆ ๐‘‰ โˆง ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ ) โˆง ( ๐‘ฅ = ๐‘‹ โˆง ๐‘ฆ = ๐‘Œ ) ) โ†’ ( ๐‘ง โˆ’ ๐‘ฅ ) = ( ๐‘ง โˆ’ ๐‘‹ ) )
11 simprr โŠข ( ( ( ๐ป โˆˆ ๐‘‰ โˆง ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ ) โˆง ( ๐‘ฅ = ๐‘‹ โˆง ๐‘ฆ = ๐‘Œ ) ) โ†’ ๐‘ฆ = ๐‘Œ )
12 11 9 oveq12d โŠข ( ( ( ๐ป โˆˆ ๐‘‰ โˆง ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ ) โˆง ( ๐‘ฅ = ๐‘‹ โˆง ๐‘ฆ = ๐‘Œ ) ) โ†’ ( ๐‘ฆ โˆ’ ๐‘ฅ ) = ( ๐‘Œ โˆ’ ๐‘‹ ) )
13 12 oveq2d โŠข ( ( ( ๐ป โˆˆ ๐‘‰ โˆง ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ ) โˆง ( ๐‘ฅ = ๐‘‹ โˆง ๐‘ฆ = ๐‘Œ ) ) โ†’ ( ๐‘˜ ยท ( ๐‘ฆ โˆ’ ๐‘ฅ ) ) = ( ๐‘˜ ยท ( ๐‘Œ โˆ’ ๐‘‹ ) ) )
14 10 13 eqeq12d โŠข ( ( ( ๐ป โˆˆ ๐‘‰ โˆง ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ ) โˆง ( ๐‘ฅ = ๐‘‹ โˆง ๐‘ฆ = ๐‘Œ ) ) โ†’ ( ( ๐‘ง โˆ’ ๐‘ฅ ) = ( ๐‘˜ ยท ( ๐‘ฆ โˆ’ ๐‘ฅ ) ) โ†” ( ๐‘ง โˆ’ ๐‘‹ ) = ( ๐‘˜ ยท ( ๐‘Œ โˆ’ ๐‘‹ ) ) ) )
15 14 rexbidv โŠข ( ( ( ๐ป โˆˆ ๐‘‰ โˆง ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ ) โˆง ( ๐‘ฅ = ๐‘‹ โˆง ๐‘ฆ = ๐‘Œ ) ) โ†’ ( โˆƒ ๐‘˜ โˆˆ ( 0 [,] 1 ) ( ๐‘ง โˆ’ ๐‘ฅ ) = ( ๐‘˜ ยท ( ๐‘ฆ โˆ’ ๐‘ฅ ) ) โ†” โˆƒ ๐‘˜ โˆˆ ( 0 [,] 1 ) ( ๐‘ง โˆ’ ๐‘‹ ) = ( ๐‘˜ ยท ( ๐‘Œ โˆ’ ๐‘‹ ) ) ) )
16 15 rabbidv โŠข ( ( ( ๐ป โˆˆ ๐‘‰ โˆง ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ ) โˆง ( ๐‘ฅ = ๐‘‹ โˆง ๐‘ฆ = ๐‘Œ ) ) โ†’ { ๐‘ง โˆˆ ๐‘ƒ โˆฃ โˆƒ ๐‘˜ โˆˆ ( 0 [,] 1 ) ( ๐‘ง โˆ’ ๐‘ฅ ) = ( ๐‘˜ ยท ( ๐‘ฆ โˆ’ ๐‘ฅ ) ) } = { ๐‘ง โˆˆ ๐‘ƒ โˆฃ โˆƒ ๐‘˜ โˆˆ ( 0 [,] 1 ) ( ๐‘ง โˆ’ ๐‘‹ ) = ( ๐‘˜ ยท ( ๐‘Œ โˆ’ ๐‘‹ ) ) } )
17 simp2 โŠข ( ( ๐ป โˆˆ ๐‘‰ โˆง ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ ) โ†’ ๐‘‹ โˆˆ ๐‘ƒ )
18 simp3 โŠข ( ( ๐ป โˆˆ ๐‘‰ โˆง ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ ) โ†’ ๐‘Œ โˆˆ ๐‘ƒ )
19 3 fvexi โŠข ๐‘ƒ โˆˆ V
20 19 rabex โŠข { ๐‘ง โˆˆ ๐‘ƒ โˆฃ โˆƒ ๐‘˜ โˆˆ ( 0 [,] 1 ) ( ๐‘ง โˆ’ ๐‘‹ ) = ( ๐‘˜ ยท ( ๐‘Œ โˆ’ ๐‘‹ ) ) } โˆˆ V
21 20 a1i โŠข ( ( ๐ป โˆˆ ๐‘‰ โˆง ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ ) โ†’ { ๐‘ง โˆˆ ๐‘ƒ โˆฃ โˆƒ ๐‘˜ โˆˆ ( 0 [,] 1 ) ( ๐‘ง โˆ’ ๐‘‹ ) = ( ๐‘˜ ยท ( ๐‘Œ โˆ’ ๐‘‹ ) ) } โˆˆ V )
22 8 16 17 18 21 ovmpod โŠข ( ( ๐ป โˆˆ ๐‘‰ โˆง ๐‘‹ โˆˆ ๐‘ƒ โˆง ๐‘Œ โˆˆ ๐‘ƒ ) โ†’ ( ๐‘‹ ๐ผ ๐‘Œ ) = { ๐‘ง โˆˆ ๐‘ƒ โˆฃ โˆƒ ๐‘˜ โˆˆ ( 0 [,] 1 ) ( ๐‘ง โˆ’ ๐‘‹ ) = ( ๐‘˜ ยท ( ๐‘Œ โˆ’ ๐‘‹ ) ) } )