Step | Hyp | Ref
| Expression |
1 | | resrng 21028 |
. . . . 5
β’
βfld β *-Ring |
2 | | srngring 20314 |
. . . . 5
β’
(βfld β *-Ring β βfld β
Ring) |
3 | 1, 2 | ax-mp 5 |
. . . 4
β’
βfld β Ring |
4 | | eqid 2737 |
. . . . 5
β’
(βfld freeLMod πΌ) = (βfld freeLMod πΌ) |
5 | 4 | frlmlmod 21158 |
. . . 4
β’
((βfld β Ring β§ πΌ β π) β (βfld freeLMod
πΌ) β
LMod) |
6 | 3, 5 | mpan 689 |
. . 3
β’ (πΌ β π β (βfld freeLMod
πΌ) β
LMod) |
7 | | lmodgrp 20332 |
. . 3
β’
((βfld freeLMod πΌ) β LMod β (βfld
freeLMod πΌ) β
Grp) |
8 | | eqid 2737 |
. . . 4
β’
(toβPreHilβ(βfld freeLMod πΌ)) =
(toβPreHilβ(βfld freeLMod πΌ)) |
9 | | eqid 2737 |
. . . 4
β’
(normβ(toβPreHilβ(βfld freeLMod πΌ))) =
(normβ(toβPreHilβ(βfld freeLMod πΌ))) |
10 | | eqid 2737 |
. . . 4
β’
(Baseβ(βfld freeLMod πΌ)) = (Baseβ(βfld
freeLMod πΌ)) |
11 | | eqid 2737 |
. . . 4
β’
(Β·πβ(βfld
freeLMod πΌ)) =
(Β·πβ(βfld freeLMod
πΌ)) |
12 | 8, 9, 10, 11 | tchnmfval 24595 |
. . 3
β’
((βfld freeLMod πΌ) β Grp β
(normβ(toβPreHilβ(βfld freeLMod πΌ))) = (π β (Baseβ(βfld
freeLMod πΌ)) β¦
(ββ(π(Β·πβ(βfld
freeLMod πΌ))π)))) |
13 | 6, 7, 12 | 3syl 18 |
. 2
β’ (πΌ β π β
(normβ(toβPreHilβ(βfld freeLMod πΌ))) = (π β (Baseβ(βfld
freeLMod πΌ)) β¦
(ββ(π(Β·πβ(βfld
freeLMod πΌ))π)))) |
14 | | rrxval.r |
. . . 4
β’ π» = (β^βπΌ) |
15 | 14 | rrxval 24754 |
. . 3
β’ (πΌ β π β π» =
(toβPreHilβ(βfld freeLMod πΌ))) |
16 | 15 | fveq2d 6847 |
. 2
β’ (πΌ β π β (normβπ») =
(normβ(toβPreHilβ(βfld freeLMod πΌ)))) |
17 | 15 | fveq2d 6847 |
. . . 4
β’ (πΌ β π β (Baseβπ») =
(Baseβ(toβPreHilβ(βfld freeLMod πΌ)))) |
18 | | rrxbase.b |
. . . 4
β’ π΅ = (Baseβπ») |
19 | 8, 10 | tcphbas 24586 |
. . . 4
β’
(Baseβ(βfld freeLMod πΌ)) =
(Baseβ(toβPreHilβ(βfld freeLMod πΌ))) |
20 | 17, 18, 19 | 3eqtr4g 2802 |
. . 3
β’ (πΌ β π β π΅ = (Baseβ(βfld
freeLMod πΌ))) |
21 | 14, 18 | rrxbase 24755 |
. . . . . . . 8
β’ (πΌ β π β π΅ = {π β (β βm πΌ) β£ π finSupp 0}) |
22 | | ssrab2 4038 |
. . . . . . . 8
β’ {π β (β
βm πΌ)
β£ π finSupp 0}
β (β βm πΌ) |
23 | 21, 22 | eqsstrdi 3999 |
. . . . . . 7
β’ (πΌ β π β π΅ β (β βm πΌ)) |
24 | 23 | sselda 3945 |
. . . . . 6
β’ ((πΌ β π β§ π β π΅) β π β (β βm πΌ)) |
25 | 15 | fveq2d 6847 |
. . . . . . . . 9
β’ (πΌ β π β
(Β·πβπ») =
(Β·πβ(toβPreHilβ(βfld
freeLMod πΌ)))) |
26 | 14, 18 | rrxip 24757 |
. . . . . . . . 9
β’ (πΌ β π β (β β (β βm πΌ), π β (β βm πΌ) β¦ (βfld
Ξ£g (π₯ β πΌ β¦ ((ββπ₯) Β· (πβπ₯))))) =
(Β·πβπ»)) |
27 | 8, 11 | tcphip 24592 |
. . . . . . . . . 10
β’
(Β·πβ(βfld
freeLMod πΌ)) =
(Β·πβ(toβPreHilβ(βfld
freeLMod πΌ))) |
28 | 27 | a1i 11 |
. . . . . . . . 9
β’ (πΌ β π β
(Β·πβ(βfld freeLMod
πΌ)) =
(Β·πβ(toβPreHilβ(βfld
freeLMod πΌ)))) |
29 | 25, 26, 28 | 3eqtr4rd 2788 |
. . . . . . . 8
β’ (πΌ β π β
(Β·πβ(βfld freeLMod
πΌ)) = (β β (β βm πΌ), π β (β βm πΌ) β¦ (βfld
Ξ£g (π₯ β πΌ β¦ ((ββπ₯) Β· (πβπ₯)))))) |
30 | 29 | adantr 482 |
. . . . . . 7
β’ ((πΌ β π β§ π β (β βm πΌ)) β
(Β·πβ(βfld freeLMod
πΌ)) = (β β (β βm πΌ), π β (β βm πΌ) β¦ (βfld
Ξ£g (π₯ β πΌ β¦ ((ββπ₯) Β· (πβπ₯)))))) |
31 | | simprl 770 |
. . . . . . . . . . . . 13
β’ (((πΌ β π β§ π β (β βm πΌ)) β§ (β = π β§ π = π)) β β = π) |
32 | 31 | fveq1d 6845 |
. . . . . . . . . . . 12
β’ (((πΌ β π β§ π β (β βm πΌ)) β§ (β = π β§ π = π)) β (ββπ₯) = (πβπ₯)) |
33 | | simprr 772 |
. . . . . . . . . . . . 13
β’ (((πΌ β π β§ π β (β βm πΌ)) β§ (β = π β§ π = π)) β π = π) |
34 | 33 | fveq1d 6845 |
. . . . . . . . . . . 12
β’ (((πΌ β π β§ π β (β βm πΌ)) β§ (β = π β§ π = π)) β (πβπ₯) = (πβπ₯)) |
35 | 32, 34 | oveq12d 7376 |
. . . . . . . . . . 11
β’ (((πΌ β π β§ π β (β βm πΌ)) β§ (β = π β§ π = π)) β ((ββπ₯) Β· (πβπ₯)) = ((πβπ₯) Β· (πβπ₯))) |
36 | 35 | adantr 482 |
. . . . . . . . . 10
β’ ((((πΌ β π β§ π β (β βm πΌ)) β§ (β = π β§ π = π)) β§ π₯ β πΌ) β ((ββπ₯) Β· (πβπ₯)) = ((πβπ₯) Β· (πβπ₯))) |
37 | | elmapi 8788 |
. . . . . . . . . . . . . . 15
β’ (π β (β
βm πΌ)
β π:πΌβΆβ) |
38 | 37 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((πΌ β π β§ π β (β βm πΌ)) β π:πΌβΆβ) |
39 | 38 | ffvelcdmda 7036 |
. . . . . . . . . . . . 13
β’ (((πΌ β π β§ π β (β βm πΌ)) β§ π₯ β πΌ) β (πβπ₯) β β) |
40 | 39 | recnd 11184 |
. . . . . . . . . . . 12
β’ (((πΌ β π β§ π β (β βm πΌ)) β§ π₯ β πΌ) β (πβπ₯) β β) |
41 | 40 | adantlr 714 |
. . . . . . . . . . 11
β’ ((((πΌ β π β§ π β (β βm πΌ)) β§ (β = π β§ π = π)) β§ π₯ β πΌ) β (πβπ₯) β β) |
42 | 41 | sqvald 14049 |
. . . . . . . . . 10
β’ ((((πΌ β π β§ π β (β βm πΌ)) β§ (β = π β§ π = π)) β§ π₯ β πΌ) β ((πβπ₯)β2) = ((πβπ₯) Β· (πβπ₯))) |
43 | 36, 42 | eqtr4d 2780 |
. . . . . . . . 9
β’ ((((πΌ β π β§ π β (β βm πΌ)) β§ (β = π β§ π = π)) β§ π₯ β πΌ) β ((ββπ₯) Β· (πβπ₯)) = ((πβπ₯)β2)) |
44 | 43 | mpteq2dva 5206 |
. . . . . . . 8
β’ (((πΌ β π β§ π β (β βm πΌ)) β§ (β = π β§ π = π)) β (π₯ β πΌ β¦ ((ββπ₯) Β· (πβπ₯))) = (π₯ β πΌ β¦ ((πβπ₯)β2))) |
45 | 44 | oveq2d 7374 |
. . . . . . 7
β’ (((πΌ β π β§ π β (β βm πΌ)) β§ (β = π β§ π = π)) β (βfld
Ξ£g (π₯ β πΌ β¦ ((ββπ₯) Β· (πβπ₯)))) = (βfld
Ξ£g (π₯ β πΌ β¦ ((πβπ₯)β2)))) |
46 | | simpr 486 |
. . . . . . 7
β’ ((πΌ β π β§ π β (β βm πΌ)) β π β (β βm πΌ)) |
47 | | ovexd 7393 |
. . . . . . 7
β’ ((πΌ β π β§ π β (β βm πΌ)) β (βfld
Ξ£g (π₯ β πΌ β¦ ((πβπ₯)β2))) β V) |
48 | 30, 45, 46, 46, 47 | ovmpod 7508 |
. . . . . 6
β’ ((πΌ β π β§ π β (β βm πΌ)) β (π(Β·πβ(βfld
freeLMod πΌ))π) = (βfld Ξ£g (π₯ β πΌ β¦ ((πβπ₯)β2)))) |
49 | 24, 48 | syldan 592 |
. . . . 5
β’ ((πΌ β π β§ π β π΅) β (π(Β·πβ(βfld
freeLMod πΌ))π) = (βfld Ξ£g (π₯ β πΌ β¦ ((πβπ₯)β2)))) |
50 | 49 | eqcomd 2743 |
. . . 4
β’ ((πΌ β π β§ π β π΅) β (βfld
Ξ£g (π₯ β πΌ β¦ ((πβπ₯)β2))) = (π(Β·πβ(βfld
freeLMod πΌ))π)) |
51 | 50 | fveq2d 6847 |
. . 3
β’ ((πΌ β π β§ π β π΅) β
(ββ(βfld Ξ£g (π₯ β πΌ β¦ ((πβπ₯)β2)))) = (ββ(π(Β·πβ(βfld
freeLMod πΌ))π))) |
52 | 20, 51 | mpteq12dva 5195 |
. 2
β’ (πΌ β π β (π β π΅ β¦
(ββ(βfld Ξ£g (π₯ β πΌ β¦ ((πβπ₯)β2))))) = (π β (Baseβ(βfld
freeLMod πΌ)) β¦
(ββ(π(Β·πβ(βfld
freeLMod πΌ))π)))) |
53 | 13, 16, 52 | 3eqtr4rd 2788 |
1
β’ (πΌ β π β (π β π΅ β¦
(ββ(βfld Ξ£g (π₯ β πΌ β¦ ((πβπ₯)β2))))) = (normβπ»)) |