lssatomic

Description: The lattice of subspaces is atomic, i.e. any nonzero element is greater than or equal to some atom. ( shatomici analog.) (Contributed by NM, 10-Jan-2015)

	Ref	Expression
Hypotheses	lssatomic.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
	lssatomic.o	⊢ 0 = ( 0_g ‘ 𝑊 )
	lssatomic.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
	lssatomic.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	lssatomic.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
	lssatomic.n	⊢ ( 𝜑 → 𝑈 ≠ { 0 } )
Assertion	lssatomic	⊢ ( 𝜑 → ∃ 𝑞 ∈ 𝐴 𝑞 ⊆ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		lssatomic.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2		lssatomic.o	⊢ 0 = ( 0_g ‘ 𝑊 )
3		lssatomic.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
4		lssatomic.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
5		lssatomic.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
6		lssatomic.n	⊢ ( 𝜑 → 𝑈 ≠ { 0 } )
7	2 1	lssne0	⊢ ( 𝑈 ∈ 𝑆 → ( 𝑈 ≠ { 0 } ↔ ∃ 𝑥 ∈ 𝑈 𝑥 ≠ 0 ) )
8	5 7	syl	⊢ ( 𝜑 → ( 𝑈 ≠ { 0 } ↔ ∃ 𝑥 ∈ 𝑈 𝑥 ≠ 0 ) )
9	6 8	mpbid	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑈 𝑥 ≠ 0 )
10	4	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ∧ 𝑥 ≠ 0 ) → 𝑊 ∈ LMod )
11	5	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ∧ 𝑥 ≠ 0 ) → 𝑈 ∈ 𝑆 )
12		simp2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ∧ 𝑥 ≠ 0 ) → 𝑥 ∈ 𝑈 )
13		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
14	13 1	lssel	⊢ ( ( 𝑈 ∈ 𝑆 ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
15	11 12 14	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ∧ 𝑥 ≠ 0 ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
16		simp3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ∧ 𝑥 ≠ 0 ) → 𝑥 ≠ 0 )
17		eqid	⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
18	13 17 2 3	lsatlspsn2	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑥 ≠ 0 ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ∈ 𝐴 )
19	10 15 16 18	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ∧ 𝑥 ≠ 0 ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ∈ 𝐴 )
20	1 17 10 11 12	lspsnel5a	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ∧ 𝑥 ≠ 0 ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ⊆ 𝑈 )
21		sseq1	⊢ ( 𝑞 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) → ( 𝑞 ⊆ 𝑈 ↔ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ⊆ 𝑈 ) )
22	21	rspcev	⊢ ( ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ∈ 𝐴 ∧ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑥 } ) ⊆ 𝑈 ) → ∃ 𝑞 ∈ 𝐴 𝑞 ⊆ 𝑈 )
23	19 20 22	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ∧ 𝑥 ≠ 0 ) → ∃ 𝑞 ∈ 𝐴 𝑞 ⊆ 𝑈 )
24	23	rexlimdv3a	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑈 𝑥 ≠ 0 → ∃ 𝑞 ∈ 𝐴 𝑞 ⊆ 𝑈 ) )
25	9 24	mpd	⊢ ( 𝜑 → ∃ 𝑞 ∈ 𝐴 𝑞 ⊆ 𝑈 )

Metamath Proof Explorer

Theorem lssatomic

Proof