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

Theorem hlhilsrnglem 32754
 Description: Lemma for hlhilsrng 32755. (Contributed by NM, 21-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.)
Hypotheses
Ref Expression
hlhillvec.h
hlhillvec.u HLHil
hlhillvec.k
hlhildrng.r Scalar
hlhilsrng.l
hlhilsrng.s Scalar
hlhilsrng.b
hlhilsrng.p
hlhilsrng.t
hlhilsrng.g HGMap
Assertion
Ref Expression
hlhilsrnglem

Proof of Theorem hlhilsrnglem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hlhillvec.h . . 3
2 hlhilsrng.l . . 3
3 hlhilsrng.s . . 3 Scalar
4 hlhillvec.u . . 3 HLHil
5 hlhildrng.r . . 3 Scalar
6 hlhillvec.k . . 3
7 hlhilsrng.b . . 3
81, 2, 3, 4, 5, 6, 7hlhilsbase2 32743 . 2
9 hlhilsrng.p . . 3
101, 2, 3, 4, 5, 6, 9hlhilsplus2 32744 . 2
11 hlhilsrng.t . . 3
121, 2, 3, 4, 5, 6, 11hlhilsmul2 32745 . 2
13 hlhilsrng.g . . 3 HGMap
141, 4, 5, 13, 6hlhilnvl 32751 . 2
151, 4, 6, 5hlhildrng 32753 . . 3
16 drngrng 15842 . . 3
1715, 16syl 16 . 2