Step | Hyp | Ref
| Expression |
1 | | fvex 6904 |
. . . . . . 7
β’
(Baseβπ
)
β V |
2 | | snex 5431 |
. . . . . . 7
β’ {πΌ} β V |
3 | 1, 2 | pm3.2i 471 |
. . . . . 6
β’
((Baseβπ
)
β V β§ {πΌ} β
V) |
4 | | mpoexga 8066 |
. . . . . 6
β’
(((Baseβπ
)
β V β§ {πΌ} β
V) β (π₯ β
(Baseβπ
), π¦ β {πΌ} β¦ π¦) β V) |
5 | 3, 4 | mp1i 13 |
. . . . 5
β’ ((πΌ β π β§ π
β Ring β§ π β (Baseβπ
)) β (π₯ β (Baseβπ
), π¦ β {πΌ} β¦ π¦) β V) |
6 | | lmod1.m |
. . . . . 6
β’ π = ({β¨(Baseβndx),
{πΌ}β©,
β¨(+gβndx), {β¨β¨πΌ, πΌβ©, πΌβ©}β©, β¨(Scalarβndx),
π
β©} βͺ {β¨(
Β·π βndx), (π₯ β (Baseβπ
), π¦ β {πΌ} β¦ π¦)β©}) |
7 | 6 | lmodvsca 17276 |
. . . . 5
β’ ((π₯ β (Baseβπ
), π¦ β {πΌ} β¦ π¦) β V β (π₯ β (Baseβπ
), π¦ β {πΌ} β¦ π¦) = ( Β·π
βπ)) |
8 | 5, 7 | syl 17 |
. . . 4
β’ ((πΌ β π β§ π
β Ring β§ π β (Baseβπ
)) β (π₯ β (Baseβπ
), π¦ β {πΌ} β¦ π¦) = ( Β·π
βπ)) |
9 | 8 | eqcomd 2738 |
. . 3
β’ ((πΌ β π β§ π
β Ring β§ π β (Baseβπ
)) β (
Β·π βπ) = (π₯ β (Baseβπ
), π¦ β {πΌ} β¦ π¦)) |
10 | | simprr 771 |
. . 3
β’ (((πΌ β π β§ π
β Ring β§ π β (Baseβπ
)) β§ (π₯ = π β§ π¦ = πΌ)) β π¦ = πΌ) |
11 | | simp3 1138 |
. . 3
β’ ((πΌ β π β§ π
β Ring β§ π β (Baseβπ
)) β π β (Baseβπ
)) |
12 | | snidg 4662 |
. . . 4
β’ (πΌ β π β πΌ β {πΌ}) |
13 | 12 | 3ad2ant1 1133 |
. . 3
β’ ((πΌ β π β§ π
β Ring β§ π β (Baseβπ
)) β πΌ β {πΌ}) |
14 | 9, 10, 11, 13, 13 | ovmpod 7562 |
. 2
β’ ((πΌ β π β§ π
β Ring β§ π β (Baseβπ
)) β (π( Β·π
βπ)πΌ) = πΌ) |
15 | | snex 5431 |
. . . . . . 7
β’
{β¨β¨πΌ,
πΌβ©, πΌβ©} β V |
16 | 6 | lmodplusg 17274 |
. . . . . . 7
β’
({β¨β¨πΌ,
πΌβ©, πΌβ©} β V β {β¨β¨πΌ, πΌβ©, πΌβ©} = (+gβπ)) |
17 | 15, 16 | mp1i 13 |
. . . . . 6
β’ ((πΌ β π β§ π
β Ring β§ π β (Baseβπ
)) β {β¨β¨πΌ, πΌβ©, πΌβ©} = (+gβπ)) |
18 | 17 | eqcomd 2738 |
. . . . 5
β’ ((πΌ β π β§ π
β Ring β§ π β (Baseβπ
)) β (+gβπ) = {β¨β¨πΌ, πΌβ©, πΌβ©}) |
19 | 18 | oveqd 7428 |
. . . 4
β’ ((πΌ β π β§ π
β Ring β§ π β (Baseβπ
)) β (πΌ(+gβπ)πΌ) = (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ)) |
20 | | df-ov 7414 |
. . . . 5
β’ (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = ({β¨β¨πΌ, πΌβ©, πΌβ©}ββ¨πΌ, πΌβ©) |
21 | | opex 5464 |
. . . . . 6
β’
β¨πΌ, πΌβ© β V |
22 | | simp1 1136 |
. . . . . 6
β’ ((πΌ β π β§ π
β Ring β§ π β (Baseβπ
)) β πΌ β π) |
23 | | fvsng 7180 |
. . . . . 6
β’
((β¨πΌ, πΌβ© β V β§ πΌ β π) β ({β¨β¨πΌ, πΌβ©, πΌβ©}ββ¨πΌ, πΌβ©) = πΌ) |
24 | 21, 22, 23 | sylancr 587 |
. . . . 5
β’ ((πΌ β π β§ π
β Ring β§ π β (Baseβπ
)) β ({β¨β¨πΌ, πΌβ©, πΌβ©}ββ¨πΌ, πΌβ©) = πΌ) |
25 | 20, 24 | eqtrid 2784 |
. . . 4
β’ ((πΌ β π β§ π
β Ring β§ π β (Baseβπ
)) β (πΌ{β¨β¨πΌ, πΌβ©, πΌβ©}πΌ) = πΌ) |
26 | 19, 25 | eqtrd 2772 |
. . 3
β’ ((πΌ β π β§ π
β Ring β§ π β (Baseβπ
)) β (πΌ(+gβπ)πΌ) = πΌ) |
27 | 26 | oveq2d 7427 |
. 2
β’ ((πΌ β π β§ π
β Ring β§ π β (Baseβπ
)) β (π( Β·π
βπ)(πΌ(+gβπ)πΌ)) = (π( Β·π
βπ)πΌ)) |
28 | 2 | a1i 11 |
. . . . . . . 8
β’ ((πΌ β π β§ π
β Ring β§ π β (Baseβπ
)) β {πΌ} β V) |
29 | 1, 28, 4 | sylancr 587 |
. . . . . . 7
β’ ((πΌ β π β§ π
β Ring β§ π β (Baseβπ
)) β (π₯ β (Baseβπ
), π¦ β {πΌ} β¦ π¦) β V) |
30 | 29, 7 | syl 17 |
. . . . . 6
β’ ((πΌ β π β§ π
β Ring β§ π β (Baseβπ
)) β (π₯ β (Baseβπ
), π¦ β {πΌ} β¦ π¦) = ( Β·π
βπ)) |
31 | 30 | eqcomd 2738 |
. . . . 5
β’ ((πΌ β π β§ π
β Ring β§ π β (Baseβπ
)) β (
Β·π βπ) = (π₯ β (Baseβπ
), π¦ β {πΌ} β¦ π¦)) |
32 | 31, 10, 11, 13, 13 | ovmpod 7562 |
. . . 4
β’ ((πΌ β π β§ π
β Ring β§ π β (Baseβπ
)) β (π( Β·π
βπ)πΌ) = πΌ) |
33 | 32, 32 | oveq12d 7429 |
. . 3
β’ ((πΌ β π β§ π
β Ring β§ π β (Baseβπ
)) β ((π( Β·π
βπ)πΌ)(+gβπ)(π( Β·π
βπ)πΌ)) = (πΌ(+gβπ)πΌ)) |
34 | 33, 26 | eqtrd 2772 |
. 2
β’ ((πΌ β π β§ π
β Ring β§ π β (Baseβπ
)) β ((π( Β·π
βπ)πΌ)(+gβπ)(π( Β·π
βπ)πΌ)) = πΌ) |
35 | 14, 27, 34 | 3eqtr4d 2782 |
1
β’ ((πΌ β π β§ π
β Ring β§ π β (Baseβπ
)) β (π( Β·π
βπ)(πΌ(+gβπ)πΌ)) = ((π( Β·π
βπ)πΌ)(+gβπ)(π( Β·π
βπ)πΌ))) |