Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lshpkrlem4 Structured version   Unicode version

Theorem lshpkrlem4 29838
 Description: Lemma for lshpkrex 29843. Part of showing linearity of . (Contributed by NM, 16-Jul-2014.)
Hypotheses
Ref Expression
lshpkrlem.v
lshpkrlem.a
lshpkrlem.n
lshpkrlem.p
lshpkrlem.h LSHyp
lshpkrlem.w
lshpkrlem.u
lshpkrlem.z
lshpkrlem.x
lshpkrlem.e
lshpkrlem.d Scalar
lshpkrlem.k
lshpkrlem.t
lshpkrlem.o
lshpkrlem.g
Assertion
Ref Expression
lshpkrlem4
Distinct variable groups:   ,,,   ,,   ,   ,,,   ,,,   ,   ,,,   ,,,   ,   ,   ,   ,   ,   ,,,,   ,   ,,,,
Allowed substitution hints:   (,,,,,,,)   (,,,,,,,)   (,,,)   (,,,,,,,)   (,,,)   (,,,)   (,,,,,,)   (,,,,,,,)   (,,,,)   (,,,,,,,)   (,,,,,,)   (,,,,,,,)   (,,,)   (,,,,,,)   (,,,)

Proof of Theorem lshpkrlem4
StepHypRef Expression
1 simp3l 985 . . . 4
21oveq2d 6089 . . 3
3 simp3r 986 . . 3
42, 3oveq12d 6091 . 2
5 simpl1 960 . . . . . . . 8
6 lshpkrlem.w . . . . . . . 8
7 lveclmod 16170 . . . . . . . 8
85, 6, 73syl 19 . . . . . . 7
9 simpl2 961 . . . . . . 7
10 simpr2 964 . . . . . . 7
11 simpl3 962 . . . . . . . . 9
12 lshpkrlem.v . . . . . . . . . 10
13 lshpkrlem.a . . . . . . . . . 10
14 lshpkrlem.n . . . . . . . . . 10
15 lshpkrlem.p . . . . . . . . . 10
16 lshpkrlem.h . . . . . . . . . 10 LSHyp
176adantr 452 . . . . . . . . . 10
18 lshpkrlem.u . . . . . . . . . . 11
1918adantr 452 . . . . . . . . . 10
20 lshpkrlem.z . . . . . . . . . . 11
2120adantr 452 . . . . . . . . . 10
22 simpr 448 . . . . . . . . . 10
23 lshpkrlem.e . . . . . . . . . . 11
2423adantr 452 . . . . . . . . . 10
25 lshpkrlem.d . . . . . . . . . 10 Scalar
26 lshpkrlem.k . . . . . . . . . 10
27 lshpkrlem.t . . . . . . . . . 10
28 lshpkrlem.o . . . . . . . . . 10
29 lshpkrlem.g . . . . . . . . . 10
3012, 13, 14, 15, 16, 17, 19, 21, 22, 24, 25, 26, 27, 28, 29lshpkrlem2 29836 . . . . . . . . 9
315, 11, 30syl2anc 643 . . . . . . . 8
325, 20syl 16 . . . . . . . 8
3312, 25, 27, 26lmodvscl 15959 . . . . . . . 8
348, 31, 32, 33syl3anc 1184 . . . . . . 7
3512, 13, 25, 27, 26lmodvsdi 15965 . . . . . . 7
368, 9, 10, 34, 35syl13anc 1186 . . . . . 6
37 eqid 2435 . . . . . . . . 9
3812, 25, 27, 26, 37lmodvsass 15967 . . . . . . . 8
398, 9, 31, 32, 38syl13anc 1186 . . . . . . 7
4039oveq2d 6089 . . . . . 6
4136, 40eqtr4d 2470 . . . . 5
4241oveq1d 6088 . . . 4
4312, 25, 27, 26lmodvscl 15959 . . . . . . 7
448, 9, 10, 43syl3anc 1184 . . . . . 6
4525, 26, 37lmodmcl 15954 . . . . . . . 8
468, 9, 31, 45syl3anc 1184 . . . . . . 7
4712, 25, 27, 26lmodvscl 15959 . . . . . . 7
488, 46, 32, 47syl3anc 1184 . . . . . 6
49 simpr3 965 . . . . . 6
50 simpr1 963 . . . . . . . 8
516adantr 452 . . . . . . . . 9
5218adantr 452 . . . . . . . . 9
5320adantr 452 . . . . . . . . 9
54 simpr 448 . . . . . . . . 9
5523adantr 452 . . . . . . . . 9
5612, 13, 14, 15, 16, 51, 52, 53, 54, 55, 25, 26, 27, 28, 29lshpkrlem2 29836 . . . . . . . 8
575, 50, 56syl2anc 643 . . . . . . 7
5812, 25, 27, 26lmodvscl 15959 . . . . . . 7
598, 57, 32, 58syl3anc 1184 . . . . . 6
6012, 13lmod4 15986 . . . . . 6
618, 44, 48, 49, 59, 60syl122anc 1193 . . . . 5
62 eqid 2435 . . . . . . . 8
6312, 13, 25, 27, 26, 62lmodvsdir 15966 . . . . . . 7
648, 46, 57, 32, 63syl13anc 1186 . . . . . 6
6564oveq2d 6089 . . . . 5
6661, 65eqtr4d 2470 . . . 4
6742, 66eqtrd 2467 . . 3