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	⊢ ( 𝜑 → ( 𝑈 ∩ ( 𝑄 ⊕ 𝑅 ) ) ∈ 𝐴 )