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 + ˙ = + W
lsmspsn.f F = Scalar W
lsmspsn.k K = Base F
lsmspsn.t · ˙ = W
lsmspsn.p ˙ = LSSum W
lsmspsn.n N = LSpan W
lsmspsn.w φ W LMod
lsmspsn.x φ X V
lsmspsn.y φ Y V
Assertion lsmspsn φ U N X ˙ N Y j K k K U = j · ˙ X + ˙ k · ˙ Y

Proof

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