Metamath Proof Explorer


Theorem lsatcvatlem

Description: Lemma for lsatcvat . (Contributed by NM, 10-Jan-2015)

Ref Expression
Hypotheses lsatcvat.o 0 ˙ = 0 W
lsatcvat.s S = LSubSp W
lsatcvat.p ˙ = LSSum W
lsatcvat.a A = LSAtoms W
lsatcvat.w φ W LVec
lsatcvat.u φ U S
lsatcvat.q φ Q A
lsatcvat.r φ R A
lsatcvat.n φ U 0 ˙
lsatcvat.l φ U Q ˙ R
lsatcvat.m φ ¬ Q U
Assertion lsatcvatlem φ U A

Proof

Step Hyp Ref Expression
1 lsatcvat.o 0 ˙ = 0 W
2 lsatcvat.s S = LSubSp W
3 lsatcvat.p ˙ = LSSum W
4 lsatcvat.a A = LSAtoms W
5 lsatcvat.w φ W LVec
6 lsatcvat.u φ U S
7 lsatcvat.q φ Q A
8 lsatcvat.r φ R A
9 lsatcvat.n φ U 0 ˙
10 lsatcvat.l φ U Q ˙ R
11 lsatcvat.m φ ¬ Q U
12 lveclmod W LVec W LMod
13 5 12 syl φ W LMod
14 2 1 4 13 6 9 lssatomic φ x A x U
15 eqid L W = L W
16 5 3ad2ant1 φ x A x U W LVec
17 13 3ad2ant1 φ x A x U W LMod
18 simp2 φ x A x U x A
19 2 4 17 18 lsatlssel φ x A x U x S
20 2 4 13 7 lsatlssel φ Q S
21 20 3ad2ant1 φ x A x U Q S
22 2 3 lsmcl W LMod Q S x S Q ˙ x S
23 17 21 19 22 syl3anc φ x A x U Q ˙ x S
24 6 3ad2ant1 φ x A x U U S
25 11 3ad2ant1 φ x A x U ¬ Q U
26 sseq1 x = Q x U Q U
27 26 biimpcd x U x = Q Q U
28 27 necon3bd x U ¬ Q U x Q
29 28 3ad2ant3 φ x A x U ¬ Q U x Q
30 25 29 mpd φ x A x U x Q
31 7 3ad2ant1 φ x A x U Q A
32 1 4 16 18 31 lsatnem0 φ x A x U x Q x Q = 0 ˙
33 30 32 mpbid φ x A x U x Q = 0 ˙
34 2 3 1 4 15 16 19 31 lcvp φ x A x U x Q = 0 ˙ x L W x ˙ Q
35 33 34 mpbid φ x A x U x L W x ˙ Q
36 lmodabl W LMod W Abel
37 17 36 syl φ x A x U W Abel
38 2 lsssssubg W LMod S SubGrp W
39 17 38 syl φ x A x U S SubGrp W
40 39 19 sseldd φ x A x U x SubGrp W
41 39 21 sseldd φ x A x U Q SubGrp W
42 3 lsmcom W Abel x SubGrp W Q SubGrp W x ˙ Q = Q ˙ x
43 37 40 41 42 syl3anc φ x A x U x ˙ Q = Q ˙ x
44 35 43 breqtrd φ x A x U x L W Q ˙ x
45 simp3 φ x A x U x U
46 10 3ad2ant1 φ x A x U U Q ˙ R
47 3 lsmub1 Q SubGrp W x SubGrp W Q Q ˙ x
48 41 40 47 syl2anc φ x A x U Q Q ˙ x
49 8 3ad2ant1 φ x A x U R A
50 10 pssssd φ U Q ˙ R
51 50 3ad2ant1 φ x A x U U Q ˙ R
52 45 51 sstrd φ x A x U x Q ˙ R
53 3 4 16 18 49 31 52 30 lsatexch1 φ x A x U R Q ˙ x
54 2 4 13 8 lsatlssel φ R S
55 54 3ad2ant1 φ x A x U R S
56 39 55 sseldd φ x A x U R SubGrp W
57 39 23 sseldd φ x A x U Q ˙ x SubGrp W
58 3 lsmlub Q SubGrp W R SubGrp W Q ˙ x SubGrp W Q Q ˙ x R Q ˙ x Q ˙ R Q ˙ x
59 41 56 57 58 syl3anc φ x A x U Q Q ˙ x R Q ˙ x Q ˙ R Q ˙ x
60 48 53 59 mpbi2and φ x A x U Q ˙ R Q ˙ x
61 46 60 psssstrd φ x A x U U Q ˙ x
62 2 15 16 19 23 24 44 45 61 lcvnbtwn3 φ x A x U U = x
63 62 18 eqeltrd φ x A x U U A
64 63 rexlimdv3a φ x A x U U A
65 14 64 mpd φ U A