Metamath Proof Explorer

Theorem lsatcvatlem

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

Ref Expression
Hypotheses lsatcvat.o ⊢ 0 = ( 0g ‘ 𝑊 )
lsatcvat.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lsatcvat.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
lsatcvat.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
lsatcvat.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lsatcvat.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
lsatcvat.q ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
lsatcvat.r ⊢ ( 𝜑 → 𝑅 ∈ 𝐴 )
lsatcvat.n ⊢ ( 𝜑 → 𝑈 ≠ { 0 } )
lsatcvat.l ⊢ ( 𝜑 → 𝑈 ⊊ ( 𝑄 ⊕ 𝑅 ) )
lsatcvat.m ⊢ ( 𝜑 → ¬ 𝑄 ⊆ 𝑈 )
Assertion lsatcvatlem ( 𝜑 → 𝑈 ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 lsatcvat.o ⊢ 0 = ( 0g ‘ 𝑊 )
2 lsatcvat.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3 lsatcvat.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
4 lsatcvat.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
5 lsatcvat.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
6 lsatcvat.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
7 lsatcvat.q ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
8 lsatcvat.r ⊢ ( 𝜑 → 𝑅 ∈ 𝐴 )
9 lsatcvat.n ⊢ ( 𝜑 → 𝑈 ≠ { 0 } )
10 lsatcvat.l ⊢ ( 𝜑 → 𝑈 ⊊ ( 𝑄 ⊕ 𝑅 ) )
11 lsatcvat.m ⊢ ( 𝜑 → ¬ 𝑄 ⊆ 𝑈 )
12 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
13 5 12 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
14 2 1 4 13 6 9 lssatomic ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 𝑥 ⊆ 𝑈 )
15 eqid ⊢ ( ⋖L ‘ 𝑊 ) = ( ⋖L ‘ 𝑊 )
16 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → 𝑊 ∈ LVec )
17 13 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → 𝑊 ∈ LMod )
18 simp2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → 𝑥 ∈ 𝐴 )
19 2 4 17 18 lsatlssel ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → 𝑥 ∈ 𝑆 )
20 2 4 13 7 lsatlssel ⊢ ( 𝜑 → 𝑄 ∈ 𝑆 )
21 20 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → 𝑄 ∈ 𝑆 )
22 2 3 lsmcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑄 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑄 ⊕ 𝑥 ) ∈ 𝑆 )
23 17 21 19 22 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → ( 𝑄 ⊕ 𝑥 ) ∈ 𝑆 )
24 6 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → 𝑈 ∈ 𝑆 )
25 11 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → ¬ 𝑄 ⊆ 𝑈 )
26 sseq1 ⊢ ( 𝑥 = 𝑄 → ( 𝑥 ⊆ 𝑈 ↔ 𝑄 ⊆ 𝑈 ) )
27 26 biimpcd ⊢ ( 𝑥 ⊆ 𝑈 → ( 𝑥 = 𝑄 → 𝑄 ⊆ 𝑈 ) )
28 27 necon3bd ⊢ ( 𝑥 ⊆ 𝑈 → ( ¬ 𝑄 ⊆ 𝑈 → 𝑥 ≠ 𝑄 ) )
29 28 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → ( ¬ 𝑄 ⊆ 𝑈 → 𝑥 ≠ 𝑄 ) )
30 25 29 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → 𝑥 ≠ 𝑄 )
31 7 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → 𝑄 ∈ 𝐴 )
32 1 4 16 18 31 lsatnem0 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → ( 𝑥 ≠ 𝑄 ↔ ( 𝑥 ∩ 𝑄 ) = { 0 } ) )
33 30 32 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → ( 𝑥 ∩ 𝑄 ) = { 0 } )
34 2 3 1 4 15 16 19 31 lcvp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → ( ( 𝑥 ∩ 𝑄 ) = { 0 } ↔ 𝑥 ( ⋖L ‘ 𝑊 ) ( 𝑥 ⊕ 𝑄 ) ) )
35 33 34 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → 𝑥 ( ⋖L ‘ 𝑊 ) ( 𝑥 ⊕ 𝑄 ) )
36 lmodabl ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
37 17 36 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → 𝑊 ∈ Abel )
38 2 lsssssubg ⊢ ( 𝑊 ∈ LMod → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
39 17 38 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
40 39 19 sseldd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → 𝑥 ∈ ( SubGrp ‘ 𝑊 ) )
41 39 21 sseldd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → 𝑄 ∈ ( SubGrp ‘ 𝑊 ) )
42 3 lsmcom ⊢ ( ( 𝑊 ∈ Abel ∧ 𝑥 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑄 ∈ ( SubGrp ‘ 𝑊 ) ) → ( 𝑥 ⊕ 𝑄 ) = ( 𝑄 ⊕ 𝑥 ) )
43 37 40 41 42 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → ( 𝑥 ⊕ 𝑄 ) = ( 𝑄 ⊕ 𝑥 ) )
44 35 43 breqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → 𝑥 ( ⋖L ‘ 𝑊 ) ( 𝑄 ⊕ 𝑥 ) )
45 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → 𝑥 ⊆ 𝑈 )
46 10 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → 𝑈 ⊊ ( 𝑄 ⊕ 𝑅 ) )
47 3 lsmub1 ⊢ ( ( 𝑄 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝑊 ) ) → 𝑄 ⊆ ( 𝑄 ⊕ 𝑥 ) )
48 41 40 47 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → 𝑄 ⊆ ( 𝑄 ⊕ 𝑥 ) )
49 8 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → 𝑅 ∈ 𝐴 )
50 10 pssssd ⊢ ( 𝜑 → 𝑈 ⊆ ( 𝑄 ⊕ 𝑅 ) )
51 50 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → 𝑈 ⊆ ( 𝑄 ⊕ 𝑅 ) )
52 45 51 sstrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → 𝑥 ⊆ ( 𝑄 ⊕ 𝑅 ) )
53 3 4 16 18 49 31 52 30 lsatexch1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → 𝑅 ⊆ ( 𝑄 ⊕ 𝑥 ) )
54 2 4 13 8 lsatlssel ⊢ ( 𝜑 → 𝑅 ∈ 𝑆 )
55 54 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → 𝑅 ∈ 𝑆 )
56 39 55 sseldd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → 𝑅 ∈ ( SubGrp ‘ 𝑊 ) )
57 39 23 sseldd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → ( 𝑄 ⊕ 𝑥 ) ∈ ( SubGrp ‘ 𝑊 ) )
58 3 lsmlub ⊢ ( ( 𝑄 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑅 ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑄 ⊕ 𝑥 ) ∈ ( SubGrp ‘ 𝑊 ) ) → ( ( 𝑄 ⊆ ( 𝑄 ⊕ 𝑥 ) ∧ 𝑅 ⊆ ( 𝑄 ⊕ 𝑥 ) ) ↔ ( 𝑄 ⊕ 𝑅 ) ⊆ ( 𝑄 ⊕ 𝑥 ) ) )
59 41 56 57 58 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → ( ( 𝑄 ⊆ ( 𝑄 ⊕ 𝑥 ) ∧ 𝑅 ⊆ ( 𝑄 ⊕ 𝑥 ) ) ↔ ( 𝑄 ⊕ 𝑅 ) ⊆ ( 𝑄 ⊕ 𝑥 ) ) )
60 48 53 59 mpbi2and ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → ( 𝑄 ⊕ 𝑅 ) ⊆ ( 𝑄 ⊕ 𝑥 ) )
61 46 60 psssstrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → 𝑈 ⊊ ( 𝑄 ⊕ 𝑥 ) )
62 2 15 16 19 23 24 44 45 61 lcvnbtwn3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → 𝑈 = 𝑥 )
63 62 18 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑈 ) → 𝑈 ∈ 𝐴 )
64 63 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝑥 ⊆ 𝑈 → 𝑈 ∈ 𝐴 ) )
65 14 64 mpd ⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )