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

Theorem lcfrlem41 32381
 Description: Lemma for lcfr 32383. Eliminate span condition. (Contributed by NM, 11-Mar-2015.)
Hypotheses
Ref Expression
lcfrlem38.h
lcfrlem38.o
lcfrlem38.u
lcfrlem38.p
lcfrlem38.f LFnl
lcfrlem38.l LKer
lcfrlem38.d LDual
lcfrlem38.q
lcfrlem38.c LFnl
lcfrlem38.e
lcfrlem38.k
lcfrlem38.g
lcfrlem38.gs
lcfrlem38.xe
lcfrlem38.ye
lcfrlem38.z
lcfrlem38.x
lcfrlem38.y
Assertion
Ref Expression
lcfrlem41
Distinct variable groups:   ,   ,   ,,   ,,   ,,   ,,   ,,   ,,   ,,   ,
Allowed substitution hints:   ()   (,)   ()   (,)   (,)   (,)   ()   (,)   (,)   (,)

Proof of Theorem lcfrlem41
StepHypRef Expression
1 lcfrlem38.h . . 3
2 lcfrlem38.o . . 3
3 lcfrlem38.u . . 3
4 lcfrlem38.p . . 3
5 eqid 2436 . . 3
6 lcfrlem38.l . . 3 LKer
7 lcfrlem38.d . . 3 LDual
8 lcfrlem38.q . . 3
9 lcfrlem38.k . . . 4
11 lcfrlem38.g . . . 4
13 lcfrlem38.e . . 3
14 lcfrlem38.xe . . . 4
16 lcfrlem38.ye . . . 4
18 simpr 448 . . 3
191, 2, 3, 4, 5, 6, 7, 8, 10, 12, 13, 15, 17, 18lcfrlem6 32345 . 2
20 lcfrlem38.f . . 3 LFnl
21 lcfrlem38.c . . 3 LFnl
24 lcfrlem38.gs . . . 4