Metamath Proof Explorer


Theorem lcfrlem20

Description: Lemma for lcfr . (Contributed by NM, 11-Mar-2015)

Ref Expression
Hypotheses lcfrlem17.h H=LHypK
lcfrlem17.o ˙=ocHKW
lcfrlem17.u U=DVecHKW
lcfrlem17.v V=BaseU
lcfrlem17.p +˙=+U
lcfrlem17.z 0˙=0U
lcfrlem17.n N=LSpanU
lcfrlem17.a A=LSAtomsU
lcfrlem17.k φKHLWH
lcfrlem17.x φXV0˙
lcfrlem17.y φYV0˙
lcfrlem17.ne φNXNY
lcfrlem20.e φ¬X˙X+˙Y
Assertion lcfrlem20 φNXY˙X+˙YA

Proof

Step Hyp Ref Expression
1 lcfrlem17.h H=LHypK
2 lcfrlem17.o ˙=ocHKW
3 lcfrlem17.u U=DVecHKW
4 lcfrlem17.v V=BaseU
5 lcfrlem17.p +˙=+U
6 lcfrlem17.z 0˙=0U
7 lcfrlem17.n N=LSpanU
8 lcfrlem17.a A=LSAtomsU
9 lcfrlem17.k φKHLWH
10 lcfrlem17.x φXV0˙
11 lcfrlem17.y φYV0˙
12 lcfrlem17.ne φNXNY
13 lcfrlem20.e φ¬X˙X+˙Y
14 eqid LSSumU=LSSumU
15 1 3 9 dvhlmod φULMod
16 10 eldifad φXV
17 11 eldifad φYV
18 4 7 14 15 16 17 lsmpr φNXY=NXLSSumUNY
19 18 ineq1d φNXY˙X+˙Y=NXLSSumUNY˙X+˙Y
20 eqid LSubSpU=LSubSpU
21 eqid LSHypU=LSHypU
22 1 3 9 dvhlvec φULVec
23 1 2 3 4 5 6 7 8 9 10 11 12 lcfrlem17 φX+˙YV0˙
24 1 2 3 4 6 21 9 23 dochsnshp φ˙X+˙YLSHypU
25 4 7 6 8 15 10 lsatlspsn φNXA
26 4 7 6 8 15 11 lsatlspsn φNYA
27 4 5 lmodvacl ULModXVYVX+˙YV
28 15 16 17 27 syl3anc φX+˙YV
29 28 snssd φX+˙YV
30 1 3 4 20 2 dochlss KHLWHX+˙YV˙X+˙YLSubSpU
31 9 29 30 syl2anc φ˙X+˙YLSubSpU
32 4 20 7 15 31 16 lspsnel5 φX˙X+˙YNX˙X+˙Y
33 13 32 mtbid φ¬NX˙X+˙Y
34 20 14 21 8 22 24 25 26 12 33 lshpat φNXLSSumUNY˙X+˙YA
35 19 34 eqeltrd φNXY˙X+˙YA