lsatcvat

Description: A nonzero subspace less than the sum of two atoms is an atom. ( atcvati analog.) (Contributed by NM, 10-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lsatcvat.o	⊢ 0 = ( 0_g ‘ 𝑊 )
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	5	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑄 ⊆ 𝑈 ) → 𝑊 ∈ LVec )
12	6	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑄 ⊆ 𝑈 ) → 𝑈 ∈ 𝑆 )
13	7	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑄 ⊆ 𝑈 ) → 𝑄 ∈ 𝐴 )
14	8	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑄 ⊆ 𝑈 ) → 𝑅 ∈ 𝐴 )
15	9	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑄 ⊆ 𝑈 ) → 𝑈 ≠ { 0 } )
16	10	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑄 ⊆ 𝑈 ) → 𝑈 ⊊ ( 𝑄 ⊕ 𝑅 ) )
17		simpr	⊢ ( ( 𝜑 ∧ ¬ 𝑄 ⊆ 𝑈 ) → ¬ 𝑄 ⊆ 𝑈 )
18	1 2 3 4 11 12 13 14 15 16 17	lsatcvatlem	⊢ ( ( 𝜑 ∧ ¬ 𝑄 ⊆ 𝑈 ) → 𝑈 ∈ 𝐴 )
19	5	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ⊆ 𝑈 ) → 𝑊 ∈ LVec )
20	6	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ⊆ 𝑈 ) → 𝑈 ∈ 𝑆 )
21	8	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ⊆ 𝑈 ) → 𝑅 ∈ 𝐴 )
22	7	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ⊆ 𝑈 ) → 𝑄 ∈ 𝐴 )
23	9	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ⊆ 𝑈 ) → 𝑈 ≠ { 0 } )
24		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
25	5 24	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
26		lmodabl	⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
27	25 26	syl	⊢ ( 𝜑 → 𝑊 ∈ Abel )
28	2	lsssssubg	⊢ ( 𝑊 ∈ LMod → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
29	25 28	syl	⊢ ( 𝜑 → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
30	2 4 25 7	lsatlssel	⊢ ( 𝜑 → 𝑄 ∈ 𝑆 )
31	29 30	sseldd	⊢ ( 𝜑 → 𝑄 ∈ ( SubGrp ‘ 𝑊 ) )
32	2 4 25 8	lsatlssel	⊢ ( 𝜑 → 𝑅 ∈ 𝑆 )
33	29 32	sseldd	⊢ ( 𝜑 → 𝑅 ∈ ( SubGrp ‘ 𝑊 ) )
34	3	lsmcom	⊢ ( ( 𝑊 ∈ Abel ∧ 𝑄 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑅 ∈ ( SubGrp ‘ 𝑊 ) ) → ( 𝑄 ⊕ 𝑅 ) = ( 𝑅 ⊕ 𝑄 ) )
35	27 31 33 34	syl3anc	⊢ ( 𝜑 → ( 𝑄 ⊕ 𝑅 ) = ( 𝑅 ⊕ 𝑄 ) )
36	35	psseq2d	⊢ ( 𝜑 → ( 𝑈 ⊊ ( 𝑄 ⊕ 𝑅 ) ↔ 𝑈 ⊊ ( 𝑅 ⊕ 𝑄 ) ) )
37	10 36	mpbid	⊢ ( 𝜑 → 𝑈 ⊊ ( 𝑅 ⊕ 𝑄 ) )
38	37	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ⊆ 𝑈 ) → 𝑈 ⊊ ( 𝑅 ⊕ 𝑄 ) )
39		simpr	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ⊆ 𝑈 ) → ¬ 𝑅 ⊆ 𝑈 )
40	1 2 3 4 19 20 21 22 23 38 39	lsatcvatlem	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ⊆ 𝑈 ) → 𝑈 ∈ 𝐴 )
41	29 6	sseldd	⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
42	3	lsmlub	⊢ ( ( 𝑄 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑅 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ) → ( ( 𝑄 ⊆ 𝑈 ∧ 𝑅 ⊆ 𝑈 ) ↔ ( 𝑄 ⊕ 𝑅 ) ⊆ 𝑈 ) )
43	31 33 41 42	syl3anc	⊢ ( 𝜑 → ( ( 𝑄 ⊆ 𝑈 ∧ 𝑅 ⊆ 𝑈 ) ↔ ( 𝑄 ⊕ 𝑅 ) ⊆ 𝑈 ) )
44		ssnpss	⊢ ( ( 𝑄 ⊕ 𝑅 ) ⊆ 𝑈 → ¬ 𝑈 ⊊ ( 𝑄 ⊕ 𝑅 ) )
45	43 44	biimtrdi	⊢ ( 𝜑 → ( ( 𝑄 ⊆ 𝑈 ∧ 𝑅 ⊆ 𝑈 ) → ¬ 𝑈 ⊊ ( 𝑄 ⊕ 𝑅 ) ) )
46	45	con2d	⊢ ( 𝜑 → ( 𝑈 ⊊ ( 𝑄 ⊕ 𝑅 ) → ¬ ( 𝑄 ⊆ 𝑈 ∧ 𝑅 ⊆ 𝑈 ) ) )
47		ianor	⊢ ( ¬ ( 𝑄 ⊆ 𝑈 ∧ 𝑅 ⊆ 𝑈 ) ↔ ( ¬ 𝑄 ⊆ 𝑈 ∨ ¬ 𝑅 ⊆ 𝑈 ) )
48	46 47	imbitrdi	⊢ ( 𝜑 → ( 𝑈 ⊊ ( 𝑄 ⊕ 𝑅 ) → ( ¬ 𝑄 ⊆ 𝑈 ∨ ¬ 𝑅 ⊆ 𝑈 ) ) )
49	10 48	mpd	⊢ ( 𝜑 → ( ¬ 𝑄 ⊆ 𝑈 ∨ ¬ 𝑅 ⊆ 𝑈 ) )
50	18 40 49	mpjaodan	⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )

Metamath Proof Explorer

Theorem lsatcvat

Proof