Metamath Proof Explorer

Theorem lsmsatcv

Description: Subspace sum has the covering property (using spans of singletons to represent atoms). Similar to Exercise 5 of Kalmbach p. 153. ( spansncvi analog.) Explicit atom version of lsmcv . (Contributed by NM, 29-Oct-2014)

Ref Expression
Hypotheses lsmsatcv.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lsmsatcv.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
lsmsatcv.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
lsmsatcv.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lsmsatcv.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
lsmsatcv.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
lsmsatcv.x ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
Assertion lsmsatcv ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ 𝑄 ) ) → 𝑈 = ( 𝑇 ⊕ 𝑄 ) )

Proof

Step Hyp Ref Expression
1 lsmsatcv.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2 lsmsatcv.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
3 lsmsatcv.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
4 lsmsatcv.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
5 lsmsatcv.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
6 lsmsatcv.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
7 lsmsatcv.x ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
8 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
9 eqid ⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
10 8 9 3 islsati ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑄 ∈ 𝐴 ) → ∃ 𝑣 ∈ ( Base ‘ 𝑊 ) 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) )
11 4 7 10 syl2anc ⊢ ( 𝜑 → ∃ 𝑣 ∈ ( Base ‘ 𝑊 ) 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) )
12 4 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → 𝑊 ∈ LVec )
13 5 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → 𝑇 ∈ 𝑆 )
14 6 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → 𝑈 ∈ 𝑆 )
15 simpr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → 𝑣 ∈ ( Base ‘ 𝑊 ) )
16 8 1 9 2 12 13 14 15 lsmcv ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) ) → 𝑈 = ( 𝑇 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) )
17 16 3expib ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → ( ( 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) ) → 𝑈 = ( 𝑇 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) ) )
18 17 3adant3 ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) → ( ( 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) ) → 𝑈 = ( 𝑇 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) ) )
19 oveq2 ⊢ ( 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → ( 𝑇 ⊕ 𝑄 ) = ( 𝑇 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) )
20 19 sseq2d ⊢ ( 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → ( 𝑈 ⊆ ( 𝑇 ⊕ 𝑄 ) ↔ 𝑈 ⊆ ( 𝑇 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) ) )
21 20 anbi2d ⊢ ( 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → ( ( 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ 𝑄 ) ) ↔ ( 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) ) ) )
22 19 eqeq2d ⊢ ( 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → ( 𝑈 = ( 𝑇 ⊕ 𝑄 ) ↔ 𝑈 = ( 𝑇 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) ) )
23 21 22 imbi12d ⊢ ( 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → ( ( ( 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ 𝑄 ) ) → 𝑈 = ( 𝑇 ⊕ 𝑄 ) ) ↔ ( ( 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) ) → 𝑈 = ( 𝑇 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) ) ) )
24 23 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) → ( ( ( 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ 𝑄 ) ) → 𝑈 = ( 𝑇 ⊕ 𝑄 ) ) ↔ ( ( 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) ) → 𝑈 = ( 𝑇 ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) ) ) )
25 18 24 mpbird ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) → ( ( 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ 𝑄 ) ) → 𝑈 = ( 𝑇 ⊕ 𝑄 ) ) )
26 25 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑣 ∈ ( Base ‘ 𝑊 ) 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → ( ( 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ 𝑄 ) ) → 𝑈 = ( 𝑇 ⊕ 𝑄 ) ) ) )
27 11 26 mpd ⊢ ( 𝜑 → ( ( 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ 𝑄 ) ) → 𝑈 = ( 𝑇 ⊕ 𝑄 ) ) )
28 27 3impib ⊢ ( ( 𝜑 ∧ 𝑇 ⊊ 𝑈 ∧ 𝑈 ⊆ ( 𝑇 ⊕ 𝑄 ) ) → 𝑈 = ( 𝑇 ⊕ 𝑄 ) )