Metamath Proof Explorer


Theorem zlmodzxzldep

Description: { A , B } is a linearly dependent set within the ZZ-module ZZ X. ZZ (see example in Roman p. 112). (Contributed by AV, 22-May-2019) (Revised by AV, 10-Jun-2019)

Ref Expression
Hypotheses zlmodzxzldep.z Z = ring freeLMod 0 1
zlmodzxzldep.a A = 0 3 1 6
zlmodzxzldep.b B = 0 2 1 4
Assertion zlmodzxzldep A B linDepS Z

Proof

Step Hyp Ref Expression
1 zlmodzxzldep.z Z = ring freeLMod 0 1
2 zlmodzxzldep.a A = 0 3 1 6
3 zlmodzxzldep.b B = 0 2 1 4
4 eqid A 2 B 3 = A 2 B 3
5 1 2 3 4 zlmodzxzldeplem1 A 2 B 3 A B
6 1 2 3 4 zlmodzxzldeplem2 finSupp 0 A 2 B 3
7 1 2 3 4 zlmodzxzldeplem3 A 2 B 3 linC Z A B = 0 Z
8 1 2 3 4 zlmodzxzldeplem4 y A B A 2 B 3 y 0
9 6 7 8 3pm3.2i finSupp 0 A 2 B 3 A 2 B 3 linC Z A B = 0 Z y A B A 2 B 3 y 0
10 breq1 x = A 2 B 3 finSupp 0 x finSupp 0 A 2 B 3
11 oveq1 x = A 2 B 3 x linC Z A B = A 2 B 3 linC Z A B
12 11 eqeq1d x = A 2 B 3 x linC Z A B = 0 Z A 2 B 3 linC Z A B = 0 Z
13 fveq1 x = A 2 B 3 x y = A 2 B 3 y
14 13 neeq1d x = A 2 B 3 x y 0 A 2 B 3 y 0
15 14 rexbidv x = A 2 B 3 y A B x y 0 y A B A 2 B 3 y 0
16 10 12 15 3anbi123d x = A 2 B 3 finSupp 0 x x linC Z A B = 0 Z y A B x y 0 finSupp 0 A 2 B 3 A 2 B 3 linC Z A B = 0 Z y A B A 2 B 3 y 0
17 16 rspcev A 2 B 3 A B finSupp 0 A 2 B 3 A 2 B 3 linC Z A B = 0 Z y A B A 2 B 3 y 0 x A B finSupp 0 x x linC Z A B = 0 Z y A B x y 0
18 5 9 17 mp2an x A B finSupp 0 x x linC Z A B = 0 Z y A B x y 0
19 ovex ring freeLMod 0 1 V
20 1 19 eqeltri Z V
21 3z 3
22 6nn 6
23 22 nnzi 6
24 1 zlmodzxzel 3 6 0 3 1 6 Base Z
25 21 23 24 mp2an 0 3 1 6 Base Z
26 2 25 eqeltri A Base Z
27 2z 2
28 4z 4
29 1 zlmodzxzel 2 4 0 2 1 4 Base Z
30 27 28 29 mp2an 0 2 1 4 Base Z
31 3 30 eqeltri B Base Z
32 prelpwi A Base Z B Base Z A B 𝒫 Base Z
33 26 31 32 mp2an A B 𝒫 Base Z
34 eqid Base Z = Base Z
35 eqid 0 Z = 0 Z
36 1 zlmodzxzlmod Z LMod ring = Scalar Z
37 36 simpri ring = Scalar Z
38 zringbas = Base ring
39 zring0 0 = 0 ring
40 34 35 37 38 39 islindeps Z V A B 𝒫 Base Z A B linDepS Z x A B finSupp 0 x x linC Z A B = 0 Z y A B x y 0
41 20 33 40 mp2an A B linDepS Z x A B finSupp 0 x x linC Z A B = 0 Z y A B x y 0
42 18 41 mpbir A B linDepS Z