This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lsatcvat3

Description: A condition implying that a certain subspace is an atom. Part of Lemma 3.2.20 of PtakPulmannova p. 68. ( atcvat3i analog.) (Contributed by NM, 11-Jan-2015)

Ref Expression
Hypotheses lsatcvat3.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lsatcvat3.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
lsatcvat3.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
lsatcvat3.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lsatcvat3.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
lsatcvat3.q ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
lsatcvat3.r ⊢ ( 𝜑 → 𝑅 ∈ 𝐴 )
lsatcvat3.n ⊢ ( 𝜑 → 𝑄 ≠ 𝑅 )
lsatcvat3.m ⊢ ( 𝜑 → ¬ 𝑅 ⊆ 𝑈 )
lsatcvat3.l ⊢ ( 𝜑 → 𝑄 ⊆ ( 𝑈 ⊕ 𝑅 ) )
Assertion lsatcvat3 ( 𝜑 → ( 𝑈 ∩ ( 𝑄 ⊕ 𝑅 ) ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 lsatcvat3.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2 lsatcvat3.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
3 lsatcvat3.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
4 lsatcvat3.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
5 lsatcvat3.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
6 lsatcvat3.q ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
7 lsatcvat3.r ⊢ ( 𝜑 → 𝑅 ∈ 𝐴 )
8 lsatcvat3.n ⊢ ( 𝜑 → 𝑄 ≠ 𝑅 )
9 lsatcvat3.m ⊢ ( 𝜑 → ¬ 𝑅 ⊆ 𝑈 )
10 lsatcvat3.l ⊢ ( 𝜑 → 𝑄 ⊆ ( 𝑈 ⊕ 𝑅 ) )
11 eqid ⊢ ( ⋖L ‘ 𝑊 ) = ( ⋖L ‘ 𝑊 )
12 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
13 4 12 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
14 1 3 13 6 lsatlssel ⊢ ( 𝜑 → 𝑄 ∈ 𝑆 )
15 1 3 13 7 lsatlssel ⊢ ( 𝜑 → 𝑅 ∈ 𝑆 )
16 1 2 lsmcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑄 ∈ 𝑆 ∧ 𝑅 ∈ 𝑆 ) → ( 𝑄 ⊕ 𝑅 ) ∈ 𝑆 )
17 13 14 15 16 syl3anc ⊢ ( 𝜑 → ( 𝑄 ⊕ 𝑅 ) ∈ 𝑆 )
18 1 lssincl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ ( 𝑄 ⊕ 𝑅 ) ∈ 𝑆 ) → ( 𝑈 ∩ ( 𝑄 ⊕ 𝑅 ) ) ∈ 𝑆 )
19 13 5 17 18 syl3anc ⊢ ( 𝜑 → ( 𝑈 ∩ ( 𝑄 ⊕ 𝑅 ) ) ∈ 𝑆 )
20 1 2 3 11 4 5 7 lcv1 ⊢ ( 𝜑 → ( ¬ 𝑅 ⊆ 𝑈 ↔ 𝑈 ( ⋖L ‘ 𝑊 ) ( 𝑈 ⊕ 𝑅 ) ) )
21 9 20 mpbid ⊢ ( 𝜑 → 𝑈 ( ⋖L ‘ 𝑊 ) ( 𝑈 ⊕ 𝑅 ) )
22 lmodabl ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
23 13 22 syl ⊢ ( 𝜑 → 𝑊 ∈ Abel )
24 1 lsssssubg ⊢ ( 𝑊 ∈ LMod → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
25 13 24 syl ⊢ ( 𝜑 → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
26 25 14 sseldd ⊢ ( 𝜑 → 𝑄 ∈ ( SubGrp ‘ 𝑊 ) )
27 25 15 sseldd ⊢ ( 𝜑 → 𝑅 ∈ ( SubGrp ‘ 𝑊 ) )
28 2 lsmcom ⊢ ( ( 𝑊 ∈ Abel ∧ 𝑄 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑅 ∈ ( SubGrp ‘ 𝑊 ) ) → ( 𝑄 ⊕ 𝑅 ) = ( 𝑅 ⊕ 𝑄 ) )
29 23 26 27 28 syl3anc ⊢ ( 𝜑 → ( 𝑄 ⊕ 𝑅 ) = ( 𝑅 ⊕ 𝑄 ) )
30 29 oveq2d ⊢ ( 𝜑 → ( 𝑈 ⊕ ( 𝑄 ⊕ 𝑅 ) ) = ( 𝑈 ⊕ ( 𝑅 ⊕ 𝑄 ) ) )
31 25 5 sseldd ⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
32 2 lsmass ⊢ ( ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑅 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑄 ∈ ( SubGrp ‘ 𝑊 ) ) → ( ( 𝑈 ⊕ 𝑅 ) ⊕ 𝑄 ) = ( 𝑈 ⊕ ( 𝑅 ⊕ 𝑄 ) ) )
33 31 27 26 32 syl3anc ⊢ ( 𝜑 → ( ( 𝑈 ⊕ 𝑅 ) ⊕ 𝑄 ) = ( 𝑈 ⊕ ( 𝑅 ⊕ 𝑄 ) ) )
34 30 33 eqtr4d ⊢ ( 𝜑 → ( 𝑈 ⊕ ( 𝑄 ⊕ 𝑅 ) ) = ( ( 𝑈 ⊕ 𝑅 ) ⊕ 𝑄 ) )
35 1 2 lsmcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑅 ∈ 𝑆 ) → ( 𝑈 ⊕ 𝑅 ) ∈ 𝑆 )
36 13 5 15 35 syl3anc ⊢ ( 𝜑 → ( 𝑈 ⊕ 𝑅 ) ∈ 𝑆 )
37 25 36 sseldd ⊢ ( 𝜑 → ( 𝑈 ⊕ 𝑅 ) ∈ ( SubGrp ‘ 𝑊 ) )
38 2 lsmless2 ⊢ ( ( ( 𝑈 ⊕ 𝑅 ) ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑈 ⊕ 𝑅 ) ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑄 ⊆ ( 𝑈 ⊕ 𝑅 ) ) → ( ( 𝑈 ⊕ 𝑅 ) ⊕ 𝑄 ) ⊆ ( ( 𝑈 ⊕ 𝑅 ) ⊕ ( 𝑈 ⊕ 𝑅 ) ) )
39 37 37 10 38 syl3anc ⊢ ( 𝜑 → ( ( 𝑈 ⊕ 𝑅 ) ⊕ 𝑄 ) ⊆ ( ( 𝑈 ⊕ 𝑅 ) ⊕ ( 𝑈 ⊕ 𝑅 ) ) )
40 34 39 eqsstrd ⊢ ( 𝜑 → ( 𝑈 ⊕ ( 𝑄 ⊕ 𝑅 ) ) ⊆ ( ( 𝑈 ⊕ 𝑅 ) ⊕ ( 𝑈 ⊕ 𝑅 ) ) )
41 2 lsmidm ⊢ ( ( 𝑈 ⊕ 𝑅 ) ∈ ( SubGrp ‘ 𝑊 ) → ( ( 𝑈 ⊕ 𝑅 ) ⊕ ( 𝑈 ⊕ 𝑅 ) ) = ( 𝑈 ⊕ 𝑅 ) )
42 37 41 syl ⊢ ( 𝜑 → ( ( 𝑈 ⊕ 𝑅 ) ⊕ ( 𝑈 ⊕ 𝑅 ) ) = ( 𝑈 ⊕ 𝑅 ) )
43 40 42 sseqtrd ⊢ ( 𝜑 → ( 𝑈 ⊕ ( 𝑄 ⊕ 𝑅 ) ) ⊆ ( 𝑈 ⊕ 𝑅 ) )
44 25 17 sseldd ⊢ ( 𝜑 → ( 𝑄 ⊕ 𝑅 ) ∈ ( SubGrp ‘ 𝑊 ) )
45 2 lsmub2 ⊢ ( ( 𝑄 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑅 ∈ ( SubGrp ‘ 𝑊 ) ) → 𝑅 ⊆ ( 𝑄 ⊕ 𝑅 ) )
46 26 27 45 syl2anc ⊢ ( 𝜑 → 𝑅 ⊆ ( 𝑄 ⊕ 𝑅 ) )
47 2 lsmless2 ⊢ ( ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑄 ⊕ 𝑅 ) ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑅 ⊆ ( 𝑄 ⊕ 𝑅 ) ) → ( 𝑈 ⊕ 𝑅 ) ⊆ ( 𝑈 ⊕ ( 𝑄 ⊕ 𝑅 ) ) )
48 31 44 46 47 syl3anc ⊢ ( 𝜑 → ( 𝑈 ⊕ 𝑅 ) ⊆ ( 𝑈 ⊕ ( 𝑄 ⊕ 𝑅 ) ) )
49 43 48 eqssd ⊢ ( 𝜑 → ( 𝑈 ⊕ ( 𝑄 ⊕ 𝑅 ) ) = ( 𝑈 ⊕ 𝑅 ) )
50 21 49 breqtrrd ⊢ ( 𝜑 → 𝑈 ( ⋖L ‘ 𝑊 ) ( 𝑈 ⊕ ( 𝑄 ⊕ 𝑅 ) ) )
51 1 2 11 13 5 17 50 lcvexchlem4 ⊢ ( 𝜑 → ( 𝑈 ∩ ( 𝑄 ⊕ 𝑅 ) ) ( ⋖L ‘ 𝑊 ) ( 𝑄 ⊕ 𝑅 ) )
52 1 2 3 11 4 19 6 7 8 51 lsatcvat2 ⊢ ( 𝜑 → ( 𝑈 ∩ ( 𝑄 ⊕ 𝑅 ) ) ∈ 𝐴 )