Step | Hyp | Ref
| Expression |
1 | | zlmodzxzldep.z |
. . . 4
β’ π = (β€ring
freeLMod {0, 1}) |
2 | | ovex 7391 |
. . . 4
β’
(β€ring freeLMod {0, 1}) β V |
3 | 1, 2 | eqeltri 2830 |
. . 3
β’ π β V |
4 | | zlmodzxzldep.a |
. . . . 5
β’ π΄ = {β¨0, 3β©, β¨1,
6β©} |
5 | | zlmodzxzldep.b |
. . . . 5
β’ π΅ = {β¨0, 2β©, β¨1,
4β©} |
6 | | zlmodzxzldeplem.f |
. . . . 5
β’ πΉ = {β¨π΄, 2β©, β¨π΅, -3β©} |
7 | 1, 4, 5, 6 | zlmodzxzldeplem1 46667 |
. . . 4
β’ πΉ β (β€
βm {π΄,
π΅}) |
8 | 1 | zlmodzxzlmod 46516 |
. . . . . . . 8
β’ (π β LMod β§
β€ring = (Scalarβπ)) |
9 | | simpr 486 |
. . . . . . . . 9
β’ ((π β LMod β§
β€ring = (Scalarβπ)) β β€ring =
(Scalarβπ)) |
10 | 9 | eqcomd 2739 |
. . . . . . . 8
β’ ((π β LMod β§
β€ring = (Scalarβπ)) β (Scalarβπ) = β€ring) |
11 | 8, 10 | ax-mp 5 |
. . . . . . 7
β’
(Scalarβπ) =
β€ring |
12 | 11 | fveq2i 6846 |
. . . . . 6
β’
(Baseβ(Scalarβπ)) =
(Baseββ€ring) |
13 | | zringbas 20891 |
. . . . . . 7
β’ β€ =
(Baseββ€ring) |
14 | 13 | eqcomi 2742 |
. . . . . 6
β’
(Baseββ€ring) = β€ |
15 | 12, 14 | eqtri 2761 |
. . . . 5
β’
(Baseβ(Scalarβπ)) = β€ |
16 | 15 | oveq1i 7368 |
. . . 4
β’
((Baseβ(Scalarβπ)) βm {π΄, π΅}) = (β€ βm {π΄, π΅}) |
17 | 7, 16 | eleqtrri 2833 |
. . 3
β’ πΉ β
((Baseβ(Scalarβπ)) βm {π΄, π΅}) |
18 | | 3z 12541 |
. . . . . 6
β’ 3 β
β€ |
19 | | 6nn 12247 |
. . . . . . 7
β’ 6 β
β |
20 | 19 | nnzi 12532 |
. . . . . 6
β’ 6 β
β€ |
21 | 1 | zlmodzxzel 46517 |
. . . . . 6
β’ ((3
β β€ β§ 6 β β€) β {β¨0, 3β©, β¨1,
6β©} β (Baseβπ)) |
22 | 18, 20, 21 | mp2an 691 |
. . . . 5
β’ {β¨0,
3β©, β¨1, 6β©} β (Baseβπ) |
23 | | 2z 12540 |
. . . . . 6
β’ 2 β
β€ |
24 | | 4z 12542 |
. . . . . 6
β’ 4 β
β€ |
25 | 1 | zlmodzxzel 46517 |
. . . . . 6
β’ ((2
β β€ β§ 4 β β€) β {β¨0, 2β©, β¨1,
4β©} β (Baseβπ)) |
26 | 23, 24, 25 | mp2an 691 |
. . . . 5
β’ {β¨0,
2β©, β¨1, 4β©} β (Baseβπ) |
27 | 4 | eleq1i 2825 |
. . . . . 6
β’ (π΄ β (Baseβπ) β {β¨0, 3β©,
β¨1, 6β©} β (Baseβπ)) |
28 | 5 | eleq1i 2825 |
. . . . . 6
β’ (π΅ β (Baseβπ) β {β¨0, 2β©,
β¨1, 4β©} β (Baseβπ)) |
29 | 27, 28 | anbi12i 628 |
. . . . 5
β’ ((π΄ β (Baseβπ) β§ π΅ β (Baseβπ)) β ({β¨0, 3β©, β¨1,
6β©} β (Baseβπ) β§ {β¨0, 2β©, β¨1, 4β©}
β (Baseβπ))) |
30 | 22, 26, 29 | mpbir2an 710 |
. . . 4
β’ (π΄ β (Baseβπ) β§ π΅ β (Baseβπ)) |
31 | | prelpwi 5405 |
. . . 4
β’ ((π΄ β (Baseβπ) β§ π΅ β (Baseβπ)) β {π΄, π΅} β π« (Baseβπ)) |
32 | 30, 31 | ax-mp 5 |
. . 3
β’ {π΄, π΅} β π« (Baseβπ) |
33 | | lincval 46576 |
. . 3
β’ ((π β V β§ πΉ β
((Baseβ(Scalarβπ)) βm {π΄, π΅}) β§ {π΄, π΅} β π« (Baseβπ)) β (πΉ( linC βπ){π΄, π΅}) = (π Ξ£g (π₯ β {π΄, π΅} β¦ ((πΉβπ₯)( Β·π
βπ)π₯)))) |
34 | 3, 17, 32, 33 | mp3an 1462 |
. 2
β’ (πΉ( linC βπ){π΄, π΅}) = (π Ξ£g (π₯ β {π΄, π΅} β¦ ((πΉβπ₯)( Β·π
βπ)π₯))) |
35 | | lmodcmn 20385 |
. . . . 5
β’ (π β LMod β π β CMnd) |
36 | 35 | adantr 482 |
. . . 4
β’ ((π β LMod β§
β€ring = (Scalarβπ)) β π β CMnd) |
37 | 8, 36 | ax-mp 5 |
. . 3
β’ π β CMnd |
38 | | prex 5390 |
. . . . 5
β’ {β¨0,
3β©, β¨1, 6β©} β V |
39 | 4, 38 | eqeltri 2830 |
. . . 4
β’ π΄ β V |
40 | | prex 5390 |
. . . . 5
β’ {β¨0,
2β©, β¨1, 4β©} β V |
41 | 5, 40 | eqeltri 2830 |
. . . 4
β’ π΅ β V |
42 | 1, 4, 5 | zlmodzxzldeplem 46665 |
. . . 4
β’ π΄ β π΅ |
43 | 39, 41, 42 | 3pm3.2i 1340 |
. . 3
β’ (π΄ β V β§ π΅ β V β§ π΄ β π΅) |
44 | 8 | simpli 485 |
. . . . 5
β’ π β LMod |
45 | | elmapi 8790 |
. . . . . . 7
β’ (πΉ β (β€
βm {π΄,
π΅}) β πΉ:{π΄, π΅}βΆβ€) |
46 | 39 | prid1 4724 |
. . . . . . . 8
β’ π΄ β {π΄, π΅} |
47 | | ffvelcdm 7033 |
. . . . . . . 8
β’ ((πΉ:{π΄, π΅}βΆβ€ β§ π΄ β {π΄, π΅}) β (πΉβπ΄) β β€) |
48 | 46, 47 | mpan2 690 |
. . . . . . 7
β’ (πΉ:{π΄, π΅}βΆβ€ β (πΉβπ΄) β β€) |
49 | 7, 45, 48 | mp2b 10 |
. . . . . 6
β’ (πΉβπ΄) β β€ |
50 | 8, 9 | ax-mp 5 |
. . . . . . . . 9
β’
β€ring = (Scalarβπ) |
51 | 50 | eqcomi 2742 |
. . . . . . . 8
β’
(Scalarβπ) =
β€ring |
52 | 51 | fveq2i 6846 |
. . . . . . 7
β’
(Baseβ(Scalarβπ)) =
(Baseββ€ring) |
53 | 52, 14 | eqtri 2761 |
. . . . . 6
β’
(Baseβ(Scalarβπ)) = β€ |
54 | 49, 53 | eleqtrri 2833 |
. . . . 5
β’ (πΉβπ΄) β (Baseβ(Scalarβπ)) |
55 | 4, 22 | eqeltri 2830 |
. . . . 5
β’ π΄ β (Baseβπ) |
56 | | eqid 2733 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
57 | | eqid 2733 |
. . . . . 6
β’
(Scalarβπ) =
(Scalarβπ) |
58 | | eqid 2733 |
. . . . . 6
β’ (
Β·π βπ) = ( Β·π
βπ) |
59 | | eqid 2733 |
. . . . . 6
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
60 | 56, 57, 58, 59 | lmodvscl 20354 |
. . . . 5
β’ ((π β LMod β§ (πΉβπ΄) β (Baseβ(Scalarβπ)) β§ π΄ β (Baseβπ)) β ((πΉβπ΄)( Β·π
βπ)π΄) β (Baseβπ)) |
61 | 44, 54, 55, 60 | mp3an 1462 |
. . . 4
β’ ((πΉβπ΄)( Β·π
βπ)π΄) β (Baseβπ) |
62 | 41 | prid2 4725 |
. . . . . . . 8
β’ π΅ β {π΄, π΅} |
63 | | ffvelcdm 7033 |
. . . . . . . 8
β’ ((πΉ:{π΄, π΅}βΆβ€ β§ π΅ β {π΄, π΅}) β (πΉβπ΅) β β€) |
64 | 62, 63 | mpan2 690 |
. . . . . . 7
β’ (πΉ:{π΄, π΅}βΆβ€ β (πΉβπ΅) β β€) |
65 | 7, 45, 64 | mp2b 10 |
. . . . . 6
β’ (πΉβπ΅) β β€ |
66 | 65, 53 | eleqtrri 2833 |
. . . . 5
β’ (πΉβπ΅) β (Baseβ(Scalarβπ)) |
67 | 5, 26 | eqeltri 2830 |
. . . . 5
β’ π΅ β (Baseβπ) |
68 | 56, 57, 58, 59 | lmodvscl 20354 |
. . . . 5
β’ ((π β LMod β§ (πΉβπ΅) β (Baseβ(Scalarβπ)) β§ π΅ β (Baseβπ)) β ((πΉβπ΅)( Β·π
βπ)π΅) β (Baseβπ)) |
69 | 44, 66, 67, 68 | mp3an 1462 |
. . . 4
β’ ((πΉβπ΅)( Β·π
βπ)π΅) β (Baseβπ) |
70 | 61, 69 | pm3.2i 472 |
. . 3
β’ (((πΉβπ΄)( Β·π
βπ)π΄) β (Baseβπ) β§ ((πΉβπ΅)( Β·π
βπ)π΅) β (Baseβπ)) |
71 | | eqid 2733 |
. . . 4
β’
(+gβπ) = (+gβπ) |
72 | | fveq2 6843 |
. . . . 5
β’ (π₯ = π΄ β (πΉβπ₯) = (πΉβπ΄)) |
73 | | id 22 |
. . . . 5
β’ (π₯ = π΄ β π₯ = π΄) |
74 | 72, 73 | oveq12d 7376 |
. . . 4
β’ (π₯ = π΄ β ((πΉβπ₯)( Β·π
βπ)π₯) = ((πΉβπ΄)( Β·π
βπ)π΄)) |
75 | | fveq2 6843 |
. . . . 5
β’ (π₯ = π΅ β (πΉβπ₯) = (πΉβπ΅)) |
76 | | id 22 |
. . . . 5
β’ (π₯ = π΅ β π₯ = π΅) |
77 | 75, 76 | oveq12d 7376 |
. . . 4
β’ (π₯ = π΅ β ((πΉβπ₯)( Β·π
βπ)π₯) = ((πΉβπ΅)( Β·π
βπ)π΅)) |
78 | 56, 71, 74, 77 | gsumpr 19737 |
. . 3
β’ ((π β CMnd β§ (π΄ β V β§ π΅ β V β§ π΄ β π΅) β§ (((πΉβπ΄)( Β·π
βπ)π΄) β (Baseβπ) β§ ((πΉβπ΅)( Β·π
βπ)π΅) β (Baseβπ))) β (π Ξ£g (π₯ β {π΄, π΅} β¦ ((πΉβπ₯)( Β·π
βπ)π₯))) = (((πΉβπ΄)( Β·π
βπ)π΄)(+gβπ)((πΉβπ΅)( Β·π
βπ)π΅))) |
79 | 37, 43, 70, 78 | mp3an 1462 |
. 2
β’ (π Ξ£g
(π₯ β {π΄, π΅} β¦ ((πΉβπ₯)( Β·π
βπ)π₯))) = (((πΉβπ΄)( Β·π
βπ)π΄)(+gβπ)((πΉβπ΅)( Β·π
βπ)π΅)) |
80 | 6 | fveq1i 6844 |
. . . . . 6
β’ (πΉβπ΄) = ({β¨π΄, 2β©, β¨π΅, -3β©}βπ΄) |
81 | | 2ex 12235 |
. . . . . . . 8
β’ 2 β
V |
82 | 39, 81 | fvpr1 7140 |
. . . . . . 7
β’ (π΄ β π΅ β ({β¨π΄, 2β©, β¨π΅, -3β©}βπ΄) = 2) |
83 | 42, 82 | ax-mp 5 |
. . . . . 6
β’
({β¨π΄, 2β©,
β¨π΅,
-3β©}βπ΄) =
2 |
84 | 80, 83 | eqtri 2761 |
. . . . 5
β’ (πΉβπ΄) = 2 |
85 | 84 | oveq1i 7368 |
. . . 4
β’ ((πΉβπ΄)( Β·π
βπ)π΄) = (2( Β·π
βπ)π΄) |
86 | 6 | fveq1i 6844 |
. . . . . 6
β’ (πΉβπ΅) = ({β¨π΄, 2β©, β¨π΅, -3β©}βπ΅) |
87 | | negex 11404 |
. . . . . . . 8
β’ -3 β
V |
88 | 41, 87 | fvpr2 7142 |
. . . . . . 7
β’ (π΄ β π΅ β ({β¨π΄, 2β©, β¨π΅, -3β©}βπ΅) = -3) |
89 | 42, 88 | ax-mp 5 |
. . . . . 6
β’
({β¨π΄, 2β©,
β¨π΅,
-3β©}βπ΅) =
-3 |
90 | 86, 89 | eqtri 2761 |
. . . . 5
β’ (πΉβπ΅) = -3 |
91 | 90 | oveq1i 7368 |
. . . 4
β’ ((πΉβπ΅)( Β·π
βπ)π΅) = (-3( Β·π
βπ)π΅) |
92 | 85, 91 | oveq12i 7370 |
. . 3
β’ (((πΉβπ΄)( Β·π
βπ)π΄)(+gβπ)((πΉβπ΅)( Β·π
βπ)π΅)) = ((2(
Β·π βπ)π΄)(+gβπ)(-3( Β·π
βπ)π΅)) |
93 | | eqid 2733 |
. . . . . 6
β’ {β¨0,
0β©, β¨1, 0β©} = {β¨0, 0β©, β¨1,
0β©} |
94 | 1, 93 | zlmodzxz0 46518 |
. . . . 5
β’ {β¨0,
0β©, β¨1, 0β©} = (0gβπ) |
95 | 94 | eqcomi 2742 |
. . . 4
β’
(0gβπ) = {β¨0, 0β©, β¨1,
0β©} |
96 | 1, 4, 5, 95, 71, 58 | zlmodzxzequap 46666 |
. . 3
β’ ((2(
Β·π βπ)π΄)(+gβπ)(-3( Β·π
βπ)π΅)) = (0gβπ) |
97 | 92, 96 | eqtri 2761 |
. 2
β’ (((πΉβπ΄)( Β·π
βπ)π΄)(+gβπ)((πΉβπ΅)( Β·π
βπ)π΅)) = (0gβπ) |
98 | 34, 79, 97 | 3eqtri 2765 |
1
β’ (πΉ( linC βπ){π΄, π΅}) = (0gβπ) |