Description: Lemma 2 for lmod1 . (Contributed by AV, 28-Apr-2019)
Ref | Expression | ||
---|---|---|---|
Hypothesis | lmod1.m | |
|
Assertion | lmod1lem2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lmod1.m | |
|
2 | fvex | |
|
3 | snex | |
|
4 | 2 3 | pm3.2i | |
5 | mpoexga | |
|
6 | 4 5 | mp1i | |
7 | 1 | lmodvsca | |
8 | 6 7 | syl | |
9 | 8 | eqcomd | |
10 | simprr | |
|
11 | simp3 | |
|
12 | snidg | |
|
13 | 12 | 3ad2ant1 | |
14 | 9 10 11 13 13 | ovmpod | |
15 | snex | |
|
16 | 1 | lmodplusg | |
17 | 15 16 | mp1i | |
18 | 17 | eqcomd | |
19 | 18 | oveqd | |
20 | df-ov | |
|
21 | opex | |
|
22 | simp1 | |
|
23 | fvsng | |
|
24 | 21 22 23 | sylancr | |
25 | 20 24 | eqtrid | |
26 | 19 25 | eqtrd | |
27 | 26 | oveq2d | |
28 | 3 | a1i | |
29 | 2 28 5 | sylancr | |
30 | 29 7 | syl | |
31 | 30 | eqcomd | |
32 | 31 10 11 13 13 | ovmpod | |
33 | 32 32 | oveq12d | |
34 | 33 26 | eqtrd | |
35 | 14 27 34 | 3eqtr4d | |