Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lmod1lem5 Structured version   Unicode version

Theorem lmod1lem5 32050
 Description: Lemma 5 for lmod1 32051. (Contributed by AV, 28-Apr-2019.)
Hypothesis
Ref Expression
lmod1.m Scalar
Assertion
Ref Expression
lmod1lem5 Scalar
Distinct variable groups:   ,,   ,,   ,,   ,,

Proof of Theorem lmod1lem5
StepHypRef Expression
1 fvex 5869 . . . . . . 7
2 snex 4683 . . . . . . 7
31, 2pm3.2i 455 . . . . . 6
43a1i 11 . . . . 5
5 eqid 2462 . . . . . 6
65mpt2exg 6850 . . . . 5
7 lmod1.m . . . . . 6 Scalar
87lmodvsca 14614 . . . . 5
94, 6, 83syl 20 . . . 4
109eqcomd 2470 . . 3
1110oveqd 6294 . 2 Scalar Scalar
12 eqidd 2463 . . 3
13 simprr 756 . . 3 Scalar
147lmodsca 14613 . . . . . . 7 Scalar
1514adantl 466 . . . . . 6 Scalar
1615eqcomd 2470 . . . . 5 Scalar
1716fveq2d 5863 . . . 4 Scalar
18 eqid 2462 . . . . . 6
19 eqid 2462 . . . . . 6
2018, 19rngidcl 17001 . . . . 5
2120adantl 466 . . . 4
2217, 21eqeltrd 2550 . . 3 Scalar
23 snidg 4048 . . . 4