Step | Hyp | Ref
| Expression |
1 | | elmapi 8790 |
. 2
β’ (πΉ β
((Baseββ€ring) βm {π΄}) β πΉ:{π΄}βΆ(Baseββ€ring)) |
2 | | zlmodzxzldep.a |
. . . . 5
β’ π΄ = {β¨0, 3β©, β¨1,
6β©} |
3 | | prex 5390 |
. . . . 5
β’ {β¨0,
3β©, β¨1, 6β©} β V |
4 | 2, 3 | eqeltri 2830 |
. . . 4
β’ π΄ β V |
5 | 4 | fsn2 7083 |
. . 3
β’ (πΉ:{π΄}βΆ(Baseββ€ring)
β ((πΉβπ΄) β
(Baseββ€ring) β§ πΉ = {β¨π΄, (πΉβπ΄)β©})) |
6 | | oveq1 7365 |
. . . . . 6
β’ (πΉ = {β¨π΄, (πΉβπ΄)β©} β (πΉ( linC βπ){π΄}) = ({β¨π΄, (πΉβπ΄)β©} ( linC βπ){π΄})) |
7 | 6 | adantl 483 |
. . . . 5
β’ (((πΉβπ΄) β (Baseββ€ring)
β§ πΉ = {β¨π΄, (πΉβπ΄)β©}) β (πΉ( linC βπ){π΄}) = ({β¨π΄, (πΉβπ΄)β©} ( linC βπ){π΄})) |
8 | | zlmodzxzldep.z |
. . . . . . . . 9
β’ π = (β€ring
freeLMod {0, 1}) |
9 | 8 | zlmodzxzlmod 46516 |
. . . . . . . 8
β’ (π β LMod β§
β€ring = (Scalarβπ)) |
10 | 9 | simpli 485 |
. . . . . . 7
β’ π β LMod |
11 | 10 | a1i 11 |
. . . . . 6
β’ (((πΉβπ΄) β (Baseββ€ring)
β§ πΉ = {β¨π΄, (πΉβπ΄)β©}) β π β LMod) |
12 | | 3z 12541 |
. . . . . . . . 9
β’ 3 β
β€ |
13 | | 6nn 12247 |
. . . . . . . . . 10
β’ 6 β
β |
14 | 13 | nnzi 12532 |
. . . . . . . . 9
β’ 6 β
β€ |
15 | 8 | zlmodzxzel 46517 |
. . . . . . . . 9
β’ ((3
β β€ β§ 6 β β€) β {β¨0, 3β©, β¨1,
6β©} β (Baseβπ)) |
16 | 12, 14, 15 | mp2an 691 |
. . . . . . . 8
β’ {β¨0,
3β©, β¨1, 6β©} β (Baseβπ) |
17 | 2, 16 | eqeltri 2830 |
. . . . . . 7
β’ π΄ β (Baseβπ) |
18 | 17 | a1i 11 |
. . . . . 6
β’ (((πΉβπ΄) β (Baseββ€ring)
β§ πΉ = {β¨π΄, (πΉβπ΄)β©}) β π΄ β (Baseβπ)) |
19 | | simpl 484 |
. . . . . 6
β’ (((πΉβπ΄) β (Baseββ€ring)
β§ πΉ = {β¨π΄, (πΉβπ΄)β©}) β (πΉβπ΄) β
(Baseββ€ring)) |
20 | | eqid 2733 |
. . . . . . 7
β’
(Baseβπ) =
(Baseβπ) |
21 | 9 | simpri 487 |
. . . . . . 7
β’
β€ring = (Scalarβπ) |
22 | | eqid 2733 |
. . . . . . 7
β’
(Baseββ€ring) =
(Baseββ€ring) |
23 | | eqid 2733 |
. . . . . . 7
β’ (
Β·π βπ) = ( Β·π
βπ) |
24 | 20, 21, 22, 23 | lincvalsng 46583 |
. . . . . 6
β’ ((π β LMod β§ π΄ β (Baseβπ) β§ (πΉβπ΄) β
(Baseββ€ring)) β ({β¨π΄, (πΉβπ΄)β©} ( linC βπ){π΄}) = ((πΉβπ΄)( Β·π
βπ)π΄)) |
25 | 11, 18, 19, 24 | syl3anc 1372 |
. . . . 5
β’ (((πΉβπ΄) β (Baseββ€ring)
β§ πΉ = {β¨π΄, (πΉβπ΄)β©}) β ({β¨π΄, (πΉβπ΄)β©} ( linC βπ){π΄}) = ((πΉβπ΄)( Β·π
βπ)π΄)) |
26 | 7, 25 | eqtrd 2773 |
. . . 4
β’ (((πΉβπ΄) β (Baseββ€ring)
β§ πΉ = {β¨π΄, (πΉβπ΄)β©}) β (πΉ( linC βπ){π΄}) = ((πΉβπ΄)( Β·π
βπ)π΄)) |
27 | | eqid 2733 |
. . . . . 6
β’ {β¨0,
0β©, β¨1, 0β©} = {β¨0, 0β©, β¨1,
0β©} |
28 | | eqid 2733 |
. . . . . 6
β’
(-gβπ) = (-gβπ) |
29 | | zlmodzxzldep.b |
. . . . . 6
β’ π΅ = {β¨0, 2β©, β¨1,
4β©} |
30 | 8, 27, 23, 28, 2, 29 | zlmodzxznm 46664 |
. . . . 5
β’
βπ β
β€ ((π(
Β·π βπ)π΄) β π΅ β§ (π( Β·π
βπ)π΅) β π΄) |
31 | | r19.26 3111 |
. . . . . 6
β’
(βπ β
β€ ((π(
Β·π βπ)π΄) β π΅ β§ (π( Β·π
βπ)π΅) β π΄) β (βπ β β€ (π( Β·π
βπ)π΄) β π΅ β§ βπ β β€ (π( Β·π
βπ)π΅) β π΄)) |
32 | | oveq1 7365 |
. . . . . . . . . 10
β’ (π = (πΉβπ΄) β (π( Β·π
βπ)π΄) = ((πΉβπ΄)( Β·π
βπ)π΄)) |
33 | 32 | neeq1d 3000 |
. . . . . . . . 9
β’ (π = (πΉβπ΄) β ((π( Β·π
βπ)π΄) β π΅ β ((πΉβπ΄)( Β·π
βπ)π΄) β π΅)) |
34 | 33 | rspcv 3576 |
. . . . . . . 8
β’ ((πΉβπ΄) β β€ β (βπ β β€ (π(
Β·π βπ)π΄) β π΅ β ((πΉβπ΄)( Β·π
βπ)π΄) β π΅)) |
35 | | zringbas 20891 |
. . . . . . . . . . . 12
β’ β€ =
(Baseββ€ring) |
36 | 35 | eqcomi 2742 |
. . . . . . . . . . 11
β’
(Baseββ€ring) = β€ |
37 | 36 | eleq2i 2826 |
. . . . . . . . . 10
β’ ((πΉβπ΄) β (Baseββ€ring)
β (πΉβπ΄) β
β€) |
38 | 37 | biimpi 215 |
. . . . . . . . 9
β’ ((πΉβπ΄) β (Baseββ€ring)
β (πΉβπ΄) β
β€) |
39 | 38 | adantr 482 |
. . . . . . . 8
β’ (((πΉβπ΄) β (Baseββ€ring)
β§ πΉ = {β¨π΄, (πΉβπ΄)β©}) β (πΉβπ΄) β β€) |
40 | 34, 39 | syl11 33 |
. . . . . . 7
β’
(βπ β
β€ (π(
Β·π βπ)π΄) β π΅ β (((πΉβπ΄) β (Baseββ€ring)
β§ πΉ = {β¨π΄, (πΉβπ΄)β©}) β ((πΉβπ΄)( Β·π
βπ)π΄) β π΅)) |
41 | 40 | adantr 482 |
. . . . . 6
β’
((βπ β
β€ (π(
Β·π βπ)π΄) β π΅ β§ βπ β β€ (π( Β·π
βπ)π΅) β π΄) β (((πΉβπ΄) β (Baseββ€ring)
β§ πΉ = {β¨π΄, (πΉβπ΄)β©}) β ((πΉβπ΄)( Β·π
βπ)π΄) β π΅)) |
42 | 31, 41 | sylbi 216 |
. . . . 5
β’
(βπ β
β€ ((π(
Β·π βπ)π΄) β π΅ β§ (π( Β·π
βπ)π΅) β π΄) β (((πΉβπ΄) β (Baseββ€ring)
β§ πΉ = {β¨π΄, (πΉβπ΄)β©}) β ((πΉβπ΄)( Β·π
βπ)π΄) β π΅)) |
43 | 30, 42 | ax-mp 5 |
. . . 4
β’ (((πΉβπ΄) β (Baseββ€ring)
β§ πΉ = {β¨π΄, (πΉβπ΄)β©}) β ((πΉβπ΄)( Β·π
βπ)π΄) β π΅) |
44 | 26, 43 | eqnetrd 3008 |
. . 3
β’ (((πΉβπ΄) β (Baseββ€ring)
β§ πΉ = {β¨π΄, (πΉβπ΄)β©}) β (πΉ( linC βπ){π΄}) β π΅) |
45 | 5, 44 | sylbi 216 |
. 2
β’ (πΉ:{π΄}βΆ(Baseββ€ring)
β (πΉ( linC
βπ){π΄}) β π΅) |
46 | 1, 45 | syl 17 |
1
β’ (πΉ β
((Baseββ€ring) βm {π΄}) β (πΉ( linC βπ){π΄}) β π΅) |