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}={\mathrm{Base}}_{{W}}$
lsmspsn.a
lsmspsn.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
lsmspsn.k ${⊢}{K}={\mathrm{Base}}_{{F}}$
lsmspsn.t
lsmspsn.p
lsmspsn.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
lsmspsn.w ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
lsmspsn.x ${⊢}{\phi }\to {X}\in {V}$
lsmspsn.y ${⊢}{\phi }\to {Y}\in {V}$
Assertion lsmspsn

Proof

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