Theorem lssats2

Description: A way to express atomisticity (a subspace is the union of its atoms). (Contributed by NM, 3-Feb-2015)

	Ref	Expression
Hypotheses	lssats2.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
	lssats2.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	lssats2.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	lssats2.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
Assertion	lssats2	⊢ ( 𝜑 → 𝑈 = ∪ 𝑥 ∈ 𝑈 ( 𝑁 ‘ { 𝑥 } ) )

Proof

Step	Hyp	Ref	Expression
1		lssats2.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2		lssats2.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3		lssats2.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
4		lssats2.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
5		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑈 ) → 𝑦 ∈ 𝑈 )
6	3	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑈 ) → 𝑊 ∈ LMod )
7		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
8	7 1	lssel	⊢ ( ( 𝑈 ∈ 𝑆 ∧ 𝑦 ∈ 𝑈 ) → 𝑦 ∈ ( Base ‘ 𝑊 ) )
9	4 8	sylan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑈 ) → 𝑦 ∈ ( Base ‘ 𝑊 ) )
10	7 2	lspsnid	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → 𝑦 ∈ ( 𝑁 ‘ { 𝑦 } ) )
11	6 9 10	syl2anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑈 ) → 𝑦 ∈ ( 𝑁 ‘ { 𝑦 } ) )
12		sneq	⊢ ( 𝑥 = 𝑦 → { 𝑥 } = { 𝑦 } )
13	12	fveq2d	⊢ ( 𝑥 = 𝑦 → ( 𝑁 ‘ { 𝑥 } ) = ( 𝑁 ‘ { 𝑦 } ) )
14	13	eleq2d	⊢ ( 𝑥 = 𝑦 → ( 𝑦 ∈ ( 𝑁 ‘ { 𝑥 } ) ↔ 𝑦 ∈ ( 𝑁 ‘ { 𝑦 } ) ) )
15	14	rspcev	⊢ ( ( 𝑦 ∈ 𝑈 ∧ 𝑦 ∈ ( 𝑁 ‘ { 𝑦 } ) ) → ∃ 𝑥 ∈ 𝑈 𝑦 ∈ ( 𝑁 ‘ { 𝑥 } ) )
16	5 11 15	syl2anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑈 ) → ∃ 𝑥 ∈ 𝑈 𝑦 ∈ ( 𝑁 ‘ { 𝑥 } ) )
17	16	ex	⊢ ( 𝜑 → ( 𝑦 ∈ 𝑈 → ∃ 𝑥 ∈ 𝑈 𝑦 ∈ ( 𝑁 ‘ { 𝑥 } ) ) )
18	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → 𝑊 ∈ LMod )
19	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → 𝑈 ∈ 𝑆 )
20		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ∈ 𝑈 )
21	1 2 18 19 20	lspsnel5a	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → ( 𝑁 ‘ { 𝑥 } ) ⊆ 𝑈 )
22	21	sseld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → ( 𝑦 ∈ ( 𝑁 ‘ { 𝑥 } ) → 𝑦 ∈ 𝑈 ) )
23	22	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑈 𝑦 ∈ ( 𝑁 ‘ { 𝑥 } ) → 𝑦 ∈ 𝑈 ) )
24	17 23	impbid	⊢ ( 𝜑 → ( 𝑦 ∈ 𝑈 ↔ ∃ 𝑥 ∈ 𝑈 𝑦 ∈ ( 𝑁 ‘ { 𝑥 } ) ) )
25		eliun	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝑈 ( 𝑁 ‘ { 𝑥 } ) ↔ ∃ 𝑥 ∈ 𝑈 𝑦 ∈ ( 𝑁 ‘ { 𝑥 } ) )
26	24 25	bitr4di	⊢ ( 𝜑 → ( 𝑦 ∈ 𝑈 ↔ 𝑦 ∈ ∪ 𝑥 ∈ 𝑈 ( 𝑁 ‘ { 𝑥 } ) ) )
27	26	eqrdv	⊢ ( 𝜑 → 𝑈 = ∪ 𝑥 ∈ 𝑈 ( 𝑁 ‘ { 𝑥 } ) )