# Metamath Proof Explorer

## Theorem lsslsp

Description: Spans in submodules correspond to spans in the containing module. (Contributed by Stefan O'Rear, 12-Dec-2014) TODO: Shouldn't we swap MG and NG since we are computing a property of NG ? (Like we say sin 0 = 0 and not 0 = sin 0.) - NM 15-Mar-2015.

Ref Expression
Hypotheses lsslsp.x ${⊢}{X}={W}{↾}_{𝑠}{U}$
lsslsp.m ${⊢}{M}=\mathrm{LSpan}\left({W}\right)$
lsslsp.n ${⊢}{N}=\mathrm{LSpan}\left({X}\right)$
lsslsp.l ${⊢}{L}=\mathrm{LSubSp}\left({W}\right)$
Assertion lsslsp ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {L}\wedge {G}\subseteq {U}\right)\to {M}\left({G}\right)={N}\left({G}\right)$

### Proof

Step Hyp Ref Expression
1 lsslsp.x ${⊢}{X}={W}{↾}_{𝑠}{U}$
2 lsslsp.m ${⊢}{M}=\mathrm{LSpan}\left({W}\right)$
3 lsslsp.n ${⊢}{N}=\mathrm{LSpan}\left({X}\right)$
4 lsslsp.l ${⊢}{L}=\mathrm{LSubSp}\left({W}\right)$
5 simp1 ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {L}\wedge {G}\subseteq {U}\right)\to {W}\in \mathrm{LMod}$
6 1 4 lsslmod ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {L}\right)\to {X}\in \mathrm{LMod}$
7 6 3adant3 ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {L}\wedge {G}\subseteq {U}\right)\to {X}\in \mathrm{LMod}$
8 simp3 ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {L}\wedge {G}\subseteq {U}\right)\to {G}\subseteq {U}$
9 eqid ${⊢}{\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{W}}$
10 9 4 lssss ${⊢}{U}\in {L}\to {U}\subseteq {\mathrm{Base}}_{{W}}$
11 10 3ad2ant2 ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {L}\wedge {G}\subseteq {U}\right)\to {U}\subseteq {\mathrm{Base}}_{{W}}$
12 1 9 ressbas2 ${⊢}{U}\subseteq {\mathrm{Base}}_{{W}}\to {U}={\mathrm{Base}}_{{X}}$
13 11 12 syl ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {L}\wedge {G}\subseteq {U}\right)\to {U}={\mathrm{Base}}_{{X}}$
14 8 13 sseqtrd ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {L}\wedge {G}\subseteq {U}\right)\to {G}\subseteq {\mathrm{Base}}_{{X}}$
15 eqid ${⊢}{\mathrm{Base}}_{{X}}={\mathrm{Base}}_{{X}}$
16 eqid ${⊢}\mathrm{LSubSp}\left({X}\right)=\mathrm{LSubSp}\left({X}\right)$
17 15 16 3 lspcl ${⊢}\left({X}\in \mathrm{LMod}\wedge {G}\subseteq {\mathrm{Base}}_{{X}}\right)\to {N}\left({G}\right)\in \mathrm{LSubSp}\left({X}\right)$
18 7 14 17 syl2anc ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {L}\wedge {G}\subseteq {U}\right)\to {N}\left({G}\right)\in \mathrm{LSubSp}\left({X}\right)$
19 1 4 16 lsslss ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {L}\right)\to \left({N}\left({G}\right)\in \mathrm{LSubSp}\left({X}\right)↔\left({N}\left({G}\right)\in {L}\wedge {N}\left({G}\right)\subseteq {U}\right)\right)$
20 19 3adant3 ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {L}\wedge {G}\subseteq {U}\right)\to \left({N}\left({G}\right)\in \mathrm{LSubSp}\left({X}\right)↔\left({N}\left({G}\right)\in {L}\wedge {N}\left({G}\right)\subseteq {U}\right)\right)$
21 18 20 mpbid ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {L}\wedge {G}\subseteq {U}\right)\to \left({N}\left({G}\right)\in {L}\wedge {N}\left({G}\right)\subseteq {U}\right)$
22 21 simpld ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {L}\wedge {G}\subseteq {U}\right)\to {N}\left({G}\right)\in {L}$
23 15 3 lspssid ${⊢}\left({X}\in \mathrm{LMod}\wedge {G}\subseteq {\mathrm{Base}}_{{X}}\right)\to {G}\subseteq {N}\left({G}\right)$
24 7 14 23 syl2anc ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {L}\wedge {G}\subseteq {U}\right)\to {G}\subseteq {N}\left({G}\right)$
25 4 2 lspssp ${⊢}\left({W}\in \mathrm{LMod}\wedge {N}\left({G}\right)\in {L}\wedge {G}\subseteq {N}\left({G}\right)\right)\to {M}\left({G}\right)\subseteq {N}\left({G}\right)$
26 5 22 24 25 syl3anc ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {L}\wedge {G}\subseteq {U}\right)\to {M}\left({G}\right)\subseteq {N}\left({G}\right)$
27 8 11 sstrd ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {L}\wedge {G}\subseteq {U}\right)\to {G}\subseteq {\mathrm{Base}}_{{W}}$
28 9 4 2 lspcl ${⊢}\left({W}\in \mathrm{LMod}\wedge {G}\subseteq {\mathrm{Base}}_{{W}}\right)\to {M}\left({G}\right)\in {L}$
29 5 27 28 syl2anc ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {L}\wedge {G}\subseteq {U}\right)\to {M}\left({G}\right)\in {L}$
30 4 2 lspssp ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {L}\wedge {G}\subseteq {U}\right)\to {M}\left({G}\right)\subseteq {U}$
31 1 4 16 lsslss ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {L}\right)\to \left({M}\left({G}\right)\in \mathrm{LSubSp}\left({X}\right)↔\left({M}\left({G}\right)\in {L}\wedge {M}\left({G}\right)\subseteq {U}\right)\right)$
32 31 3adant3 ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {L}\wedge {G}\subseteq {U}\right)\to \left({M}\left({G}\right)\in \mathrm{LSubSp}\left({X}\right)↔\left({M}\left({G}\right)\in {L}\wedge {M}\left({G}\right)\subseteq {U}\right)\right)$
33 29 30 32 mpbir2and ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {L}\wedge {G}\subseteq {U}\right)\to {M}\left({G}\right)\in \mathrm{LSubSp}\left({X}\right)$
34 9 2 lspssid ${⊢}\left({W}\in \mathrm{LMod}\wedge {G}\subseteq {\mathrm{Base}}_{{W}}\right)\to {G}\subseteq {M}\left({G}\right)$
35 5 27 34 syl2anc ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {L}\wedge {G}\subseteq {U}\right)\to {G}\subseteq {M}\left({G}\right)$
36 16 3 lspssp ${⊢}\left({X}\in \mathrm{LMod}\wedge {M}\left({G}\right)\in \mathrm{LSubSp}\left({X}\right)\wedge {G}\subseteq {M}\left({G}\right)\right)\to {N}\left({G}\right)\subseteq {M}\left({G}\right)$
37 7 33 35 36 syl3anc ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {L}\wedge {G}\subseteq {U}\right)\to {N}\left({G}\right)\subseteq {M}\left({G}\right)$
38 26 37 eqssd ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {L}\wedge {G}\subseteq {U}\right)\to {M}\left({G}\right)={N}\left({G}\right)$