Step | Hyp | Ref
| Expression |
1 | | simpll 764 |
. . . 4
β’ (((π β§ π β (0[,]1)) β§ (π β π) = (π Β· (π β π))) β π) |
2 | | simpr 484 |
. . . . 5
β’ (((π β§ π β (0[,]1)) β§ (π β π) = (π Β· (π β π))) β (π β π) = (π Β· (π β π))) |
3 | | ttgbtwnid.1 |
. . . . . . . . 9
β’ (π β π» β βMod) |
4 | | clmlmod 24949 |
. . . . . . . . 9
β’ (π» β βMod β π» β LMod) |
5 | 3, 4 | syl 17 |
. . . . . . . 8
β’ (π β π» β LMod) |
6 | | ttgelitv.x |
. . . . . . . 8
β’ (π β π β π) |
7 | | ttgitvval.b |
. . . . . . . . 9
β’ π = (Baseβπ») |
8 | | eqid 2726 |
. . . . . . . . 9
β’
(0gβπ») = (0gβπ») |
9 | | ttgitvval.m |
. . . . . . . . 9
β’ β =
(-gβπ») |
10 | 7, 8, 9 | lmodsubid 20768 |
. . . . . . . 8
β’ ((π» β LMod β§ π β π) β (π β π) = (0gβπ»)) |
11 | 5, 6, 10 | syl2anc 583 |
. . . . . . 7
β’ (π β (π β π) = (0gβπ»)) |
12 | 11 | ad2antrr 723 |
. . . . . 6
β’ (((π β§ π β (0[,]1)) β§ (π β π) = (π Β· (π β π))) β (π β π) = (0gβπ»)) |
13 | 12 | oveq2d 7421 |
. . . . 5
β’ (((π β§ π β (0[,]1)) β§ (π β π) = (π Β· (π β π))) β (π Β· (π β π)) = (π Β·
(0gβπ»))) |
14 | 5 | ad2antrr 723 |
. . . . . 6
β’ (((π β§ π β (0[,]1)) β§ (π β π) = (π Β· (π β π))) β π» β LMod) |
15 | | ttgbtwnid.2 |
. . . . . . . 8
β’ (π β (0[,]1) β π
) |
16 | 15 | ad2antrr 723 |
. . . . . . 7
β’ (((π β§ π β (0[,]1)) β§ (π β π) = (π Β· (π β π))) β (0[,]1) β π
) |
17 | | simplr 766 |
. . . . . . 7
β’ (((π β§ π β (0[,]1)) β§ (π β π) = (π Β· (π β π))) β π β (0[,]1)) |
18 | 16, 17 | sseldd 3978 |
. . . . . 6
β’ (((π β§ π β (0[,]1)) β§ (π β π) = (π Β· (π β π))) β π β π
) |
19 | | eqid 2726 |
. . . . . . 7
β’
(Scalarβπ») =
(Scalarβπ») |
20 | | ttgitvval.s |
. . . . . . 7
β’ Β· = (
Β·π βπ») |
21 | | ttgbtwnid.r |
. . . . . . 7
β’ π
=
(Baseβ(Scalarβπ»)) |
22 | 19, 20, 21, 8 | lmodvs0 20742 |
. . . . . 6
β’ ((π» β LMod β§ π β π
) β (π Β·
(0gβπ»)) =
(0gβπ»)) |
23 | 14, 18, 22 | syl2anc 583 |
. . . . 5
β’ (((π β§ π β (0[,]1)) β§ (π β π) = (π Β· (π β π))) β (π Β·
(0gβπ»)) =
(0gβπ»)) |
24 | 2, 13, 23 | 3eqtrd 2770 |
. . . 4
β’ (((π β§ π β (0[,]1)) β§ (π β π) = (π Β· (π β π))) β (π β π) = (0gβπ»)) |
25 | | ttgelitv.y |
. . . . . 6
β’ (π β π β π) |
26 | 7, 8, 9 | lmodsubeq0 20767 |
. . . . . 6
β’ ((π» β LMod β§ π β π β§ π β π) β ((π β π) = (0gβπ») β π = π)) |
27 | 5, 25, 6, 26 | syl3anc 1368 |
. . . . 5
β’ (π β ((π β π) = (0gβπ») β π = π)) |
28 | 27 | biimpa 476 |
. . . 4
β’ ((π β§ (π β π) = (0gβπ»)) β π = π) |
29 | 1, 24, 28 | syl2anc 583 |
. . 3
β’ (((π β§ π β (0[,]1)) β§ (π β π) = (π Β· (π β π))) β π = π) |
30 | 29 | eqcomd 2732 |
. 2
β’ (((π β§ π β (0[,]1)) β§ (π β π) = (π Β· (π β π))) β π = π) |
31 | | ttgbtwnid.y |
. . 3
β’ (π β π β (ππΌπ)) |
32 | | ttgval.n |
. . . 4
β’ πΊ = (toTGβπ») |
33 | | ttgitvval.i |
. . . 4
β’ πΌ = (ItvβπΊ) |
34 | 32, 33, 7, 9, 20, 6,
6, 3, 25 | ttgelitv 28648 |
. . 3
β’ (π β (π β (ππΌπ) β βπ β (0[,]1)(π β π) = (π Β· (π β π)))) |
35 | 31, 34 | mpbid 231 |
. 2
β’ (π β βπ β (0[,]1)(π β π) = (π Β· (π β π))) |
36 | 30, 35 | r19.29a 3156 |
1
β’ (π β π = π) |