Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . 3
β’ ((πΊ β Grp β§ π:πβΆπ΄) β π:πβΆπ΄) |
2 | 1 | feqmptd 6914 |
. 2
β’ ((πΊ β Grp β§ π:πβΆπ΄) β π = (π₯ β π β¦ (πβπ₯))) |
3 | | tngnm.x |
. . . . . . . 8
β’ π = (BaseβπΊ) |
4 | | eqid 2733 |
. . . . . . . 8
β’
(-gβπΊ) = (-gβπΊ) |
5 | 3, 4 | grpsubf 18834 |
. . . . . . 7
β’ (πΊ β Grp β
(-gβπΊ):(π Γ π)βΆπ) |
6 | 5 | ad2antrr 725 |
. . . . . 6
β’ (((πΊ β Grp β§ π:πβΆπ΄) β§ π₯ β π) β (-gβπΊ):(π Γ π)βΆπ) |
7 | | simpr 486 |
. . . . . . 7
β’ (((πΊ β Grp β§ π:πβΆπ΄) β§ π₯ β π) β π₯ β π) |
8 | | eqid 2733 |
. . . . . . . . 9
β’
(0gβπΊ) = (0gβπΊ) |
9 | 3, 8 | grpidcl 18786 |
. . . . . . . 8
β’ (πΊ β Grp β
(0gβπΊ)
β π) |
10 | 9 | ad2antrr 725 |
. . . . . . 7
β’ (((πΊ β Grp β§ π:πβΆπ΄) β§ π₯ β π) β (0gβπΊ) β π) |
11 | 7, 10 | opelxpd 5675 |
. . . . . 6
β’ (((πΊ β Grp β§ π:πβΆπ΄) β§ π₯ β π) β β¨π₯, (0gβπΊ)β© β (π Γ π)) |
12 | | fvco3 6944 |
. . . . . 6
β’
(((-gβπΊ):(π Γ π)βΆπ β§ β¨π₯, (0gβπΊ)β© β (π Γ π)) β ((π β (-gβπΊ))ββ¨π₯, (0gβπΊ)β©) = (πβ((-gβπΊ)ββ¨π₯, (0gβπΊ)β©))) |
13 | 6, 11, 12 | syl2anc 585 |
. . . . 5
β’ (((πΊ β Grp β§ π:πβΆπ΄) β§ π₯ β π) β ((π β (-gβπΊ))ββ¨π₯, (0gβπΊ)β©) = (πβ((-gβπΊ)ββ¨π₯, (0gβπΊ)β©))) |
14 | | df-ov 7364 |
. . . . 5
β’ (π₯(π β (-gβπΊ))(0gβπΊ)) = ((π β (-gβπΊ))ββ¨π₯, (0gβπΊ)β©) |
15 | | df-ov 7364 |
. . . . . 6
β’ (π₯(-gβπΊ)(0gβπΊ)) = ((-gβπΊ)ββ¨π₯, (0gβπΊ)β©) |
16 | 15 | fveq2i 6849 |
. . . . 5
β’ (πβ(π₯(-gβπΊ)(0gβπΊ))) = (πβ((-gβπΊ)ββ¨π₯, (0gβπΊ)β©)) |
17 | 13, 14, 16 | 3eqtr4g 2798 |
. . . 4
β’ (((πΊ β Grp β§ π:πβΆπ΄) β§ π₯ β π) β (π₯(π β (-gβπΊ))(0gβπΊ)) = (πβ(π₯(-gβπΊ)(0gβπΊ)))) |
18 | 3, 8, 4 | grpsubid1 18840 |
. . . . . 6
β’ ((πΊ β Grp β§ π₯ β π) β (π₯(-gβπΊ)(0gβπΊ)) = π₯) |
19 | 18 | adantlr 714 |
. . . . 5
β’ (((πΊ β Grp β§ π:πβΆπ΄) β§ π₯ β π) β (π₯(-gβπΊ)(0gβπΊ)) = π₯) |
20 | 19 | fveq2d 6850 |
. . . 4
β’ (((πΊ β Grp β§ π:πβΆπ΄) β§ π₯ β π) β (πβ(π₯(-gβπΊ)(0gβπΊ))) = (πβπ₯)) |
21 | 17, 20 | eqtr2d 2774 |
. . 3
β’ (((πΊ β Grp β§ π:πβΆπ΄) β§ π₯ β π) β (πβπ₯) = (π₯(π β (-gβπΊ))(0gβπΊ))) |
22 | 21 | mpteq2dva 5209 |
. 2
β’ ((πΊ β Grp β§ π:πβΆπ΄) β (π₯ β π β¦ (πβπ₯)) = (π₯ β π β¦ (π₯(π β (-gβπΊ))(0gβπΊ)))) |
23 | 3 | fvexi 6860 |
. . . . . . 7
β’ π β V |
24 | | tngnm.a |
. . . . . . 7
β’ π΄ β V |
25 | | fex2 7874 |
. . . . . . 7
β’ ((π:πβΆπ΄ β§ π β V β§ π΄ β V) β π β V) |
26 | 23, 24, 25 | mp3an23 1454 |
. . . . . 6
β’ (π:πβΆπ΄ β π β V) |
27 | 26 | adantl 483 |
. . . . 5
β’ ((πΊ β Grp β§ π:πβΆπ΄) β π β V) |
28 | | tngnm.t |
. . . . . 6
β’ π = (πΊ toNrmGrp π) |
29 | 28, 3 | tngbas 24021 |
. . . . 5
β’ (π β V β π = (Baseβπ)) |
30 | 27, 29 | syl 17 |
. . . 4
β’ ((πΊ β Grp β§ π:πβΆπ΄) β π = (Baseβπ)) |
31 | 28, 4 | tngds 24034 |
. . . . . 6
β’ (π β V β (π β
(-gβπΊ)) =
(distβπ)) |
32 | 27, 31 | syl 17 |
. . . . 5
β’ ((πΊ β Grp β§ π:πβΆπ΄) β (π β (-gβπΊ)) = (distβπ)) |
33 | | eqidd 2734 |
. . . . 5
β’ ((πΊ β Grp β§ π:πβΆπ΄) β π₯ = π₯) |
34 | 28, 8 | tng0 24025 |
. . . . . 6
β’ (π β V β
(0gβπΊ) =
(0gβπ)) |
35 | 27, 34 | syl 17 |
. . . . 5
β’ ((πΊ β Grp β§ π:πβΆπ΄) β (0gβπΊ) = (0gβπ)) |
36 | 32, 33, 35 | oveq123d 7382 |
. . . 4
β’ ((πΊ β Grp β§ π:πβΆπ΄) β (π₯(π β (-gβπΊ))(0gβπΊ)) = (π₯(distβπ)(0gβπ))) |
37 | 30, 36 | mpteq12dv 5200 |
. . 3
β’ ((πΊ β Grp β§ π:πβΆπ΄) β (π₯ β π β¦ (π₯(π β (-gβπΊ))(0gβπΊ))) = (π₯ β (Baseβπ) β¦ (π₯(distβπ)(0gβπ)))) |
38 | | eqid 2733 |
. . . 4
β’
(normβπ) =
(normβπ) |
39 | | eqid 2733 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
40 | | eqid 2733 |
. . . 4
β’
(0gβπ) = (0gβπ) |
41 | | eqid 2733 |
. . . 4
β’
(distβπ) =
(distβπ) |
42 | 38, 39, 40, 41 | nmfval 23967 |
. . 3
β’
(normβπ) =
(π₯ β (Baseβπ) β¦ (π₯(distβπ)(0gβπ))) |
43 | 37, 42 | eqtr4di 2791 |
. 2
β’ ((πΊ β Grp β§ π:πβΆπ΄) β (π₯ β π β¦ (π₯(π β (-gβπΊ))(0gβπΊ))) = (normβπ)) |
44 | 2, 22, 43 | 3eqtrd 2777 |
1
β’ ((πΊ β Grp β§ π:πβΆπ΄) β π = (normβπ)) |