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