Description: The scalar product of a vector with powers of _i belongs to the base set of a subcomplex module if the scalar subring of th subcomplex module contains _i . (Contributed by AV, 18-Oct-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cmodscexp.f | |
|
cmodscexp.k | |
||
cmodscmulexp.x | |
||
cmodscmulexp.s | |
||
Assertion | cmodscmulexp | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cmodscexp.f | |
|
2 | cmodscexp.k | |
|
3 | cmodscmulexp.x | |
|
4 | cmodscmulexp.s | |
|
5 | clmlmod | |
|
6 | 5 | adantr | |
7 | simp1 | |
|
8 | 7 | anim2i | |
9 | simpr3 | |
|
10 | 1 2 | cmodscexp | |
11 | 8 9 10 | syl2anc | |
12 | simpr2 | |
|
13 | 3 1 4 2 | lmodvscl | |
14 | 6 11 12 13 | syl3anc | |