Step | Hyp | Ref
| Expression |
1 | | ttglemOLD.2 |
. . . . . 6
β’ πΈ = Slot π |
2 | | ttglemOLD.3 |
. . . . . 6
β’ π β β |
3 | 1, 2 | ndxid 17076 |
. . . . 5
β’ πΈ = Slot (πΈβndx) |
4 | 2 | nnrei 12169 |
. . . . . . 7
β’ π β β |
5 | | ttglemOLD.4 |
. . . . . . 7
β’ π < ;16 |
6 | 4, 5 | ltneii 11275 |
. . . . . 6
β’ π β ;16 |
7 | 1, 2 | ndxarg 17075 |
. . . . . . 7
β’ (πΈβndx) = π |
8 | | itvndx 27421 |
. . . . . . 7
β’
(Itvβndx) = ;16 |
9 | 7, 8 | neeq12i 3011 |
. . . . . 6
β’ ((πΈβndx) β (Itvβndx)
β π β ;16) |
10 | 6, 9 | mpbir 230 |
. . . . 5
β’ (πΈβndx) β
(Itvβndx) |
11 | 3, 10 | setsnid 17088 |
. . . 4
β’ (πΈβπ») = (πΈβ(π» sSet β¨(Itvβndx), (π₯ β (Baseβπ»), π¦ β (Baseβπ») β¦ {π§ β (Baseβπ») β£ βπ β (0[,]1)(π§(-gβπ»)π₯) = (π( Β·π
βπ»)(π¦(-gβπ»)π₯))})β©)) |
12 | | 1nn0 12436 |
. . . . . . . . 9
β’ 1 β
β0 |
13 | | 6nn0 12441 |
. . . . . . . . 9
β’ 6 β
β0 |
14 | | 7nn 12252 |
. . . . . . . . 9
β’ 7 β
β |
15 | | 6lt7 12346 |
. . . . . . . . 9
β’ 6 <
7 |
16 | 12, 13, 14, 15 | declt 12653 |
. . . . . . . 8
β’ ;16 < ;17 |
17 | | 6nn 12249 |
. . . . . . . . . . 11
β’ 6 β
β |
18 | 12, 17 | decnncl 12645 |
. . . . . . . . . 10
β’ ;16 β β |
19 | 18 | nnrei 12169 |
. . . . . . . . 9
β’ ;16 β β |
20 | 12, 14 | decnncl 12645 |
. . . . . . . . . 10
β’ ;17 β β |
21 | 20 | nnrei 12169 |
. . . . . . . . 9
β’ ;17 β β |
22 | 4, 19, 21 | lttri 11288 |
. . . . . . . 8
β’ ((π < ;16 β§ ;16 < ;17) β π < ;17) |
23 | 5, 16, 22 | mp2an 691 |
. . . . . . 7
β’ π < ;17 |
24 | 4, 23 | ltneii 11275 |
. . . . . 6
β’ π β ;17 |
25 | | lngndx 27422 |
. . . . . . 7
β’
(LineGβndx) = ;17 |
26 | 7, 25 | neeq12i 3011 |
. . . . . 6
β’ ((πΈβndx) β
(LineGβndx) β π
β ;17) |
27 | 24, 26 | mpbir 230 |
. . . . 5
β’ (πΈβndx) β
(LineGβndx) |
28 | 3, 27 | setsnid 17088 |
. . . 4
β’ (πΈβ(π» sSet β¨(Itvβndx), (π₯ β (Baseβπ»), π¦ β (Baseβπ») β¦ {π§ β (Baseβπ») β£ βπ β (0[,]1)(π§(-gβπ»)π₯) = (π( Β·π
βπ»)(π¦(-gβπ»)π₯))})β©)) = (πΈβ((π» sSet β¨(Itvβndx), (π₯ β (Baseβπ»), π¦ β (Baseβπ») β¦ {π§ β (Baseβπ») β£ βπ β (0[,]1)(π§(-gβπ»)π₯) = (π( Β·π
βπ»)(π¦(-gβπ»)π₯))})β©) sSet β¨(LineGβndx),
(π₯ β (Baseβπ»), π¦ β (Baseβπ») β¦ {π§ β (Baseβπ») β£ (π§ β (π₯(ItvβπΊ)π¦) β¨ π₯ β (π§(ItvβπΊ)π¦) β¨ π¦ β (π₯(ItvβπΊ)π§))})β©)) |
29 | 11, 28 | eqtri 2765 |
. . 3
β’ (πΈβπ») = (πΈβ((π» sSet β¨(Itvβndx), (π₯ β (Baseβπ»), π¦ β (Baseβπ») β¦ {π§ β (Baseβπ») β£ βπ β (0[,]1)(π§(-gβπ»)π₯) = (π( Β·π
βπ»)(π¦(-gβπ»)π₯))})β©) sSet β¨(LineGβndx),
(π₯ β (Baseβπ»), π¦ β (Baseβπ») β¦ {π§ β (Baseβπ») β£ (π§ β (π₯(ItvβπΊ)π¦) β¨ π₯ β (π§(ItvβπΊ)π¦) β¨ π¦ β (π₯(ItvβπΊ)π§))})β©)) |
30 | | ttgval.n |
. . . . . 6
β’ πΊ = (toTGβπ») |
31 | | eqid 2737 |
. . . . . 6
β’
(Baseβπ») =
(Baseβπ») |
32 | | eqid 2737 |
. . . . . 6
β’
(-gβπ») = (-gβπ») |
33 | | eqid 2737 |
. . . . . 6
β’ (
Β·π βπ») = ( Β·π
βπ») |
34 | | eqid 2737 |
. . . . . 6
β’
(ItvβπΊ) =
(ItvβπΊ) |
35 | 30, 31, 32, 33, 34 | ttgval 27859 |
. . . . 5
β’ (π» β V β (πΊ = ((π» sSet β¨(Itvβndx), (π₯ β (Baseβπ»), π¦ β (Baseβπ») β¦ {π§ β (Baseβπ») β£ βπ β (0[,]1)(π§(-gβπ»)π₯) = (π( Β·π
βπ»)(π¦(-gβπ»)π₯))})β©) sSet β¨(LineGβndx),
(π₯ β (Baseβπ»), π¦ β (Baseβπ») β¦ {π§ β (Baseβπ») β£ (π§ β (π₯(ItvβπΊ)π¦) β¨ π₯ β (π§(ItvβπΊ)π¦) β¨ π¦ β (π₯(ItvβπΊ)π§))})β©) β§ (ItvβπΊ) = (π₯ β (Baseβπ»), π¦ β (Baseβπ») β¦ {π§ β (Baseβπ») β£ βπ β (0[,]1)(π§(-gβπ»)π₯) = (π( Β·π
βπ»)(π¦(-gβπ»)π₯))}))) |
36 | 35 | simpld 496 |
. . . 4
β’ (π» β V β πΊ = ((π» sSet β¨(Itvβndx), (π₯ β (Baseβπ»), π¦ β (Baseβπ») β¦ {π§ β (Baseβπ») β£ βπ β (0[,]1)(π§(-gβπ»)π₯) = (π( Β·π
βπ»)(π¦(-gβπ»)π₯))})β©) sSet β¨(LineGβndx),
(π₯ β (Baseβπ»), π¦ β (Baseβπ») β¦ {π§ β (Baseβπ») β£ (π§ β (π₯(ItvβπΊ)π¦) β¨ π₯ β (π§(ItvβπΊ)π¦) β¨ π¦ β (π₯(ItvβπΊ)π§))})β©)) |
37 | 36 | fveq2d 6851 |
. . 3
β’ (π» β V β (πΈβπΊ) = (πΈβ((π» sSet β¨(Itvβndx), (π₯ β (Baseβπ»), π¦ β (Baseβπ») β¦ {π§ β (Baseβπ») β£ βπ β (0[,]1)(π§(-gβπ»)π₯) = (π( Β·π
βπ»)(π¦(-gβπ»)π₯))})β©) sSet β¨(LineGβndx),
(π₯ β (Baseβπ»), π¦ β (Baseβπ») β¦ {π§ β (Baseβπ») β£ (π§ β (π₯(ItvβπΊ)π¦) β¨ π₯ β (π§(ItvβπΊ)π¦) β¨ π¦ β (π₯(ItvβπΊ)π§))})β©))) |
38 | 29, 37 | eqtr4id 2796 |
. 2
β’ (π» β V β (πΈβπ») = (πΈβπΊ)) |
39 | 1 | str0 17068 |
. . 3
β’ β
=
(πΈββ
) |
40 | | fvprc 6839 |
. . 3
β’ (Β¬
π» β V β (πΈβπ») = β
) |
41 | | fvprc 6839 |
. . . . 5
β’ (Β¬
π» β V β
(toTGβπ») =
β
) |
42 | 30, 41 | eqtrid 2789 |
. . . 4
β’ (Β¬
π» β V β πΊ = β
) |
43 | 42 | fveq2d 6851 |
. . 3
β’ (Β¬
π» β V β (πΈβπΊ) = (πΈββ
)) |
44 | 39, 40, 43 | 3eqtr4a 2803 |
. 2
β’ (Β¬
π» β V β (πΈβπ») = (πΈβπΊ)) |
45 | 38, 44 | pm2.61i 182 |
1
β’ (πΈβπ») = (πΈβπΊ) |