Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Atoms, hyperplanes, and covering in a left vector space (or module)
lshpat
Metamath Proof Explorer
Description: Create an atom under a hyperplane. Part of proof of Lemma B in
Crawley p. 112. ( lhpat analog.) TODO: This changes U C V in
l1cvpat and l1cvat to U e. H , which in turn change U e. H
in islshpcv to U C V , with a couple of conversions of span to
atom. Seems convoluted. Would a direct proof be better? (Contributed by NM , 11-Jan-2015)
Ref
Expression
Hypotheses
lshpat.s
|- S = ( LSubSp ` W )
lshpat.p
|- .(+) = ( LSSum ` W )
ishpat.h
|- H = ( LSHyp ` W )
lshpat.a
|- A = ( LSAtoms ` W )
lshpat.w
|- ( ph -> W e. LVec )
lshpat.l
|- ( ph -> U e. H )
lshpat.q
|- ( ph -> Q e. A )
lshpat.r
|- ( ph -> R e. A )
lshpat.n
|- ( ph -> Q =/= R )
lshpat.m
|- ( ph -> -. Q C_ U )
Assertion
lshpat
|- ( ph -> ( ( Q .(+) R ) i^i U ) e. A )
Proof
Step
Hyp
Ref
Expression
1
lshpat.s
|- S = ( LSubSp ` W )
2
lshpat.p
|- .(+) = ( LSSum ` W )
3
ishpat.h
|- H = ( LSHyp ` W )
4
lshpat.a
|- A = ( LSAtoms ` W )
5
lshpat.w
|- ( ph -> W e. LVec )
6
lshpat.l
|- ( ph -> U e. H )
7
lshpat.q
|- ( ph -> Q e. A )
8
lshpat.r
|- ( ph -> R e. A )
9
lshpat.n
|- ( ph -> Q =/= R )
10
lshpat.m
|- ( ph -> -. Q C_ U )
11
eqid
|- ( Base ` W ) = ( Base ` W )
12
eqid
|- (
13
11 1 3 12 5
islshpcv
|- ( ph -> ( U e. H <-> ( U e. S /\ U (
14
6 13
mpbid
|- ( ph -> ( U e. S /\ U (
15
14
simpld
|- ( ph -> U e. S )
16
14
simprd
|- ( ph -> U (
17
11 1 2 4 12 5 15 7 8 9 16 10
l1cvat
|- ( ph -> ( ( Q .(+) R ) i^i U ) e. A )