Step | Hyp | Ref
| Expression |
1 | | isnlm.v |
. . . . 5
β’ π = (Baseβπ) |
2 | | isnlm.n |
. . . . 5
β’ π = (normβπ) |
3 | | isnlm.s |
. . . . 5
β’ Β· = (
Β·π βπ) |
4 | | isnlm.f |
. . . . 5
β’ πΉ = (Scalarβπ) |
5 | | isnlm.k |
. . . . 5
β’ πΎ = (BaseβπΉ) |
6 | | isnlm.a |
. . . . 5
β’ π΄ = (normβπΉ) |
7 | 1, 2, 3, 4, 5, 6 | isnlm 24062 |
. . . 4
β’ (π β NrmMod β ((π β NrmGrp β§ π β LMod β§ πΉ β NrmRing) β§
βπ₯ β πΎ βπ¦ β π (πβ(π₯ Β· π¦)) = ((π΄βπ₯) Β· (πβπ¦)))) |
8 | 7 | simprbi 498 |
. . 3
β’ (π β NrmMod β
βπ₯ β πΎ βπ¦ β π (πβ(π₯ Β· π¦)) = ((π΄βπ₯) Β· (πβπ¦))) |
9 | | fvoveq1 7384 |
. . . . 5
β’ (π₯ = π β (πβ(π₯ Β· π¦)) = (πβ(π Β· π¦))) |
10 | | fveq2 6846 |
. . . . . 6
β’ (π₯ = π β (π΄βπ₯) = (π΄βπ)) |
11 | 10 | oveq1d 7376 |
. . . . 5
β’ (π₯ = π β ((π΄βπ₯) Β· (πβπ¦)) = ((π΄βπ) Β· (πβπ¦))) |
12 | 9, 11 | eqeq12d 2749 |
. . . 4
β’ (π₯ = π β ((πβ(π₯ Β· π¦)) = ((π΄βπ₯) Β· (πβπ¦)) β (πβ(π Β· π¦)) = ((π΄βπ) Β· (πβπ¦)))) |
13 | | oveq2 7369 |
. . . . . 6
β’ (π¦ = π β (π Β· π¦) = (π Β· π)) |
14 | 13 | fveq2d 6850 |
. . . . 5
β’ (π¦ = π β (πβ(π Β· π¦)) = (πβ(π Β· π))) |
15 | | fveq2 6846 |
. . . . . 6
β’ (π¦ = π β (πβπ¦) = (πβπ)) |
16 | 15 | oveq2d 7377 |
. . . . 5
β’ (π¦ = π β ((π΄βπ) Β· (πβπ¦)) = ((π΄βπ) Β· (πβπ))) |
17 | 14, 16 | eqeq12d 2749 |
. . . 4
β’ (π¦ = π β ((πβ(π Β· π¦)) = ((π΄βπ) Β· (πβπ¦)) β (πβ(π Β· π)) = ((π΄βπ) Β· (πβπ)))) |
18 | 12, 17 | rspc2v 3592 |
. . 3
β’ ((π β πΎ β§ π β π) β (βπ₯ β πΎ βπ¦ β π (πβ(π₯ Β· π¦)) = ((π΄βπ₯) Β· (πβπ¦)) β (πβ(π Β· π)) = ((π΄βπ) Β· (πβπ)))) |
19 | 8, 18 | syl5com 31 |
. 2
β’ (π β NrmMod β ((π β πΎ β§ π β π) β (πβ(π Β· π)) = ((π΄βπ) Β· (πβπ)))) |
20 | 19 | 3impib 1117 |
1
β’ ((π β NrmMod β§ π β πΎ β§ π β π) β (πβ(π Β· π)) = ((π΄βπ) Β· (πβπ))) |