Description: Example of an equation within the ZZ-module ZZ X. ZZ (see example in Roman p. 112 for a linearly dependent set). (Contributed by AV, 22-May-2019) (Revised by AV, 10-Jun-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | zlmodzxzequa.z | |
|
zlmodzxzequa.o | |
||
zlmodzxzequa.t | |
||
zlmodzxzequa.m | |
||
zlmodzxzequa.a | |
||
zlmodzxzequa.b | |
||
Assertion | zlmodzxzequa | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zlmodzxzequa.z | |
|
2 | zlmodzxzequa.o | |
|
3 | zlmodzxzequa.t | |
|
4 | zlmodzxzequa.m | |
|
5 | zlmodzxzequa.a | |
|
6 | zlmodzxzequa.b | |
|
7 | 3cn | |
|
8 | 7 | 2timesi | |
9 | 3p3e6 | |
|
10 | 8 9 | eqtri | |
11 | 3t2e6 | |
|
12 | 10 11 | oveq12i | |
13 | 6cn | |
|
14 | 13 | subidi | |
15 | 12 14 | eqtri | |
16 | 15 | opeq2i | |
17 | 2t6m3t4e0 | |
|
18 | 17 | opeq2i | |
19 | 16 18 | preq12i | |
20 | 5 | oveq2i | |
21 | 2z | |
|
22 | 3z | |
|
23 | 6nn | |
|
24 | 23 | nnzi | |
25 | 1 3 | zlmodzxzscm | |
26 | 21 22 24 25 | mp3an | |
27 | 20 26 | eqtri | |
28 | 6 | oveq2i | |
29 | 4z | |
|
30 | 1 3 | zlmodzxzscm | |
31 | 22 21 29 30 | mp3an | |
32 | 28 31 | eqtri | |
33 | 27 32 | oveq12i | |
34 | zmulcl | |
|
35 | 21 22 34 | mp2an | |
36 | zmulcl | |
|
37 | 22 21 36 | mp2an | |
38 | zmulcl | |
|
39 | 21 24 38 | mp2an | |
40 | zmulcl | |
|
41 | 22 29 40 | mp2an | |
42 | 1 4 | zlmodzxzsub | |
43 | 35 37 39 41 42 | mp4an | |
44 | 33 43 | eqtri | |
45 | 19 44 2 | 3eqtr4i | |