Step | Hyp | Ref
| Expression |
1 | | eqid 2736 |
. . . 4
β’
(β€ring freeLMod {0, 1}) = (β€ring
freeLMod {0, 1}) |
2 | 1 | zlmodzxzlmod 45747 |
. . 3
β’
((β€ring freeLMod {0, 1}) β LMod β§
β€ring = (Scalarβ(β€ring freeLMod {0,
1}))) |
3 | 2 | simpli 485 |
. 2
β’
(β€ring freeLMod {0, 1}) β LMod |
4 | | 3z 12395 |
. . . . 5
β’ 3 β
β€ |
5 | | 6nn 12104 |
. . . . . 6
β’ 6 β
β |
6 | 5 | nnzi 12386 |
. . . . 5
β’ 6 β
β€ |
7 | 1 | zlmodzxzel 45748 |
. . . . 5
β’ ((3
β β€ β§ 6 β β€) β {β¨0, 3β©, β¨1,
6β©} β (Baseβ(β€ring freeLMod {0,
1}))) |
8 | 4, 6, 7 | mp2an 690 |
. . . 4
β’ {β¨0,
3β©, β¨1, 6β©} β (Baseβ(β€ring freeLMod
{0, 1})) |
9 | | 2z 12394 |
. . . . 5
β’ 2 β
β€ |
10 | | 4z 12396 |
. . . . 5
β’ 4 β
β€ |
11 | 1 | zlmodzxzel 45748 |
. . . . 5
β’ ((2
β β€ β§ 4 β β€) β {β¨0, 2β©, β¨1,
4β©} β (Baseβ(β€ring freeLMod {0,
1}))) |
12 | 9, 10, 11 | mp2an 690 |
. . . 4
β’ {β¨0,
2β©, β¨1, 4β©} β (Baseβ(β€ring freeLMod
{0, 1})) |
13 | | prelpwi 5372 |
. . . 4
β’
(({β¨0, 3β©, β¨1, 6β©} β
(Baseβ(β€ring freeLMod {0, 1})) β§ {β¨0, 2β©,
β¨1, 4β©} β (Baseβ(β€ring freeLMod {0, 1})))
β {{β¨0, 3β©, β¨1, 6β©}, {β¨0, 2β©, β¨1,
4β©}} β π« (Baseβ(β€ring freeLMod {0,
1}))) |
14 | 8, 12, 13 | mp2an 690 |
. . 3
β’
{{β¨0, 3β©, β¨1, 6β©}, {β¨0, 2β©, β¨1,
4β©}} β π« (Baseβ(β€ring freeLMod {0,
1})) |
15 | | eqid 2736 |
. . . . 5
β’ {β¨0,
3β©, β¨1, 6β©} = {β¨0, 3β©, β¨1,
6β©} |
16 | | eqid 2736 |
. . . . 5
β’ {β¨0,
2β©, β¨1, 4β©} = {β¨0, 2β©, β¨1,
4β©} |
17 | 1, 15, 16 | zlmodzxzldep 45902 |
. . . 4
β’
{{β¨0, 3β©, β¨1, 6β©}, {β¨0, 2β©, β¨1,
4β©}} linDepS (β€ring freeLMod {0, 1}) |
18 | 1, 15, 16 | ldepsnlinclem1 45903 |
. . . . . . . 8
β’ (π β
((Baseββ€ring) βm {{β¨0, 2β©,
β¨1, 4β©}}) β (π( linC β(β€ring
freeLMod {0, 1})){{β¨0, 2β©, β¨1, 4β©}}) β {β¨0,
3β©, β¨1, 6β©}) |
19 | | simpr 486 |
. . . . . . . . . . . 12
β’
(((β€ring freeLMod {0, 1}) β LMod β§
β€ring = (Scalarβ(β€ring freeLMod {0,
1}))) β β€ring = (Scalarβ(β€ring
freeLMod {0, 1}))) |
20 | 19 | eqcomd 2742 |
. . . . . . . . . . 11
β’
(((β€ring freeLMod {0, 1}) β LMod β§
β€ring = (Scalarβ(β€ring freeLMod {0,
1}))) β (Scalarβ(β€ring freeLMod {0, 1})) =
β€ring) |
21 | 2, 20 | ax-mp 5 |
. . . . . . . . . 10
β’
(Scalarβ(β€ring freeLMod {0, 1})) =
β€ring |
22 | 21 | fveq2i 6803 |
. . . . . . . . 9
β’
(Baseβ(Scalarβ(β€ring freeLMod {0, 1}))) =
(Baseββ€ring) |
23 | 22 | oveq1i 7313 |
. . . . . . . 8
β’
((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm {{β¨0, 2β©, β¨1, 4β©}}) =
((Baseββ€ring) βm {{β¨0, 2β©,
β¨1, 4β©}}) |
24 | 18, 23 | eleq2s 2855 |
. . . . . . 7
β’ (π β
((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm {{β¨0, 2β©, β¨1, 4β©}}) β (π( linC
β(β€ring freeLMod {0, 1})){{β¨0, 2β©, β¨1,
4β©}}) β {β¨0, 3β©, β¨1, 6β©}) |
25 | 24 | a1d 25 |
. . . . . 6
β’ (π β
((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm {{β¨0, 2β©, β¨1, 4β©}}) β (π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0, 1})))
β (π( linC
β(β€ring freeLMod {0, 1})){{β¨0, 2β©, β¨1,
4β©}}) β {β¨0, 3β©, β¨1, 6β©})) |
26 | 25 | rgen 3064 |
. . . . 5
β’
βπ β
((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm {{β¨0, 2β©, β¨1, 4β©}})(π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0, 1})))
β (π( linC
β(β€ring freeLMod {0, 1})){{β¨0, 2β©, β¨1,
4β©}}) β {β¨0, 3β©, β¨1, 6β©}) |
27 | 1, 15, 16 | ldepsnlinclem2 45904 |
. . . . . . . 8
β’ (π β
((Baseββ€ring) βm {{β¨0, 3β©,
β¨1, 6β©}}) β (π( linC β(β€ring
freeLMod {0, 1})){{β¨0, 3β©, β¨1, 6β©}}) β {β¨0,
2β©, β¨1, 4β©}) |
28 | 22 | oveq1i 7313 |
. . . . . . . 8
β’
((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm {{β¨0, 3β©, β¨1, 6β©}}) =
((Baseββ€ring) βm {{β¨0, 3β©,
β¨1, 6β©}}) |
29 | 27, 28 | eleq2s 2855 |
. . . . . . 7
β’ (π β
((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm {{β¨0, 3β©, β¨1, 6β©}}) β (π( linC
β(β€ring freeLMod {0, 1})){{β¨0, 3β©, β¨1,
6β©}}) β {β¨0, 2β©, β¨1, 4β©}) |
30 | 29 | a1d 25 |
. . . . . 6
β’ (π β
((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm {{β¨0, 3β©, β¨1, 6β©}}) β (π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0, 1})))
β (π( linC
β(β€ring freeLMod {0, 1})){{β¨0, 3β©, β¨1,
6β©}}) β {β¨0, 2β©, β¨1, 4β©})) |
31 | 30 | rgen 3064 |
. . . . 5
β’
βπ β
((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm {{β¨0, 3β©, β¨1, 6β©}})(π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0, 1})))
β (π( linC
β(β€ring freeLMod {0, 1})){{β¨0, 3β©, β¨1,
6β©}}) β {β¨0, 2β©, β¨1, 4β©}) |
32 | | prex 5364 |
. . . . . 6
β’ {β¨0,
3β©, β¨1, 6β©} β V |
33 | | prex 5364 |
. . . . . 6
β’ {β¨0,
2β©, β¨1, 4β©} β V |
34 | | sneq 4575 |
. . . . . . . . . 10
β’ (π£ = {β¨0, 3β©, β¨1,
6β©} β {π£} =
{{β¨0, 3β©, β¨1, 6β©}}) |
35 | 34 | difeq2d 4063 |
. . . . . . . . 9
β’ (π£ = {β¨0, 3β©, β¨1,
6β©} β ({{β¨0, 3β©, β¨1, 6β©}, {β¨0, 2β©,
β¨1, 4β©}} β {π£}) = ({{β¨0, 3β©, β¨1, 6β©},
{β¨0, 2β©, β¨1, 4β©}} β {{β¨0, 3β©, β¨1,
6β©}})) |
36 | 1, 15, 16 | zlmodzxzldeplem 45896 |
. . . . . . . . . 10
β’ {β¨0,
3β©, β¨1, 6β©} β {β¨0, 2β©, β¨1,
4β©} |
37 | | difprsn1 4739 |
. . . . . . . . . 10
β’
({β¨0, 3β©, β¨1, 6β©} β {β¨0, 2β©, β¨1,
4β©} β ({{β¨0, 3β©, β¨1, 6β©}, {β¨0, 2β©,
β¨1, 4β©}} β {{β¨0, 3β©, β¨1, 6β©}}) = {{β¨0,
2β©, β¨1, 4β©}}) |
38 | 36, 37 | ax-mp 5 |
. . . . . . . . 9
β’
({{β¨0, 3β©, β¨1, 6β©}, {β¨0, 2β©, β¨1,
4β©}} β {{β¨0, 3β©, β¨1, 6β©}}) = {{β¨0, 2β©,
β¨1, 4β©}} |
39 | 35, 38 | eqtrdi 2792 |
. . . . . . . 8
β’ (π£ = {β¨0, 3β©, β¨1,
6β©} β ({{β¨0, 3β©, β¨1, 6β©}, {β¨0, 2β©,
β¨1, 4β©}} β {π£}) = {{β¨0, 2β©, β¨1,
4β©}}) |
40 | 39 | oveq2d 7319 |
. . . . . . 7
β’ (π£ = {β¨0, 3β©, β¨1,
6β©} β ((Baseβ(Scalarβ(β€ring freeLMod {0,
1}))) βm ({{β¨0, 3β©, β¨1, 6β©}, {β¨0,
2β©, β¨1, 4β©}} β {π£})) =
((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm {{β¨0, 2β©, β¨1, 4β©}})) |
41 | 39 | oveq2d 7319 |
. . . . . . . . 9
β’ (π£ = {β¨0, 3β©, β¨1,
6β©} β (π( linC
β(β€ring freeLMod {0, 1}))({{β¨0, 3β©, β¨1,
6β©}, {β¨0, 2β©, β¨1, 4β©}} β {π£})) = (π( linC β(β€ring
freeLMod {0, 1})){{β¨0, 2β©, β¨1, 4β©}})) |
42 | | id 22 |
. . . . . . . . 9
β’ (π£ = {β¨0, 3β©, β¨1,
6β©} β π£ =
{β¨0, 3β©, β¨1, 6β©}) |
43 | 41, 42 | neeq12d 3003 |
. . . . . . . 8
β’ (π£ = {β¨0, 3β©, β¨1,
6β©} β ((π( linC
β(β€ring freeLMod {0, 1}))({{β¨0, 3β©, β¨1,
6β©}, {β¨0, 2β©, β¨1, 4β©}} β {π£})) β π£ β (π( linC β(β€ring
freeLMod {0, 1})){{β¨0, 2β©, β¨1, 4β©}}) β {β¨0,
3β©, β¨1, 6β©})) |
44 | 43 | imbi2d 342 |
. . . . . . 7
β’ (π£ = {β¨0, 3β©, β¨1,
6β©} β ((π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0, 1})))
β (π( linC
β(β€ring freeLMod {0, 1}))({{β¨0, 3β©, β¨1,
6β©}, {β¨0, 2β©, β¨1, 4β©}} β {π£})) β π£) β (π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0, 1})))
β (π( linC
β(β€ring freeLMod {0, 1})){{β¨0, 2β©, β¨1,
4β©}}) β {β¨0, 3β©, β¨1, 6β©}))) |
45 | 40, 44 | raleqbidv 3348 |
. . . . . 6
β’ (π£ = {β¨0, 3β©, β¨1,
6β©} β (βπ
β ((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm ({{β¨0, 3β©, β¨1, 6β©}, {β¨0, 2β©,
β¨1, 4β©}} β {π£}))(π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0, 1})))
β (π( linC
β(β€ring freeLMod {0, 1}))({{β¨0, 3β©, β¨1,
6β©}, {β¨0, 2β©, β¨1, 4β©}} β {π£})) β π£) β βπ β
((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm {{β¨0, 2β©, β¨1, 4β©}})(π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0, 1})))
β (π( linC
β(β€ring freeLMod {0, 1})){{β¨0, 2β©, β¨1,
4β©}}) β {β¨0, 3β©, β¨1, 6β©}))) |
46 | | sneq 4575 |
. . . . . . . . . 10
β’ (π£ = {β¨0, 2β©, β¨1,
4β©} β {π£} =
{{β¨0, 2β©, β¨1, 4β©}}) |
47 | 46 | difeq2d 4063 |
. . . . . . . . 9
β’ (π£ = {β¨0, 2β©, β¨1,
4β©} β ({{β¨0, 3β©, β¨1, 6β©}, {β¨0, 2β©,
β¨1, 4β©}} β {π£}) = ({{β¨0, 3β©, β¨1, 6β©},
{β¨0, 2β©, β¨1, 4β©}} β {{β¨0, 2β©, β¨1,
4β©}})) |
48 | | difprsn2 4740 |
. . . . . . . . . 10
β’
({β¨0, 3β©, β¨1, 6β©} β {β¨0, 2β©, β¨1,
4β©} β ({{β¨0, 3β©, β¨1, 6β©}, {β¨0, 2β©,
β¨1, 4β©}} β {{β¨0, 2β©, β¨1, 4β©}}) = {{β¨0,
3β©, β¨1, 6β©}}) |
49 | 36, 48 | ax-mp 5 |
. . . . . . . . 9
β’
({{β¨0, 3β©, β¨1, 6β©}, {β¨0, 2β©, β¨1,
4β©}} β {{β¨0, 2β©, β¨1, 4β©}}) = {{β¨0, 3β©,
β¨1, 6β©}} |
50 | 47, 49 | eqtrdi 2792 |
. . . . . . . 8
β’ (π£ = {β¨0, 2β©, β¨1,
4β©} β ({{β¨0, 3β©, β¨1, 6β©}, {β¨0, 2β©,
β¨1, 4β©}} β {π£}) = {{β¨0, 3β©, β¨1,
6β©}}) |
51 | 50 | oveq2d 7319 |
. . . . . . 7
β’ (π£ = {β¨0, 2β©, β¨1,
4β©} β ((Baseβ(Scalarβ(β€ring freeLMod {0,
1}))) βm ({{β¨0, 3β©, β¨1, 6β©}, {β¨0,
2β©, β¨1, 4β©}} β {π£})) =
((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm {{β¨0, 3β©, β¨1, 6β©}})) |
52 | 50 | oveq2d 7319 |
. . . . . . . . 9
β’ (π£ = {β¨0, 2β©, β¨1,
4β©} β (π( linC
β(β€ring freeLMod {0, 1}))({{β¨0, 3β©, β¨1,
6β©}, {β¨0, 2β©, β¨1, 4β©}} β {π£})) = (π( linC β(β€ring
freeLMod {0, 1})){{β¨0, 3β©, β¨1, 6β©}})) |
53 | | id 22 |
. . . . . . . . 9
β’ (π£ = {β¨0, 2β©, β¨1,
4β©} β π£ =
{β¨0, 2β©, β¨1, 4β©}) |
54 | 52, 53 | neeq12d 3003 |
. . . . . . . 8
β’ (π£ = {β¨0, 2β©, β¨1,
4β©} β ((π( linC
β(β€ring freeLMod {0, 1}))({{β¨0, 3β©, β¨1,
6β©}, {β¨0, 2β©, β¨1, 4β©}} β {π£})) β π£ β (π( linC β(β€ring
freeLMod {0, 1})){{β¨0, 3β©, β¨1, 6β©}}) β {β¨0,
2β©, β¨1, 4β©})) |
55 | 54 | imbi2d 342 |
. . . . . . 7
β’ (π£ = {β¨0, 2β©, β¨1,
4β©} β ((π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0, 1})))
β (π( linC
β(β€ring freeLMod {0, 1}))({{β¨0, 3β©, β¨1,
6β©}, {β¨0, 2β©, β¨1, 4β©}} β {π£})) β π£) β (π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0, 1})))
β (π( linC
β(β€ring freeLMod {0, 1})){{β¨0, 3β©, β¨1,
6β©}}) β {β¨0, 2β©, β¨1, 4β©}))) |
56 | 51, 55 | raleqbidv 3348 |
. . . . . 6
β’ (π£ = {β¨0, 2β©, β¨1,
4β©} β (βπ
β ((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm ({{β¨0, 3β©, β¨1, 6β©}, {β¨0, 2β©,
β¨1, 4β©}} β {π£}))(π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0, 1})))
β (π( linC
β(β€ring freeLMod {0, 1}))({{β¨0, 3β©, β¨1,
6β©}, {β¨0, 2β©, β¨1, 4β©}} β {π£})) β π£) β βπ β
((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm {{β¨0, 3β©, β¨1, 6β©}})(π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0, 1})))
β (π( linC
β(β€ring freeLMod {0, 1})){{β¨0, 3β©, β¨1,
6β©}}) β {β¨0, 2β©, β¨1, 4β©}))) |
57 | 32, 33, 45, 56 | ralpr 4640 |
. . . . 5
β’
(βπ£ β
{{β¨0, 3β©, β¨1, 6β©}, {β¨0, 2β©, β¨1,
4β©}}βπ β
((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm ({{β¨0, 3β©, β¨1, 6β©}, {β¨0, 2β©,
β¨1, 4β©}} β {π£}))(π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0, 1})))
β (π( linC
β(β€ring freeLMod {0, 1}))({{β¨0, 3β©, β¨1,
6β©}, {β¨0, 2β©, β¨1, 4β©}} β {π£})) β π£) β (βπ β
((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm {{β¨0, 2β©, β¨1, 4β©}})(π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0, 1})))
β (π( linC
β(β€ring freeLMod {0, 1})){{β¨0, 2β©, β¨1,
4β©}}) β {β¨0, 3β©, β¨1, 6β©}) β§ βπ β
((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm {{β¨0, 3β©, β¨1, 6β©}})(π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0, 1})))
β (π( linC
β(β€ring freeLMod {0, 1})){{β¨0, 3β©, β¨1,
6β©}}) β {β¨0, 2β©, β¨1, 4β©}))) |
58 | 26, 31, 57 | mpbir2an 709 |
. . . 4
β’
βπ£ β
{{β¨0, 3β©, β¨1, 6β©}, {β¨0, 2β©, β¨1,
4β©}}βπ β
((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm ({{β¨0, 3β©, β¨1, 6β©}, {β¨0, 2β©,
β¨1, 4β©}} β {π£}))(π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0, 1})))
β (π( linC
β(β€ring freeLMod {0, 1}))({{β¨0, 3β©, β¨1,
6β©}, {β¨0, 2β©, β¨1, 4β©}} β {π£})) β π£) |
59 | 17, 58 | pm3.2i 472 |
. . 3
β’
({{β¨0, 3β©, β¨1, 6β©}, {β¨0, 2β©, β¨1,
4β©}} linDepS (β€ring freeLMod {0, 1}) β§ βπ£ β {{β¨0, 3β©,
β¨1, 6β©}, {β¨0, 2β©, β¨1, 4β©}}βπ β
((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm ({{β¨0, 3β©, β¨1, 6β©}, {β¨0, 2β©,
β¨1, 4β©}} β {π£}))(π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0, 1})))
β (π( linC
β(β€ring freeLMod {0, 1}))({{β¨0, 3β©, β¨1,
6β©}, {β¨0, 2β©, β¨1, 4β©}} β {π£})) β π£)) |
60 | | breq1 5084 |
. . . . 5
β’ (π = {{β¨0, 3β©, β¨1,
6β©}, {β¨0, 2β©, β¨1, 4β©}} β (π linDepS (β€ring freeLMod {0,
1}) β {{β¨0, 3β©, β¨1, 6β©}, {β¨0, 2β©, β¨1,
4β©}} linDepS (β€ring freeLMod {0, 1}))) |
61 | | id 22 |
. . . . . 6
β’ (π = {{β¨0, 3β©, β¨1,
6β©}, {β¨0, 2β©, β¨1, 4β©}} β π = {{β¨0, 3β©, β¨1, 6β©},
{β¨0, 2β©, β¨1, 4β©}}) |
62 | | difeq1 4056 |
. . . . . . . 8
β’ (π = {{β¨0, 3β©, β¨1,
6β©}, {β¨0, 2β©, β¨1, 4β©}} β (π β {π£}) = ({{β¨0, 3β©, β¨1, 6β©},
{β¨0, 2β©, β¨1, 4β©}} β {π£})) |
63 | 62 | oveq2d 7319 |
. . . . . . 7
β’ (π = {{β¨0, 3β©, β¨1,
6β©}, {β¨0, 2β©, β¨1, 4β©}} β
((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm (π
β {π£})) =
((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm ({{β¨0, 3β©, β¨1, 6β©}, {β¨0, 2β©,
β¨1, 4β©}} β {π£}))) |
64 | 62 | oveq2d 7319 |
. . . . . . . . 9
β’ (π = {{β¨0, 3β©, β¨1,
6β©}, {β¨0, 2β©, β¨1, 4β©}} β (π( linC β(β€ring
freeLMod {0, 1}))(π β
{π£})) = (π( linC β(β€ring
freeLMod {0, 1}))({{β¨0, 3β©, β¨1, 6β©}, {β¨0, 2β©,
β¨1, 4β©}} β {π£}))) |
65 | 64 | neeq1d 3001 |
. . . . . . . 8
β’ (π = {{β¨0, 3β©, β¨1,
6β©}, {β¨0, 2β©, β¨1, 4β©}} β ((π( linC β(β€ring
freeLMod {0, 1}))(π β
{π£})) β π£ β (π( linC β(β€ring
freeLMod {0, 1}))({{β¨0, 3β©, β¨1, 6β©}, {β¨0, 2β©,
β¨1, 4β©}} β {π£})) β π£)) |
66 | 65 | imbi2d 342 |
. . . . . . 7
β’ (π = {{β¨0, 3β©, β¨1,
6β©}, {β¨0, 2β©, β¨1, 4β©}} β ((π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0, 1})))
β (π( linC
β(β€ring freeLMod {0, 1}))(π β {π£})) β π£) β (π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0, 1})))
β (π( linC
β(β€ring freeLMod {0, 1}))({{β¨0, 3β©, β¨1,
6β©}, {β¨0, 2β©, β¨1, 4β©}} β {π£})) β π£))) |
67 | 63, 66 | raleqbidv 3348 |
. . . . . 6
β’ (π = {{β¨0, 3β©, β¨1,
6β©}, {β¨0, 2β©, β¨1, 4β©}} β (βπ β
((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm (π
β {π£}))(π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0, 1})))
β (π( linC
β(β€ring freeLMod {0, 1}))(π β {π£})) β π£) β βπ β
((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm ({{β¨0, 3β©, β¨1, 6β©}, {β¨0, 2β©,
β¨1, 4β©}} β {π£}))(π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0, 1})))
β (π( linC
β(β€ring freeLMod {0, 1}))({{β¨0, 3β©, β¨1,
6β©}, {β¨0, 2β©, β¨1, 4β©}} β {π£})) β π£))) |
68 | 61, 67 | raleqbidv 3348 |
. . . . 5
β’ (π = {{β¨0, 3β©, β¨1,
6β©}, {β¨0, 2β©, β¨1, 4β©}} β (βπ£ β π βπ β
((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm (π
β {π£}))(π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0, 1})))
β (π( linC
β(β€ring freeLMod {0, 1}))(π β {π£})) β π£) β βπ£ β {{β¨0, 3β©, β¨1,
6β©}, {β¨0, 2β©, β¨1, 4β©}}βπ β
((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm ({{β¨0, 3β©, β¨1, 6β©}, {β¨0, 2β©,
β¨1, 4β©}} β {π£}))(π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0, 1})))
β (π( linC
β(β€ring freeLMod {0, 1}))({{β¨0, 3β©, β¨1,
6β©}, {β¨0, 2β©, β¨1, 4β©}} β {π£})) β π£))) |
69 | 60, 68 | anbi12d 632 |
. . . 4
β’ (π = {{β¨0, 3β©, β¨1,
6β©}, {β¨0, 2β©, β¨1, 4β©}} β ((π linDepS (β€ring freeLMod {0,
1}) β§ βπ£ β
π βπ β
((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm (π
β {π£}))(π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0, 1})))
β (π( linC
β(β€ring freeLMod {0, 1}))(π β {π£})) β π£)) β ({{β¨0, 3β©, β¨1,
6β©}, {β¨0, 2β©, β¨1, 4β©}} linDepS (β€ring
freeLMod {0, 1}) β§ βπ£ β {{β¨0, 3β©, β¨1,
6β©}, {β¨0, 2β©, β¨1, 4β©}}βπ β
((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm ({{β¨0, 3β©, β¨1, 6β©}, {β¨0, 2β©,
β¨1, 4β©}} β {π£}))(π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0, 1})))
β (π( linC
β(β€ring freeLMod {0, 1}))({{β¨0, 3β©, β¨1,
6β©}, {β¨0, 2β©, β¨1, 4β©}} β {π£})) β π£)))) |
70 | 69 | rspcev 3566 |
. . 3
β’
(({{β¨0, 3β©, β¨1, 6β©}, {β¨0, 2β©, β¨1,
4β©}} β π« (Baseβ(β€ring freeLMod {0,
1})) β§ ({{β¨0, 3β©, β¨1, 6β©}, {β¨0, 2β©, β¨1,
4β©}} linDepS (β€ring freeLMod {0, 1}) β§ βπ£ β {{β¨0, 3β©,
β¨1, 6β©}, {β¨0, 2β©, β¨1, 4β©}}βπ β
((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm ({{β¨0, 3β©, β¨1, 6β©}, {β¨0, 2β©,
β¨1, 4β©}} β {π£}))(π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0, 1})))
β (π( linC
β(β€ring freeLMod {0, 1}))({{β¨0, 3β©, β¨1,
6β©}, {β¨0, 2β©, β¨1, 4β©}} β {π£})) β π£))) β βπ β π«
(Baseβ(β€ring freeLMod {0, 1}))(π linDepS (β€ring freeLMod {0,
1}) β§ βπ£ β
π βπ β
((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm (π
β {π£}))(π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0, 1})))
β (π( linC
β(β€ring freeLMod {0, 1}))(π β {π£})) β π£))) |
71 | 14, 59, 70 | mp2an 690 |
. 2
β’
βπ β
π« (Baseβ(β€ring freeLMod {0, 1}))(π linDepS (β€ring
freeLMod {0, 1}) β§ βπ£ β π βπ β
((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm (π
β {π£}))(π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0, 1})))
β (π( linC
β(β€ring freeLMod {0, 1}))(π β {π£})) β π£)) |
72 | | fveq2 6800 |
. . . . 5
β’ (π = (β€ring
freeLMod {0, 1}) β (Baseβπ) = (Baseβ(β€ring
freeLMod {0, 1}))) |
73 | 72 | pweqd 4556 |
. . . 4
β’ (π = (β€ring
freeLMod {0, 1}) β π« (Baseβπ) = π«
(Baseβ(β€ring freeLMod {0, 1}))) |
74 | | breq2 5085 |
. . . . 5
β’ (π = (β€ring
freeLMod {0, 1}) β (π
linDepS π β π linDepS (β€ring
freeLMod {0, 1}))) |
75 | | 2fveq3 6805 |
. . . . . . . 8
β’ (π = (β€ring
freeLMod {0, 1}) β (Baseβ(Scalarβπ)) =
(Baseβ(Scalarβ(β€ring freeLMod {0,
1})))) |
76 | 75 | oveq1d 7318 |
. . . . . . 7
β’ (π = (β€ring
freeLMod {0, 1}) β ((Baseβ(Scalarβπ)) βm (π β {π£})) =
((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm (π
β {π£}))) |
77 | | 2fveq3 6805 |
. . . . . . . . 9
β’ (π = (β€ring
freeLMod {0, 1}) β (0gβ(Scalarβπ)) =
(0gβ(Scalarβ(β€ring freeLMod {0,
1})))) |
78 | 77 | breq2d 5093 |
. . . . . . . 8
β’ (π = (β€ring
freeLMod {0, 1}) β (π
finSupp (0gβ(Scalarβπ)) β π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0,
1}))))) |
79 | | fveq2 6800 |
. . . . . . . . . 10
β’ (π = (β€ring
freeLMod {0, 1}) β ( linC βπ) = ( linC β(β€ring
freeLMod {0, 1}))) |
80 | 79 | oveqd 7320 |
. . . . . . . . 9
β’ (π = (β€ring
freeLMod {0, 1}) β (π(
linC βπ)(π β {π£})) = (π( linC β(β€ring
freeLMod {0, 1}))(π β
{π£}))) |
81 | 80 | neeq1d 3001 |
. . . . . . . 8
β’ (π = (β€ring
freeLMod {0, 1}) β ((π( linC βπ)(π β {π£})) β π£ β (π( linC β(β€ring
freeLMod {0, 1}))(π β
{π£})) β π£)) |
82 | 78, 81 | imbi12d 346 |
. . . . . . 7
β’ (π = (β€ring
freeLMod {0, 1}) β ((π
finSupp (0gβ(Scalarβπ)) β (π( linC βπ)(π β {π£})) β π£) β (π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0, 1})))
β (π( linC
β(β€ring freeLMod {0, 1}))(π β {π£})) β π£))) |
83 | 76, 82 | raleqbidv 3348 |
. . . . . 6
β’ (π = (β€ring
freeLMod {0, 1}) β (βπ β ((Baseβ(Scalarβπ)) βm (π β {π£}))(π finSupp
(0gβ(Scalarβπ)) β (π( linC βπ)(π β {π£})) β π£) β βπ β
((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm (π
β {π£}))(π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0, 1})))
β (π( linC
β(β€ring freeLMod {0, 1}))(π β {π£})) β π£))) |
84 | 83 | ralbidv 3171 |
. . . . 5
β’ (π = (β€ring
freeLMod {0, 1}) β (βπ£ β π βπ β ((Baseβ(Scalarβπ)) βm (π β {π£}))(π finSupp
(0gβ(Scalarβπ)) β (π( linC βπ)(π β {π£})) β π£) β βπ£ β π βπ β
((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm (π
β {π£}))(π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0, 1})))
β (π( linC
β(β€ring freeLMod {0, 1}))(π β {π£})) β π£))) |
85 | 74, 84 | anbi12d 632 |
. . . 4
β’ (π = (β€ring
freeLMod {0, 1}) β ((π
linDepS π β§
βπ£ β π βπ β ((Baseβ(Scalarβπ)) βm (π β {π£}))(π finSupp
(0gβ(Scalarβπ)) β (π( linC βπ)(π β {π£})) β π£)) β (π linDepS (β€ring freeLMod {0,
1}) β§ βπ£ β
π βπ β
((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm (π
β {π£}))(π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0, 1})))
β (π( linC
β(β€ring freeLMod {0, 1}))(π β {π£})) β π£)))) |
86 | 73, 85 | rexeqbidv 3349 |
. . 3
β’ (π = (β€ring
freeLMod {0, 1}) β (βπ β π« (Baseβπ)(π linDepS π β§ βπ£ β π βπ β ((Baseβ(Scalarβπ)) βm (π β {π£}))(π finSupp
(0gβ(Scalarβπ)) β (π( linC βπ)(π β {π£})) β π£)) β βπ β π«
(Baseβ(β€ring freeLMod {0, 1}))(π linDepS (β€ring freeLMod {0,
1}) β§ βπ£ β
π βπ β
((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm (π
β {π£}))(π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0, 1})))
β (π( linC
β(β€ring freeLMod {0, 1}))(π β {π£})) β π£)))) |
87 | 86 | rspcev 3566 |
. 2
β’
(((β€ring freeLMod {0, 1}) β LMod β§
βπ β π«
(Baseβ(β€ring freeLMod {0, 1}))(π linDepS (β€ring freeLMod {0,
1}) β§ βπ£ β
π βπ β
((Baseβ(Scalarβ(β€ring freeLMod {0, 1})))
βm (π
β {π£}))(π finSupp
(0gβ(Scalarβ(β€ring freeLMod {0, 1})))
β (π( linC
β(β€ring freeLMod {0, 1}))(π β {π£})) β π£))) β βπ β LMod βπ β π« (Baseβπ)(π linDepS π β§ βπ£ β π βπ β ((Baseβ(Scalarβπ)) βm (π β {π£}))(π finSupp
(0gβ(Scalarβπ)) β (π( linC βπ)(π β {π£})) β π£))) |
88 | 3, 71, 87 | mp2an 690 |
1
β’
βπ β LMod
βπ β π«
(Baseβπ)(π linDepS π β§ βπ£ β π βπ β ((Baseβ(Scalarβπ)) βm (π β {π£}))(π finSupp
(0gβ(Scalarβπ)) β (π( linC βπ)(π β {π£})) β π£)) |