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

Theorem islshpkrN 32138
 Description: The predicate "is a hyperplane" (of a left module or left vector space). TODO: should it be or as in lshpkrex 32136? Both standards seem to be used randomly throughout set.mm; we should decide on a preferred one. (Contributed by NM, 7-Oct-2014.) (New usage is discouraged.)
Hypotheses
Ref Expression
lshpset2.v
lshpset2.d Scalar
lshpset2.z
lshpset2.h LSHyp
lshpset2.f LFnl
lshpset2.k LKer
Assertion
Ref Expression
islshpkrN
Distinct variable groups:   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem islshpkrN
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 lshpset2.v . . . 4
2 lshpset2.d . . . 4 Scalar
3 lshpset2.z . . . 4
4 lshpset2.h . . . 4 LSHyp
5 lshpset2.f . . . 4 LFnl
6 lshpset2.k . . . 4 LKer
71, 2, 3, 4, 5, 6lshpset2N 32137 . . 3
87eleq2d 2472 . 2
9 elex 3068 . . . 4
11 fvex 5859 . . . . . . 7
12 eleq1 2474 . . . . . . 7
1311, 12mpbiri 233 . . . . . 6
1413adantl 464 . . . . 5
1514rexlimivw 2893 . . . 4