Metamath Proof Explorer


Theorem lcfrlem19

Description: Lemma for lcfr . (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 lcfrlem19 φ ¬ X ˙ X + ˙ Y ¬ Y ˙ X + ˙ Y

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 2 3 4 5 6 7 8 9 10 11 12 lcfrlem17 φ X + ˙ Y V 0 ˙
14 1 2 3 4 6 9 13 dochnel φ ¬ X + ˙ Y ˙ X + ˙ Y
15 1 3 9 dvhlmod φ U LMod
16 15 adantr φ X ˙ X + ˙ Y Y ˙ X + ˙ Y U LMod
17 10 eldifad φ X V
18 11 eldifad φ Y V
19 4 5 lmodvacl U LMod X V Y V X + ˙ Y V
20 15 17 18 19 syl3anc φ X + ˙ Y V
21 20 snssd φ X + ˙ Y V
22 eqid LSubSp U = LSubSp U
23 1 3 4 22 2 dochlss K HL W H X + ˙ Y V ˙ X + ˙ Y LSubSp U
24 9 21 23 syl2anc φ ˙ X + ˙ Y LSubSp U
25 24 adantr φ X ˙ X + ˙ Y Y ˙ X + ˙ Y ˙ X + ˙ Y LSubSp U
26 simpr φ X ˙ X + ˙ Y Y ˙ X + ˙ Y X ˙ X + ˙ Y Y ˙ X + ˙ Y
27 5 22 lssvacl U LMod ˙ X + ˙ Y LSubSp U X ˙ X + ˙ Y Y ˙ X + ˙ Y X + ˙ Y ˙ X + ˙ Y
28 16 25 26 27 syl21anc φ X ˙ X + ˙ Y Y ˙ X + ˙ Y X + ˙ Y ˙ X + ˙ Y
29 14 28 mtand φ ¬ X ˙ X + ˙ Y Y ˙ X + ˙ Y
30 ianor ¬ X ˙ X + ˙ Y Y ˙ X + ˙ Y ¬ X ˙ X + ˙ Y ¬ Y ˙ X + ˙ Y
31 29 30 sylib φ ¬ X ˙ X + ˙ Y ¬ Y ˙ X + ˙ Y