Metamath Proof Explorer


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 ( 𝜑𝑈 = 𝑥𝑈 ( 𝑁 ‘ { 𝑥 } ) )