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 = LHyp K
lcfrlem17.o ˙ = ocH K W
lcfrlem17.u U = DVecH K W
lcfrlem17.v V = Base U
lcfrlem17.p + ˙ = + U
lcfrlem17.z 0 ˙ = 0 U
lcfrlem17.n N = LSpan U
lcfrlem17.a A = LSAtoms U
lcfrlem17.k φ K HL W H
lcfrlem17.x φ X V 0 ˙
lcfrlem17.y φ Y V 0 ˙
lcfrlem17.ne φ N X N Y
Assertion lcfrlem17 φ X + ˙ Y V 0 ˙

Proof

Step Hyp Ref Expression
1 lcfrlem17.h H = LHyp K
2 lcfrlem17.o ˙ = ocH K W
3 lcfrlem17.u U = DVecH K W
4 lcfrlem17.v V = Base U
5 lcfrlem17.p + ˙ = + U
6 lcfrlem17.z 0 ˙ = 0 U
7 lcfrlem17.n N = LSpan U
8 lcfrlem17.a A = LSAtoms U
9 lcfrlem17.k φ K HL W H
10 lcfrlem17.x φ X V 0 ˙
11 lcfrlem17.y φ Y V 0 ˙
12 lcfrlem17.ne φ N X N Y
13 1 3 9 dvhlmod φ U LMod
14 10 eldifad φ X V
15 11 eldifad φ Y V
16 4 5 lmodvacl U LMod X V Y V X + ˙ Y V
17 13 14 15 16 syl3anc φ X + ˙ Y V
18 4 5 6 7 13 14 15 12 lmodindp1 φ X + ˙ Y 0 ˙
19 eldifsn X + ˙ Y V 0 ˙ X + ˙ Y V X + ˙ Y 0 ˙
20 17 18 19 sylanbrc φ X + ˙ Y V 0 ˙