Step | Hyp | Ref
| Expression |
1 | | lmod1zr.m |
. . 3
β’ π = ({β¨(Baseβndx),
{πΌ}β©,
β¨(+gβndx), {β¨β¨πΌ, πΌβ©, πΌβ©}β©, β¨(Scalarβndx),
π
β©} βͺ {β¨(
Β·π βndx), {β¨β¨π, πΌβ©, πΌβ©}β©}) |
2 | | elsni 4645 |
. . . . . . . . . . 11
β’ (π β {β¨π, πΌβ©} β π = β¨π, πΌβ©) |
3 | | fveq2 6891 |
. . . . . . . . . . . . 13
β’ (π = β¨π, πΌβ© β (2nd βπ) = (2nd
ββ¨π, πΌβ©)) |
4 | 3 | adantl 481 |
. . . . . . . . . . . 12
β’ (((πΌ β π β§ π β π) β§ π = β¨π, πΌβ©) β (2nd βπ) = (2nd
ββ¨π, πΌβ©)) |
5 | | op2ndg 7991 |
. . . . . . . . . . . . . . 15
β’ ((π β π β§ πΌ β π) β (2nd ββ¨π, πΌβ©) = πΌ) |
6 | 5 | ancoms 458 |
. . . . . . . . . . . . . 14
β’ ((πΌ β π β§ π β π) β (2nd ββ¨π, πΌβ©) = πΌ) |
7 | | snidg 4662 |
. . . . . . . . . . . . . . 15
β’ (πΌ β π β πΌ β {πΌ}) |
8 | 7 | adantr 480 |
. . . . . . . . . . . . . 14
β’ ((πΌ β π β§ π β π) β πΌ β {πΌ}) |
9 | 6, 8 | eqeltrd 2832 |
. . . . . . . . . . . . 13
β’ ((πΌ β π β§ π β π) β (2nd ββ¨π, πΌβ©) β {πΌ}) |
10 | 9 | adantr 480 |
. . . . . . . . . . . 12
β’ (((πΌ β π β§ π β π) β§ π = β¨π, πΌβ©) β (2nd
ββ¨π, πΌβ©) β {πΌ}) |
11 | 4, 10 | eqeltrd 2832 |
. . . . . . . . . . 11
β’ (((πΌ β π β§ π β π) β§ π = β¨π, πΌβ©) β (2nd βπ) β {πΌ}) |
12 | 2, 11 | sylan2 592 |
. . . . . . . . . 10
β’ (((πΌ β π β§ π β π) β§ π β {β¨π, πΌβ©}) β (2nd βπ) β {πΌ}) |
13 | 12 | fmpttd 7116 |
. . . . . . . . 9
β’ ((πΌ β π β§ π β π) β (π β {β¨π, πΌβ©} β¦ (2nd βπ)):{β¨π, πΌβ©}βΆ{πΌ}) |
14 | | opex 5464 |
. . . . . . . . . 10
β’
β¨π, πΌβ© β V |
15 | | simpl 482 |
. . . . . . . . . 10
β’ ((πΌ β π β§ π β π) β πΌ β π) |
16 | | fsng 7137 |
. . . . . . . . . 10
β’
((β¨π, πΌβ© β V β§ πΌ β π) β ((π β {β¨π, πΌβ©} β¦ (2nd βπ)):{β¨π, πΌβ©}βΆ{πΌ} β (π β {β¨π, πΌβ©} β¦ (2nd βπ)) = {β¨β¨π, πΌβ©, πΌβ©})) |
17 | 14, 15, 16 | sylancr 586 |
. . . . . . . . 9
β’ ((πΌ β π β§ π β π) β ((π β {β¨π, πΌβ©} β¦ (2nd βπ)):{β¨π, πΌβ©}βΆ{πΌ} β (π β {β¨π, πΌβ©} β¦ (2nd βπ)) = {β¨β¨π, πΌβ©, πΌβ©})) |
18 | 13, 17 | mpbid 231 |
. . . . . . . 8
β’ ((πΌ β π β§ π β π) β (π β {β¨π, πΌβ©} β¦ (2nd βπ)) = {β¨β¨π, πΌβ©, πΌβ©}) |
19 | | xpsng 7139 |
. . . . . . . . . . 11
β’ ((π β π β§ πΌ β π) β ({π} Γ {πΌ}) = {β¨π, πΌβ©}) |
20 | 19 | ancoms 458 |
. . . . . . . . . 10
β’ ((πΌ β π β§ π β π) β ({π} Γ {πΌ}) = {β¨π, πΌβ©}) |
21 | 20 | eqcomd 2737 |
. . . . . . . . 9
β’ ((πΌ β π β§ π β π) β {β¨π, πΌβ©} = ({π} Γ {πΌ})) |
22 | 21 | mpteq1d 5243 |
. . . . . . . 8
β’ ((πΌ β π β§ π β π) β (π β {β¨π, πΌβ©} β¦ (2nd βπ)) = (π β ({π} Γ {πΌ}) β¦ (2nd βπ))) |
23 | 18, 22 | eqtr3d 2773 |
. . . . . . 7
β’ ((πΌ β π β§ π β π) β {β¨β¨π, πΌβ©, πΌβ©} = (π β ({π} Γ {πΌ}) β¦ (2nd βπ))) |
24 | | vex 3477 |
. . . . . . . . . 10
β’ π§ β V |
25 | | vex 3477 |
. . . . . . . . . 10
β’ π β V |
26 | 24, 25 | op2ndd 7989 |
. . . . . . . . 9
β’ (π = β¨π§, πβ© β (2nd βπ) = π) |
27 | 26 | mpompt 7525 |
. . . . . . . 8
β’ (π β ({π} Γ {πΌ}) β¦ (2nd βπ)) = (π§ β {π}, π β {πΌ} β¦ π) |
28 | 27 | a1i 11 |
. . . . . . 7
β’ ((πΌ β π β§ π β π) β (π β ({π} Γ {πΌ}) β¦ (2nd βπ)) = (π§ β {π}, π β {πΌ} β¦ π)) |
29 | | snex 5431 |
. . . . . . . . 9
β’ {π} β V |
30 | | lmod1zr.r |
. . . . . . . . . 10
β’ π
= {β¨(Baseβndx),
{π}β©,
β¨(+gβndx), {β¨β¨π, πβ©, πβ©}β©,
β¨(.rβndx), {β¨β¨π, πβ©, πβ©}β©} |
31 | 30 | rngbase 17249 |
. . . . . . . . 9
β’ ({π} β V β {π} = (Baseβπ
)) |
32 | 29, 31 | mp1i 13 |
. . . . . . . 8
β’ ((πΌ β π β§ π β π) β {π} = (Baseβπ
)) |
33 | | eqidd 2732 |
. . . . . . . 8
β’ ((πΌ β π β§ π β π) β {πΌ} = {πΌ}) |
34 | | mpoeq12 7485 |
. . . . . . . 8
β’ (({π} = (Baseβπ
) β§ {πΌ} = {πΌ}) β (π§ β {π}, π β {πΌ} β¦ π) = (π§ β (Baseβπ
), π β {πΌ} β¦ π)) |
35 | 32, 33, 34 | syl2anc 583 |
. . . . . . 7
β’ ((πΌ β π β§ π β π) β (π§ β {π}, π β {πΌ} β¦ π) = (π§ β (Baseβπ
), π β {πΌ} β¦ π)) |
36 | 23, 28, 35 | 3eqtrd 2775 |
. . . . . 6
β’ ((πΌ β π β§ π β π) β {β¨β¨π, πΌβ©, πΌβ©} = (π§ β (Baseβπ
), π β {πΌ} β¦ π)) |
37 | 36 | opeq2d 4880 |
. . . . 5
β’ ((πΌ β π β§ π β π) β β¨(
Β·π βndx), {β¨β¨π, πΌβ©, πΌβ©}β© = β¨(
Β·π βndx), (π§ β (Baseβπ
), π β {πΌ} β¦ π)β©) |
38 | 37 | sneqd 4640 |
. . . 4
β’ ((πΌ β π β§ π β π) β {β¨(
Β·π βndx), {β¨β¨π, πΌβ©, πΌβ©}β©} = {β¨(
Β·π βndx), (π§ β (Baseβπ
), π β {πΌ} β¦ π)β©}) |
39 | 38 | uneq2d 4163 |
. . 3
β’ ((πΌ β π β§ π β π) β ({β¨(Baseβndx), {πΌ}β©,
β¨(+gβndx), {β¨β¨πΌ, πΌβ©, πΌβ©}β©, β¨(Scalarβndx),
π
β©} βͺ {β¨(
Β·π βndx), {β¨β¨π, πΌβ©, πΌβ©}β©}) = ({β¨(Baseβndx),
{πΌ}β©,
β¨(+gβndx), {β¨β¨πΌ, πΌβ©, πΌβ©}β©, β¨(Scalarβndx),
π
β©} βͺ {β¨(
Β·π βndx), (π§ β (Baseβπ
), π β {πΌ} β¦ π)β©})) |
40 | 1, 39 | eqtrid 2783 |
. 2
β’ ((πΌ β π β§ π β π) β π = ({β¨(Baseβndx), {πΌ}β©,
β¨(+gβndx), {β¨β¨πΌ, πΌβ©, πΌβ©}β©, β¨(Scalarβndx),
π
β©} βͺ {β¨(
Β·π βndx), (π§ β (Baseβπ
), π β {πΌ} β¦ π)β©})) |
41 | 30 | ring1 20199 |
. . 3
β’ (π β π β π
β Ring) |
42 | | eqidd 2732 |
. . . . . . . 8
β’ (π§ = π β π = π) |
43 | | id 22 |
. . . . . . . 8
β’ (π = π β π = π) |
44 | 42, 43 | cbvmpov 7507 |
. . . . . . 7
β’ (π§ β (Baseβπ
), π β {πΌ} β¦ π) = (π β (Baseβπ
), π β {πΌ} β¦ π) |
45 | 44 | opeq2i 4877 |
. . . . . 6
β’ β¨(
Β·π βndx), (π§ β (Baseβπ
), π β {πΌ} β¦ π)β© = β¨(
Β·π βndx), (π β (Baseβπ
), π β {πΌ} β¦ π)β© |
46 | 45 | sneqi 4639 |
. . . . 5
β’ {β¨(
Β·π βndx), (π§ β (Baseβπ
), π β {πΌ} β¦ π)β©} = {β¨(
Β·π βndx), (π β (Baseβπ
), π β {πΌ} β¦ π)β©} |
47 | 46 | uneq2i 4160 |
. . . 4
β’
({β¨(Baseβndx), {πΌ}β©, β¨(+gβndx),
{β¨β¨πΌ, πΌβ©, πΌβ©}β©, β¨(Scalarβndx),
π
β©} βͺ {β¨(
Β·π βndx), (π§ β (Baseβπ
), π β {πΌ} β¦ π)β©}) = ({β¨(Baseβndx), {πΌ}β©,
β¨(+gβndx), {β¨β¨πΌ, πΌβ©, πΌβ©}β©, β¨(Scalarβndx),
π
β©} βͺ {β¨(
Β·π βndx), (π β (Baseβπ
), π β {πΌ} β¦ π)β©}) |
48 | 47 | lmod1 47261 |
. . 3
β’ ((πΌ β π β§ π
β Ring) β
({β¨(Baseβndx), {πΌ}β©, β¨(+gβndx),
{β¨β¨πΌ, πΌβ©, πΌβ©}β©, β¨(Scalarβndx),
π
β©} βͺ {β¨(
Β·π βndx), (π§ β (Baseβπ
), π β {πΌ} β¦ π)β©}) β LMod) |
49 | 41, 48 | sylan2 592 |
. 2
β’ ((πΌ β π β§ π β π) β ({β¨(Baseβndx), {πΌ}β©,
β¨(+gβndx), {β¨β¨πΌ, πΌβ©, πΌβ©}β©, β¨(Scalarβndx),
π
β©} βͺ {β¨(
Β·π βndx), (π§ β (Baseβπ
), π β {πΌ} β¦ π)β©}) β LMod) |
50 | 40, 49 | eqeltrd 2832 |
1
β’ ((πΌ β π β§ π β π) β π β LMod) |