Metamath Proof Explorer

Theorem lsmspsn

Description: Member of subspace sum of spans of singletons. (Contributed by NM, 8-Apr-2015)

Ref Expression
Hypotheses lsmspsn.v 
|- V = ( Base ` W )
lsmspsn.a 
|- .+ = ( +g ` W )
lsmspsn.f 
|- F = ( Scalar ` W )
lsmspsn.k 
|- K = ( Base ` F )
lsmspsn.t 
|- .x. = ( .s ` W )
lsmspsn.p 
|- .(+) = ( LSSum ` W )
lsmspsn.n 
|- N = ( LSpan ` W )
lsmspsn.w 
|- ( ph -> W e. LMod )
lsmspsn.x 
|- ( ph -> X e. V )
lsmspsn.y 
|- ( ph -> Y e. V )
Assertion lsmspsn 
|- ( ph -> ( U e. ( ( N ` { X } ) .(+) ( N ` { Y } ) ) <-> E. j e. K E. k e. K U = ( ( j .x. X ) .+ ( k .x. Y ) ) ) )

Proof

Step Hyp Ref Expression
1 lsmspsn.v 
 |-  V = ( Base ` W )
2 lsmspsn.a 
 |-  .+ = ( +g ` W )
3 lsmspsn.f 
 |-  F = ( Scalar ` W )
4 lsmspsn.k 
 |-  K = ( Base ` F )
5 lsmspsn.t 
 |-  .x. = ( .s ` W )
6 lsmspsn.p 
 |-  .(+) = ( LSSum ` W )
7 lsmspsn.n 
 |-  N = ( LSpan ` W )
8 lsmspsn.w 
 |-  ( ph -> W e. LMod )
9 lsmspsn.x 
 |-  ( ph -> X e. V )
10 lsmspsn.y 
 |-  ( ph -> Y e. V )
11 1 7 lspsnsubg 
 |-  ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) e. ( SubGrp ` W ) )
12 8 9 11 syl2anc 
 |-  ( ph -> ( N ` { X } ) e. ( SubGrp ` W ) )
13 1 7 lspsnsubg 
 |-  ( ( W e. LMod /\ Y e. V ) -> ( N ` { Y } ) e. ( SubGrp ` W ) )
14 8 10 13 syl2anc 
 |-  ( ph -> ( N ` { Y } ) e. ( SubGrp ` W ) )
15 2 6 lsmelval 
 |-  ( ( ( N ` { X } ) e. ( SubGrp ` W ) /\ ( N ` { Y } ) e. ( SubGrp ` W ) ) -> ( U e. ( ( N ` { X } ) .(+) ( N ` { Y } ) ) <-> E. v e. ( N ` { X } ) E. w e. ( N ` { Y } ) U = ( v .+ w ) ) )
16 12 14 15 syl2anc 
 |-  ( ph -> ( U e. ( ( N ` { X } ) .(+) ( N ` { Y } ) ) <-> E. v e. ( N ` { X } ) E. w e. ( N ` { Y } ) U = ( v .+ w ) ) )
17 3 4 1 5 7 lspsnel 
 |-  ( ( W e. LMod /\ X e. V ) -> ( v e. ( N ` { X } ) <-> E. j e. K v = ( j .x. X ) ) )
18 8 9 17 syl2anc 
 |-  ( ph -> ( v e. ( N ` { X } ) <-> E. j e. K v = ( j .x. X ) ) )
19 3 4 1 5 7 lspsnel 
 |-  ( ( W e. LMod /\ Y e. V ) -> ( w e. ( N ` { Y } ) <-> E. k e. K w = ( k .x. Y ) ) )
