Step | Hyp | Ref
| Expression |
1 | | fvex 6901 |
. . . . . . 7
β’
(Baseβπ
)
β V |
2 | | snex 5430 |
. . . . . . 7
β’ {πΌ} β V |
3 | 1, 2 | pm3.2i 471 |
. . . . . 6
β’
((Baseβπ
)
β V β§ {πΌ} β
V) |
4 | 3 | a1i 11 |
. . . . 5
β’ (((πΌ β π β§ π
β Ring) β§ (π β (Baseβπ
) β§ π β (Baseβπ
))) β ((Baseβπ
) β V β§ {πΌ} β V)) |
5 | | mpoexga 8060 |
. . . . 5
β’
(((Baseβπ
)
β V β§ {πΌ} β
V) β (π₯ β
(Baseβπ
), π¦ β {πΌ} β¦ π¦) β V) |
6 | | lmod1.m |
. . . . . 6
β’ π = ({β¨(Baseβndx),
{πΌ}β©,
β¨(+gβndx), {β¨β¨πΌ, πΌβ©, πΌβ©}β©, β¨(Scalarβndx),
π
β©} βͺ {β¨(
Β·π βndx), (π₯ β (Baseβπ
), π¦ β {πΌ} β¦ π¦)β©}) |
7 | 6 | lmodvsca 17270 |
. . . . 5
β’ ((π₯ β (Baseβπ
), π¦ β {πΌ} β¦ π¦) β V β (π₯ β (Baseβπ
), π¦ β {πΌ} β¦ π¦) = ( Β·π
βπ)) |
8 | 4, 5, 7 | 3syl 18 |
. . . 4
β’ (((πΌ β π β§ π
β Ring) β§ (π β (Baseβπ
) β§ π β (Baseβπ
))) β (π₯ β (Baseβπ
), π¦ β {πΌ} β¦ π¦) = ( Β·π
βπ)) |
9 | 8 | eqcomd 2738 |
. . 3
β’ (((πΌ β π β§ π
β Ring) β§ (π β (Baseβπ
) β§ π β (Baseβπ
))) β (
Β·π βπ) = (π₯ β (Baseβπ
), π¦ β {πΌ} β¦ π¦)) |
10 | | simprr 771 |
. . 3
β’ ((((πΌ β π β§ π
β Ring) β§ (π β (Baseβπ
) β§ π β (Baseβπ
))) β§ (π₯ = π β§ π¦ = πΌ)) β π¦ = πΌ) |
11 | | simprl 769 |
. . 3
β’ (((πΌ β π β§ π
β Ring) β§ (π β (Baseβπ
) β§ π β (Baseβπ
))) β π β (Baseβπ
)) |
12 | | snidg 4661 |
. . . 4
β’ (πΌ β π β πΌ β {πΌ}) |
13 | 12 | ad2antrr 724 |
. . 3
β’ (((πΌ β π β§ π
β Ring) β§ (π β (Baseβπ
) β§ π β (Baseβπ
))) β πΌ β {πΌ}) |
14 | 9, 10, 11, 13, 13 | ovmpod 7556 |
. 2
β’ (((πΌ β π β§ π
β Ring) β§ (π β (Baseβπ
) β§ π β (Baseβπ
))) β (π( Β·π
βπ)πΌ) = πΌ) |
15 | | simprr 771 |
. . . 4
β’ ((((πΌ β π β§ π
β Ring) β§ (π β (Baseβπ
) β§ π β (Baseβπ
))) β§ (π₯ = π β§ π¦ = πΌ)) β π¦ = πΌ) |
16 | | simprr 771 |
. . . 4
β’ (((πΌ β π β§ π
β Ring) β§ (π β (Baseβπ
) β§ π β (Baseβπ
))) β π β (Baseβπ
)) |
17 | 9, 15, 16, 13, 13 | ovmpod 7556 |
. . 3
β’ (((πΌ β π β§ π
β Ring) β§ (π β (Baseβπ
) β§ π β (Baseβπ
))) β (π( Β·π
βπ)πΌ) = πΌ) |
18 | 17 | oveq2d 7421 |
. 2
β’ (((πΌ β π β§ π
β Ring) β§ (π β (Baseβπ
) β§ π β (Baseβπ
))) β (π( Β·π
βπ)(π(
Β·π βπ)πΌ)) = (π( Β·π
βπ)πΌ)) |
19 | | simprr 771 |
. . 3
β’ ((((πΌ β π β§ π
β Ring) β§ (π β (Baseβπ
) β§ π β (Baseβπ
))) β§ (π₯ = (π(.rβ(Scalarβπ))π) β§ π¦ = πΌ)) β π¦ = πΌ) |
20 | | simplr 767 |
. . . . . . 7
β’ (((πΌ β π β§ π
β Ring) β§ (π β (Baseβπ
) β§ π β (Baseβπ
))) β π
β Ring) |
21 | 6 | lmodsca 17269 |
. . . . . . . 8
β’ (π
β Ring β π
= (Scalarβπ)) |
22 | 21 | fveq2d 6892 |
. . . . . . 7
β’ (π
β Ring β
(.rβπ
) =
(.rβ(Scalarβπ))) |
23 | 20, 22 | syl 17 |
. . . . . 6
β’ (((πΌ β π β§ π
β Ring) β§ (π β (Baseβπ
) β§ π β (Baseβπ
))) β (.rβπ
) =
(.rβ(Scalarβπ))) |
24 | 23 | eqcomd 2738 |
. . . . 5
β’ (((πΌ β π β§ π
β Ring) β§ (π β (Baseβπ
) β§ π β (Baseβπ
))) β
(.rβ(Scalarβπ)) = (.rβπ
)) |
25 | 24 | oveqd 7422 |
. . . 4
β’ (((πΌ β π β§ π
β Ring) β§ (π β (Baseβπ
) β§ π β (Baseβπ
))) β (π(.rβ(Scalarβπ))π) = (π(.rβπ
)π)) |
26 | | eqid 2732 |
. . . . . 6
β’
(Baseβπ
) =
(Baseβπ
) |
27 | | eqid 2732 |
. . . . . 6
β’
(.rβπ
) = (.rβπ
) |
28 | 26, 27 | ringcl 20066 |
. . . . 5
β’ ((π
β Ring β§ π β (Baseβπ
) β§ π β (Baseβπ
)) β (π(.rβπ
)π) β (Baseβπ
)) |
29 | 20, 11, 16, 28 | syl3anc 1371 |
. . . 4
β’ (((πΌ β π β§ π
β Ring) β§ (π β (Baseβπ
) β§ π β (Baseβπ
))) β (π(.rβπ
)π) β (Baseβπ
)) |
30 | 25, 29 | eqeltrd 2833 |
. . 3
β’ (((πΌ β π β§ π
β Ring) β§ (π β (Baseβπ
) β§ π β (Baseβπ
))) β (π(.rβ(Scalarβπ))π) β (Baseβπ
)) |
31 | 9, 19, 30, 13, 13 | ovmpod 7556 |
. 2
β’ (((πΌ β π β§ π
β Ring) β§ (π β (Baseβπ
) β§ π β (Baseβπ
))) β ((π(.rβ(Scalarβπ))π)( Β·π
βπ)πΌ) = πΌ) |
32 | 14, 18, 31 | 3eqtr4rd 2783 |
1
β’ (((πΌ β π β§ π
β Ring) β§ (π β (Baseβπ
) β§ π β (Baseβπ
))) β ((π(.rβ(Scalarβπ))π)( Β·π
βπ)πΌ) = (π( Β·π
βπ)(π(
Β·π βπ)πΌ))) |