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

Theorem lcfrlem34 32311
 Description: Lemma for lcfr 32320. (Contributed by NM, 10-Mar-2015.)
Hypotheses
Ref Expression
lcfrlem17.h
lcfrlem17.o
lcfrlem17.u
lcfrlem17.v
lcfrlem17.p
lcfrlem17.z
lcfrlem17.n
lcfrlem17.a LSAtoms
lcfrlem17.k
lcfrlem17.x
lcfrlem17.y
lcfrlem17.ne
lcfrlem22.b
lcfrlem24.t
lcfrlem24.s Scalar
lcfrlem24.q
lcfrlem24.r
lcfrlem24.j
lcfrlem24.ib
lcfrlem24.l LKer
lcfrlem25.d LDual
lcfrlem28.jn
lcfrlem29.i
lcfrlem30.m
lcfrlem30.c
Assertion
Ref Expression
lcfrlem34
Distinct variable groups:   ,,,,   ,,,,   ,,,   ,   ,,,,   ,,   ,,,,   ,,,,   ,
Allowed substitution hints:   (,,,)   (,,,)   (,,,)   (,,,)   (,,,)   (,,,)   ()   (,,)   (,,,)   (,,,)   (,,,)   (,,,)   (,,,)   (,,,)   (,,,)   (,,,)   (,,,)   (,)   (,,,)   (,,)

Proof of Theorem lcfrlem34
StepHypRef Expression
1 lcfrlem17.h . . 3
2 lcfrlem17.o . . 3
3 lcfrlem17.u . . 3
4 lcfrlem17.v . . 3
5 lcfrlem17.p . . 3
6 lcfrlem17.z . . 3
7 lcfrlem17.n . . 3
8 lcfrlem17.a . . 3 LSAtoms
9 lcfrlem17.k . . . 4
11 lcfrlem17.x . . . 4
13 lcfrlem17.y . . . 4
15 lcfrlem17.ne . . . 4
17 lcfrlem22.b . . 3
18 lcfrlem24.t . . 3
19 lcfrlem24.s . . 3 Scalar
20 lcfrlem24.q . . 3
21 lcfrlem24.r . . 3
22 lcfrlem24.j . . 3
23 lcfrlem24.ib . . . 4
25 lcfrlem24.l . . 3 LKer
26 lcfrlem25.d . . 3 LDual
27 lcfrlem28.jn . . . 4
29 lcfrlem29.i . . 3
30 lcfrlem30.m . . 3
31 lcfrlem30.c . . 3
32 simpr 448 . . 3
331, 2, 3, 4, 5, 6, 7, 8, 10, 12, 14, 16, 17, 18, 19, 20, 21, 22, 24, 25, 26, 28, 29, 30, 31, 32lcfrlem33 32310 . 2