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 
|- S = ( LSubSp ` W )
lsmsatcv.p 
|- .(+) = ( LSSum ` W )
lsmsatcv.a 
|- A = ( LSAtoms ` W )
lsmsatcv.w 
|- ( ph -> W e. LVec )
lsmsatcv.t 
|- ( ph -> T e. S )
lsmsatcv.u 
|- ( ph -> U e. S )
lsmsatcv.x 
|- ( ph -> Q e. A )
Assertion lsmsatcv 
|- ( ( ph /\ T C. U /\ U C_ ( T .(+) Q ) ) -> U = ( T .(+) Q ) )

Proof

Step Hyp Ref Expression
1 lsmsatcv.s 
 |-  S = ( LSubSp ` W )
2 lsmsatcv.p 
 |-  .(+) = ( LSSum ` W )
3 lsmsatcv.a 
 |-  A = ( LSAtoms ` W )
4 lsmsatcv.w 
 |-  ( ph -> W e. LVec )
5 lsmsatcv.t 
 |-  ( ph -> T e. S )
6 lsmsatcv.u 
 |-  ( ph -> U e. S )
7 lsmsatcv.x 
 |-  ( ph -> Q e. A )
8 eqid 
 |-  ( Base ` W ) = ( Base ` W )
9 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
10 8 9 3 islsati 
 |-  ( ( W e. LVec /\ Q e. A ) -> E. v e. ( Base ` W ) Q = ( ( LSpan ` W ) ` { v } ) )
11 4 7 10 syl2anc 
 |-  ( ph -> E. v e. ( Base ` W ) Q = ( ( LSpan ` W ) ` { v } ) )
12 4 adantr 
 |-  ( ( ph /\ v e. ( Base ` W ) ) -> W e. LVec )
13 5 adantr 
 |-  ( ( ph /\ v e. ( Base ` W ) ) -> T e. S )
14 6 adantr 
 |-  ( ( ph /\ v e. ( Base ` W ) ) -> U e. S )
15 simpr 
 |-  ( ( ph /\ v e. ( Base ` W ) ) -> v e. ( Base ` W ) )
16 8 1 9 2 12 13 14 15 lsmcv 
 |-  ( ( ( ph /\ v e. ( Base ` W ) ) /\ T C. U /\ U C_ ( T .(+) ( ( LSpan ` W ) ` { v } ) ) ) -> U = ( T .(+) ( ( LSpan ` W ) ` { v } ) ) )
17 16 3expib 
 |-  ( ( ph /\ v e. ( Base ` W ) ) -> ( ( T C. U /\ U C_ ( T .(+) ( ( LSpan ` W ) ` { v } ) ) ) -> U = ( T .(+) ( ( LSpan ` W ) ` { v } ) ) ) )
18 17 3adant3 
 |-  ( ( ph /\ v e. ( Base ` W ) /\ Q = ( ( LSpan ` W ) ` { v } ) ) -> ( ( T C. U /\ U C_ ( T .(+) ( ( LSpan ` W ) ` { v } ) ) ) -> U = ( T .(+) ( ( LSpan ` W ) ` { v } ) ) ) )
19 oveq2 
 |-  ( Q = ( ( LSpan ` W ) ` { v } ) -> ( T .(+) Q ) = ( T .(+) ( ( LSpan ` W ) ` { v } ) ) )
20 19 sseq2d 
 |-  ( Q = ( ( LSpan ` W ) ` { v } ) -> ( U C_ ( T .(+) Q ) <-> U C_ ( T .(+) ( ( LSpan ` W ) ` { v } ) ) ) )
21 20 anbi2d 
 |-  ( Q = ( ( LSpan ` W ) ` { v } ) -> ( ( T C. U /\ U C_ ( T .(+) Q ) ) <-> ( T C. U /\ U C_ ( T .(+) ( ( LSpan ` W ) ` { v } ) ) ) ) )
22 19 eqeq2d 
 |-  ( Q = ( ( LSpan ` W ) ` { v } ) -> ( U = ( T .(+) Q ) <-> U = ( T .(+) ( ( LSpan ` W ) ` { v } ) ) ) )
23 21 22 imbi12d 
 |-  ( Q = ( ( LSpan ` W ) ` { v } ) -> ( ( ( T C. U /\ U C_ ( T .(+) Q ) ) -> U = ( T .(+) Q ) ) <-> ( ( T C. U /\ U C_ ( T .(+) ( ( LSpan ` W ) ` { v } ) ) ) -> U = ( T .(+) ( ( LSpan ` W ) ` { v } ) ) ) ) )
24 23 3ad2ant3 
 |-  ( ( ph /\ v e. ( Base ` W ) /\ Q = ( ( LSpan ` W ) ` { v } ) ) -> ( ( ( T C. U /\ U C_ ( T .(+) Q ) ) -> U = ( T .(+) Q ) ) <-> ( ( T C. U /\ U C_ ( T .(+) ( ( LSpan ` W ) ` { v } ) ) ) -> U = ( T .(+) ( ( LSpan ` W ) ` { v } ) ) ) ) )
25 18 24 mpbird 
 |-  ( ( ph /\ v e. ( Base ` W ) /\ Q = ( ( LSpan ` W ) ` { v } ) ) -> ( ( T C. U /\ U C_ ( T .(+) Q ) ) -> U = ( T .(+) Q ) ) )
26 25 rexlimdv3a 
 |-  ( ph -> ( E. v e. ( Base ` W ) Q = ( ( LSpan ` W ) ` { v } ) -> ( ( T C. U /\ U C_ ( T .(+) Q ) ) -> U = ( T .(+) Q ) ) ) )
27 11 26 mpd 
 |-  ( ph -> ( ( T C. U /\ U C_ ( T .(+) Q ) ) -> U = ( T .(+) Q ) ) )
28 27 3impib 
 |-  ( ( ph /\ T C. U /\ U C_ ( T .(+) Q ) ) -> U = ( T .(+) Q ) )