Metamath Proof Explorer

Theorem lsslsp

Description: Spans in submodules correspond to spans in the containing module. (Contributed by Stefan O'Rear, 12-Dec-2014) Terms in the equation were swapped as proposed by NM on 15-Mar-2015. (Revised by AV, 18-Apr-2025)

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