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 ) ( ๐ง โ ๐ ) = ( ๐ ยท ( ๐ โ ๐ ) ) } ) |