20 8 10 19 syl2anc 
 |-  ( ph -> ( w e. ( N ` { Y } ) <-> E. k e. K w = ( k .x. Y ) ) )
21 18 20 anbi12d 
 |-  ( ph -> ( ( v e. ( N ` { X } ) /\ w e. ( N ` { Y } ) ) <-> ( E. j e. K v = ( j .x. X ) /\ E. k e. K w = ( k .x. Y ) ) ) )
22 21 biimpa 
 |-  ( ( ph /\ ( v e. ( N ` { X } ) /\ w e. ( N ` { Y } ) ) ) -> ( E. j e. K v = ( j .x. X ) /\ E. k e. K w = ( k .x. Y ) ) )
23 22 biantrurd 
 |-  ( ( ph /\ ( v e. ( N ` { X } ) /\ w e. ( N ` { Y } ) ) ) -> ( U = ( v .+ w ) <-> ( ( E. j e. K v = ( j .x. X ) /\ E. k e. K w = ( k .x. Y ) ) /\ U = ( v .+ w ) ) ) )
24 r19.41v 
 |-  ( E. k e. K ( ( v = ( j .x. X ) /\ w = ( k .x. Y ) ) /\ U = ( v .+ w ) ) <-> ( E. k e. K ( v = ( j .x. X ) /\ w = ( k .x. Y ) ) /\ U = ( v .+ w ) ) )
25 24 rexbii 
 |-  ( E. j e. K E. k e. K ( ( v = ( j .x. X ) /\ w = ( k .x. Y ) ) /\ U = ( v .+ w ) ) <-> E. j e. K ( E. k e. K ( v = ( j .x. X ) /\ w = ( k .x. Y ) ) /\ U = ( v .+ w ) ) )
26 r19.41v 
 |-  ( E. j e. K ( E. k e. K ( v = ( j .x. X ) /\ w = ( k .x. Y ) ) /\ U = ( v .+ w ) ) <-> ( E. j e. K E. k e. K ( v = ( j .x. X ) /\ w = ( k .x. Y ) ) /\ U = ( v .+ w ) ) )
27 reeanv 
 |-  ( E. j e. K E. k e. K ( v = ( j .x. X ) /\ w = ( k .x. Y ) ) <-> ( E. j e. K v = ( j .x. X ) /\ E. k e. K w = ( k .x. Y ) ) )
28 27 anbi1i 
 |-  ( ( E. j e. K E. k e. K ( v = ( j .x. X ) /\ w = ( k .x. Y ) ) /\ U = ( v .+ w ) ) <-> ( ( E. j e. K v = ( j .x. X ) /\ E. k e. K w = ( k .x. Y ) ) /\ U = ( v .+ w ) ) )
29 25 26 28 3bitrri 
 |-  ( ( ( E. j e. K v = ( j .x. X ) /\ E. k e. K w = ( k .x. Y ) ) /\ U = ( v .+ w ) ) <-> E. j e. K E. k e. K ( ( v = ( j .x. X ) /\ w = ( k .x. Y ) ) /\ U = ( v .+ w ) ) )
30 23 29 bitrdi 
 |-  ( ( ph /\ ( v e. ( N ` { X } ) /\ w e. ( N ` { Y } ) ) ) -> ( U = ( v .+ w ) <-> E. j e. K E. k e. K ( ( v = ( j .x. X ) /\ w = ( k .x. Y ) ) /\ U = ( v .+ w ) ) ) )
31 30 2rexbidva 
 |-  ( ph -> ( E. v e. ( N ` { X } ) E. w e. ( N ` { Y } ) U = ( v .+ w ) <-> E. v e. ( N ` { X } ) E. w e. ( N ` { Y } ) E. j e. K E. k e. K ( ( v = ( j .x. X ) /\ w = ( k .x. Y ) ) /\ U = ( v .+ w ) ) ) )
32 rexrot4 
 |-  ( E. v e. ( N ` { X } ) E. w e. ( N ` { Y } ) E. j e. K E. k e. K ( ( v = ( j .x. X ) /\ w = ( k .x. Y ) ) /\ U = ( v .+ w ) ) <-> E. j e. K E. k e. K E. v e. ( N ` { X } ) E. w e. ( N ` { Y } ) ( ( v = ( j .x. X ) /\ w = ( k .x. Y ) ) /\ U = ( v .+ w ) ) )
33 31 32 bitrdi 
 |-  ( ph -> ( E. v e. ( N ` { X } ) E. w e. ( N ` { Y } ) U = ( v .+ w ) <-> E. j e. K E. k e. K E. v e. ( N ` { X } ) E. w e. ( N ` { Y } ) ( ( v = ( j .x. X ) /\ w = ( k .x. Y ) ) /\ U = ( v .+ w ) ) ) )
34 8 adantr 
 |-  ( ( ph /\ ( j e. K /\ k e. K ) ) -> W e. LMod )
35 simprl 
 |-  ( ( ph /\ ( j e. K /\ k e. K ) ) -> j e. K )
36 9 adantr 
 |-  ( ( ph /\ ( j e. K /\ k e. K ) ) -> X e. V )
37 1 5 3 4 7 34 35 36 lspsneli 
 |-  ( ( ph /\ ( j e. K /\ k e. K ) ) -> ( j .x. X ) e. ( N ` { X } ) )
38 simprr 
 |-  ( ( ph /\ ( j e. K /\ k e. K ) ) -> k e. K )
39 10 adantr 
 |-  ( ( ph /\ ( j e. K /\ k e. K ) ) -> Y e. V )
40 1 5 3 4 7 34 38 39 lspsneli 
 |-  ( ( ph /\ ( j e. K /\ k e. K ) ) -> ( k .x. Y ) e. ( N ` { Y } ) )
41 oveq1 
 |-  ( v = ( j .x. X ) -> ( v .+ w ) = ( ( j .x. X ) .+ w ) )
42 41 eqeq2d 
 |-  ( v = ( j .x. X ) -> ( U = ( v .+ w ) <-> U = ( ( j .x. X ) .+ w ) ) )
43 oveq2 
 |-  ( w = ( k .x. Y ) -> ( ( j .x. X ) .+ w ) = ( ( j .x. X ) .+ ( k .x. Y ) ) )
44 43 eqeq2d 
 |-  ( w = ( k .x. Y ) -> ( U = ( ( j .x. X ) .+ w ) <-> U = ( ( j .x. X ) .+ ( k .x. Y ) ) ) )
45 42 44 ceqsrex2v 
 |-  ( ( ( j .x. X ) e. ( N ` { X } ) /\ ( k .x. Y ) e. ( N ` { Y } ) ) -> ( E. v e. ( N ` { X } ) E. w e. ( N ` { Y } ) ( ( v = ( j .x. X ) /\ w = ( k .x. Y ) ) /\ U = ( v .+ w ) ) <-> U = ( ( j .x. X ) .+ ( k .x. Y ) ) ) )
46 37 40 45 syl2anc 
 |-  ( ( ph /\ ( j e. K /\ k e. K ) ) -> ( E. v e. ( N ` { X } ) E. w e. ( N ` { Y } ) ( ( v = ( j .x. X ) /\ w = ( k .x. Y ) ) /\ U = ( v .+ w ) ) <-> U = ( ( j .x. X ) .+ ( k .x. Y ) ) ) )
47 46 2rexbidva 
 |-  ( ph -> ( E. j e. K E. k e. K E. v e. ( N ` { X } ) E. w e. ( N ` { Y } ) ( ( v = ( j .x. X ) /\ w = ( k .x. Y ) ) /\ U = ( v .+ w ) ) <-> E. j e. K E. k e. K U = ( ( j .x. X ) .+ ( k .x. Y ) ) ) )
48 16 33 47 3bitrd 
 |-  ( ph -> ( U e. ( ( N ` { X } ) .(+) ( N ` { Y } ) ) <-> E. j e. K E. k e. K U = ( ( j .x. X ) .+ ( k .x. Y ) ) ) )