Step | Hyp | Ref
| Expression |
1 | | simpr 485 |
. . 3
β’ ((πΊ β Grp β§ π:πβΆπ΄) β π:πβΆπ΄) |
2 | 1 | feqmptd 6960 |
. 2
β’ ((πΊ β Grp β§ π:πβΆπ΄) β π = (π₯ β π β¦ (πβπ₯))) |
3 | | tngnm.x |
. . . . . . . 8
β’ π = (BaseβπΊ) |
4 | | eqid 2732 |
. . . . . . . 8
β’
(-gβπΊ) = (-gβπΊ) |
5 | 3, 4 | grpsubf 18901 |
. . . . . . 7
β’ (πΊ β Grp β
(-gβπΊ):(π Γ π)βΆπ) |
6 | 5 | ad2antrr 724 |
. . . . . 6
β’ (((πΊ β Grp β§ π:πβΆπ΄) β§ π₯ β π) β (-gβπΊ):(π Γ π)βΆπ) |
7 | | simpr 485 |
. . . . . . 7
β’ (((πΊ β Grp β§ π:πβΆπ΄) β§ π₯ β π) β π₯ β π) |
8 | | eqid 2732 |
. . . . . . . . 9
β’
(0gβπΊ) = (0gβπΊ) |
9 | 3, 8 | grpidcl 18849 |
. . . . . . . 8
β’ (πΊ β Grp β
(0gβπΊ)
β π) |
10 | 9 | ad2antrr 724 |
. . . . . . 7
β’ (((πΊ β Grp β§ π:πβΆπ΄) β§ π₯ β π) β (0gβπΊ) β π) |
11 | 7, 10 | opelxpd 5715 |
. . . . . 6
β’ (((πΊ β Grp β§ π:πβΆπ΄) β§ π₯ β π) β β¨π₯, (0gβπΊ)β© β (π Γ π)) |
12 | | fvco3 6990 |
. . . . . 6
β’
(((-gβπΊ):(π Γ π)βΆπ β§ β¨π₯, (0gβπΊ)β© β (π Γ π)) β ((π β (-gβπΊ))ββ¨π₯, (0gβπΊ)β©) = (πβ((-gβπΊ)ββ¨π₯, (0gβπΊ)β©))) |
13 | 6, 11, 12 | syl2anc 584 |
. . . . 5
β’ (((πΊ β Grp β§ π:πβΆπ΄) β§ π₯ β π) β ((π β (-gβπΊ))ββ¨π₯, (0gβπΊ)β©) = (πβ((-gβπΊ)ββ¨π₯, (0gβπΊ)β©))) |
14 | | df-ov 7411 |
. . . . 5
β’ (π₯(π β (-gβπΊ))(0gβπΊ)) = ((π β (-gβπΊ))ββ¨π₯, (0gβπΊ)β©) |
15 | | df-ov 7411 |
. . . . . 6
β’ (π₯(-gβπΊ)(0gβπΊ)) = ((-gβπΊ)ββ¨π₯, (0gβπΊ)β©) |
16 | 15 | fveq2i 6894 |
. . . . 5
β’ (πβ(π₯(-gβπΊ)(0gβπΊ))) = (πβ((-gβπΊ)ββ¨π₯, (0gβπΊ)β©)) |
17 | 13, 14, 16 | 3eqtr4g 2797 |
. . . 4
β’ (((πΊ β Grp β§ π:πβΆπ΄) β§ π₯ β π) β (π₯(π β (-gβπΊ))(0gβπΊ)) = (πβ(π₯(-gβπΊ)(0gβπΊ)))) |
18 | 3, 8, 4 | grpsubid1 18907 |
. . . . . 6
β’ ((πΊ β Grp β§ π₯ β π) β (π₯(-gβπΊ)(0gβπΊ)) = π₯) |
19 | 18 | adantlr 713 |
. . . . 5
β’ (((πΊ β Grp β§ π:πβΆπ΄) β§ π₯ β π) β (π₯(-gβπΊ)(0gβπΊ)) = π₯) |
20 | 19 | fveq2d 6895 |
. . . 4
β’ (((πΊ β Grp β§ π:πβΆπ΄) β§ π₯ β π) β (πβ(π₯(-gβπΊ)(0gβπΊ))) = (πβπ₯)) |
21 | 17, 20 | eqtr2d 2773 |
. . 3
β’ (((πΊ β Grp β§ π:πβΆπ΄) β§ π₯ β π) β (πβπ₯) = (π₯(π β (-gβπΊ))(0gβπΊ))) |
22 | 21 | mpteq2dva 5248 |
. 2
β’ ((πΊ β Grp β§ π:πβΆπ΄) β (π₯ β π β¦ (πβπ₯)) = (π₯ β π β¦ (π₯(π β (-gβπΊ))(0gβπΊ)))) |
23 | 3 | fvexi 6905 |
. . . . . . 7
β’ π β V |
24 | | tngnm.a |
. . . . . . 7
β’ π΄ β V |
25 | | fex2 7923 |
. . . . . . 7
β’ ((π:πβΆπ΄ β§ π β V β§ π΄ β V) β π β V) |
26 | 23, 24, 25 | mp3an23 1453 |
. . . . . 6
β’ (π:πβΆπ΄ β π β V) |
27 | 26 | adantl 482 |
. . . . 5
β’ ((πΊ β Grp β§ π:πβΆπ΄) β π β V) |
28 | | tngnm.t |
. . . . . 6
β’ π = (πΊ toNrmGrp π) |
29 | 28, 3 | tngbas 24150 |
. . . . 5
β’ (π β V β π = (Baseβπ)) |
30 | 27, 29 | syl 17 |
. . . 4
β’ ((πΊ β Grp β§ π:πβΆπ΄) β π = (Baseβπ)) |
31 | 28, 4 | tngds 24163 |
. . . . . 6
β’ (π β V β (π β
(-gβπΊ)) =
(distβπ)) |
32 | 27, 31 | syl 17 |
. . . . 5
β’ ((πΊ β Grp β§ π:πβΆπ΄) β (π β (-gβπΊ)) = (distβπ)) |
33 | | eqidd 2733 |
. . . . 5
β’ ((πΊ β Grp β§ π:πβΆπ΄) β π₯ = π₯) |
34 | 28, 8 | tng0 24154 |
. . . . . 6
β’ (π β V β
(0gβπΊ) =
(0gβπ)) |
35 | 27, 34 | syl 17 |
. . . . 5
β’ ((πΊ β Grp β§ π:πβΆπ΄) β (0gβπΊ) = (0gβπ)) |
36 | 32, 33, 35 | oveq123d 7429 |
. . . 4
β’ ((πΊ β Grp β§ π:πβΆπ΄) β (π₯(π β (-gβπΊ))(0gβπΊ)) = (π₯(distβπ)(0gβπ))) |
37 | 30, 36 | mpteq12dv 5239 |
. . 3
β’ ((πΊ β Grp β§ π:πβΆπ΄) β (π₯ β π β¦ (π₯(π β (-gβπΊ))(0gβπΊ))) = (π₯ β (Baseβπ) β¦ (π₯(distβπ)(0gβπ)))) |
38 | | eqid 2732 |
. . . 4
β’
(normβπ) =
(normβπ) |
39 | | eqid 2732 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
40 | | eqid 2732 |
. . . 4
β’
(0gβπ) = (0gβπ) |
41 | | eqid 2732 |
. . . 4
β’
(distβπ) =
(distβπ) |
42 | 38, 39, 40, 41 | nmfval 24096 |
. . 3
β’
(normβπ) =
(π₯ β (Baseβπ) β¦ (π₯(distβπ)(0gβπ))) |
43 | 37, 42 | eqtr4di 2790 |
. 2
β’ ((πΊ β Grp β§ π:πβΆπ΄) β (π₯ β π β¦ (π₯(π β (-gβπΊ))(0gβπΊ))) = (normβπ)) |
44 | 2, 22, 43 | 3eqtrd 2776 |
1
β’ ((πΊ β Grp β§ π:πβΆπ΄) β π = (normβπ)) |