Metamath Proof Explorer


Theorem lcfrlem17

Description: Lemma for lcfr . Condition needed more than once. (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
Assertion lcfrlem17 φX+˙YV0˙

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 1 3 9 dvhlmod φULMod
14 10 eldifad φXV
15 11 eldifad φYV
16 4 5 lmodvacl ULModXVYVX+˙YV
17 13 14 15 16 syl3anc φX+˙YV
18 4 5 6 7 13 14 15 12 lmodindp1 φX+˙Y0˙
19 eldifsn X+˙YV0˙X+˙YVX+˙Y0˙
20 17 18 19 sylanbrc φX+˙YV0˙