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 |`s U )
lsslsp.m 
|- M = ( LSpan ` W )
lsslsp.n 
|- N = ( LSpan ` X )
lsslsp.l 
|- L = ( LSubSp ` W )
Assertion lsslsp 
|- ( ( W e. LMod /\ U e. L /\ G C_ U ) -> ( M ` G ) = ( N ` G ) )

Proof

Step Hyp Ref Expression
1 lsslsp.x 
 |-  X = ( W |`s U )
2 lsslsp.m 
 |-  M = ( LSpan ` W )
3 lsslsp.n 
 |-  N = ( LSpan ` X )
4 lsslsp.l 
 |-  L = ( LSubSp ` W )
5 simp1 
 |-  ( ( W e. LMod /\ U e. L /\ G C_ U ) -> W e. LMod )
6 1 4 lsslmod 
 |-  ( ( W e. LMod /\ U e. L ) -> X e. LMod )
7 6 3adant3 
 |-  ( ( W e. LMod /\ U e. L /\ G C_ U ) -> X e. LMod )
8 simp3 
 |-  ( ( W e. LMod /\ U e. L /\ G C_ U ) -> G C_ U )
9 eqid 
 |-  ( Base ` W ) = ( Base ` W )
10 9 4 lssss 
 |-  ( U e. L -> U C_ ( Base ` W ) )
11 10 3ad2ant2 
 |-  ( ( W e. LMod /\ U e. L /\ G C_ U ) -> U C_ ( Base ` W ) )
12 1 9 ressbas2 
 |-  ( U C_ ( Base ` W ) -> U = ( Base ` X ) )
13 11 12 syl 
 |-  ( ( W e. LMod /\ U e. L /\ G C_ U ) -> U = ( Base ` X ) )
14 8 13 sseqtrd 
 |-  ( ( W e. LMod /\ U e. L /\ G C_ U ) -> G C_ ( Base ` X ) )
15 eqid 
 |-  ( Base ` X ) = ( Base ` X )
16 eqid 
 |-  ( LSubSp ` X ) = ( LSubSp ` X )
17 15 16 3 lspcl 
 |-  ( ( X e. LMod /\ G C_ ( Base ` X ) ) -> ( N ` G ) e. ( LSubSp ` X ) )
18 7 14 17 syl2anc 
 |-  ( ( W e. LMod /\ U e. L /\ G C_ U ) -> ( N ` G ) e. ( LSubSp ` X ) )
19 1 4 16 lsslss 
 |-  ( ( W e. LMod /\ U e. L ) -> ( ( N ` G ) e. ( LSubSp ` X ) <-> ( ( N ` G ) e. L /\ ( N ` G ) C_ U ) ) )
20 19 3adant3 
 |-  ( ( W e. LMod /\ U e. L /\ G C_ U ) -> ( ( N ` G ) e. ( LSubSp ` X ) <-> ( ( N ` G ) e. L /\ ( N ` G ) C_ U ) ) )
21 18 20 mpbid 
 |-  ( ( W e. LMod /\ U e. L /\ G C_ U ) -> ( ( N ` G ) e. L /\ ( N ` G ) C_ U ) )
22 21 simpld 
 |-  ( ( W e. LMod /\ U e. L /\ G C_ U ) -> ( N ` G ) e. L )
23 15 3 lspssid 
 |-  ( ( X e. LMod /\ G C_ ( Base ` X ) ) -> G C_ ( N ` G ) )
24 7 14 23 syl2anc 
 |-  ( ( W e. LMod /\ U e. L /\ G C_ U ) -> G C_ ( N ` G ) )
25 4 2 lspssp 
 |-  ( ( W e. LMod /\ ( N ` G ) e. L /\ G C_ ( N ` G ) ) -> ( M ` G ) C_ ( N ` G ) )
26 5 22 24 25 syl3anc 
 |-  ( ( W e. LMod /\ U e. L /\ G C_ U ) -> ( M ` G ) C_ ( N ` G ) )
27 8 11 sstrd 
 |-  ( ( W e. LMod /\ U e. L /\ G C_ U ) -> G C_ ( Base ` W ) )
28 9 4 2 lspcl 
 |-  ( ( W e. LMod /\ G C_ ( Base ` W ) ) -> ( M ` G ) e. L )
29 5 27 28 syl2anc 
 |-  ( ( W e. LMod /\ U e. L /\ G C_ U ) -> ( M ` G ) e. L )
30 4 2 lspssp 
 |-  ( ( W e. LMod /\ U e. L /\ G C_ U ) -> ( M ` G ) C_ U )
31 1 4 16 lsslss 
 |-  ( ( W e. LMod /\ U e. L ) -> ( ( M ` G ) e. ( LSubSp ` X ) <-> ( ( M ` G ) e. L /\ ( M ` G ) C_ U ) ) )
32 31 3adant3 
 |-  ( ( W e. LMod /\ U e. L /\ G C_ U ) -> ( ( M ` G ) e. ( LSubSp ` X ) <-> ( ( M ` G ) e. L /\ ( M ` G ) C_ U ) ) )
33 29 30 32 mpbir2and 
 |-  ( ( W e. LMod /\ U e. L /\ G C_ U ) -> ( M ` G ) e. ( LSubSp ` X ) )
34 9 2 lspssid 
 |-  ( ( W e. LMod /\ G C_ ( Base ` W ) ) -> G C_ ( M ` G ) )
35 5 27 34 syl2anc 
 |-  ( ( W e. LMod /\ U e. L /\ G C_ U ) -> G C_ ( M ` G ) )
36 16 3 lspssp 
 |-  ( ( X e. LMod /\ ( M ` G ) e. ( LSubSp ` X ) /\ G C_ ( M ` G ) ) -> ( N ` G ) C_ ( M ` G ) )
37 7 33 35 36 syl3anc 
 |-  ( ( W e. LMod /\ U e. L /\ G C_ U ) -> ( N ` G ) C_ ( M ` G ) )
38 26 37 eqssd 
 |-  ( ( W e. LMod /\ U e. L /\ G C_ U ) -> ( M ` G ) = ( N ` G ) )