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 𝑋 = ( 𝑊s 𝑈 )
lsslsp.m 𝑀 = ( LSpan ‘ 𝑊 )
lsslsp.n 𝑁 = ( LSpan ‘ 𝑋 )
lsslsp.l 𝐿 = ( LSubSp ‘ 𝑊 )
Assertion lsslsp ( ( 𝑊 ∈ LMod ∧ 𝑈𝐿𝐺𝑈 ) → ( 𝑁𝐺 ) = ( 𝑀𝐺 ) )

Proof

Step Hyp Ref Expression
1 lsslsp.x 𝑋 = ( 𝑊s 𝑈 )
2 lsslsp.m 𝑀 = ( LSpan ‘ 𝑊 )
3 lsslsp.n 𝑁 = ( LSpan ‘ 𝑋 )
4 lsslsp.l 𝐿 = ( LSubSp ‘ 𝑊 )
5 1 4 lsslmod ( ( 𝑊 ∈ LMod ∧ 𝑈𝐿 ) → 𝑋 ∈ LMod )
6 5 3adant3 ( ( 𝑊 ∈ LMod ∧ 𝑈𝐿𝐺𝑈 ) → 𝑋 ∈ LMod )
7 simp1 ( ( 𝑊 ∈ LMod ∧ 𝑈𝐿𝐺𝑈 ) → 𝑊 ∈ LMod )
8 simp3 ( ( 𝑊 ∈ LMod ∧ 𝑈𝐿𝐺𝑈 ) → 𝐺𝑈 )
9 eqid ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
10 9 4 lssss ( 𝑈𝐿𝑈 ⊆ ( Base ‘ 𝑊 ) )
11 10 3ad2ant2 ( ( 𝑊 ∈ LMod ∧ 𝑈𝐿𝐺𝑈 ) → 𝑈 ⊆ ( Base ‘ 𝑊 ) )
12 8 11 sstrd ( ( 𝑊 ∈ LMod ∧ 𝑈𝐿𝐺𝑈 ) → 𝐺 ⊆ ( Base ‘ 𝑊 ) )
13 9 4 2 lspcl ( ( 𝑊 ∈ LMod ∧ 𝐺 ⊆ ( Base ‘ 𝑊 ) ) → ( 𝑀𝐺 ) ∈ 𝐿 )
14 7 12 13 syl2anc ( ( 𝑊 ∈ LMod ∧ 𝑈𝐿𝐺𝑈 ) → ( 𝑀𝐺 ) ∈ 𝐿 )
15 4 2 lspssp ( ( 𝑊 ∈ LMod ∧ 𝑈𝐿𝐺𝑈 ) → ( 𝑀𝐺 ) ⊆ 𝑈 )
16 eqid ( LSubSp ‘ 𝑋 ) = ( LSubSp ‘ 𝑋 )
17 1 4 16 lsslss ( ( 𝑊 ∈ LMod ∧ 𝑈𝐿 ) → ( ( 𝑀𝐺 ) ∈ ( LSubSp ‘ 𝑋 ) ↔ ( ( 𝑀𝐺 ) ∈ 𝐿 ∧ ( 𝑀𝐺 ) ⊆ 𝑈 ) ) )
18 17 3adant3 ( ( 𝑊 ∈ LMod ∧ 𝑈𝐿𝐺𝑈 ) → ( ( 𝑀𝐺 ) ∈ ( LSubSp ‘ 𝑋 ) ↔ ( ( 𝑀𝐺 ) ∈ 𝐿 ∧ ( 𝑀𝐺 ) ⊆ 𝑈 ) ) )
19 14 15 18 mpbir2and ( ( 𝑊 ∈ LMod ∧ 𝑈𝐿𝐺𝑈 ) → ( 𝑀𝐺 ) ∈ ( LSubSp ‘ 𝑋 ) )
20 9 2 lspssid ( ( 𝑊 ∈ LMod ∧ 𝐺 ⊆ ( Base ‘ 𝑊 ) ) → 𝐺 ⊆ ( 𝑀𝐺 ) )
21 7 12 20 syl2anc ( ( 𝑊 ∈ LMod ∧ 𝑈𝐿𝐺𝑈 ) → 𝐺 ⊆ ( 𝑀𝐺 ) )
22 16 3 lspssp ( ( 𝑋 ∈ LMod ∧ ( 𝑀𝐺 ) ∈ ( LSubSp ‘ 𝑋 ) ∧ 𝐺 ⊆ ( 𝑀𝐺 ) ) → ( 𝑁𝐺 ) ⊆ ( 𝑀𝐺 ) )
23 6 19 21 22 syl3anc ( ( 𝑊 ∈ LMod ∧ 𝑈𝐿𝐺𝑈 ) → ( 𝑁𝐺 ) ⊆ ( 𝑀𝐺 ) )
24 1 9 ressbas2 ( 𝑈 ⊆ ( Base ‘ 𝑊 ) → 𝑈 = ( Base ‘ 𝑋 ) )
25 11 24 syl ( ( 𝑊 ∈ LMod ∧ 𝑈𝐿𝐺𝑈 ) → 𝑈 = ( Base ‘ 𝑋 ) )
26 8 25 sseqtrd ( ( 𝑊 ∈ LMod ∧ 𝑈𝐿𝐺𝑈 ) → 𝐺 ⊆ ( Base ‘ 𝑋 ) )
27 eqid ( Base ‘ 𝑋 ) = ( Base ‘ 𝑋 )
28 27 16 3 lspcl ( ( 𝑋 ∈ LMod ∧ 𝐺 ⊆ ( Base ‘ 𝑋 ) ) → ( 𝑁𝐺 ) ∈ ( LSubSp ‘ 𝑋 ) )
29 6 26 28 syl2anc ( ( 𝑊 ∈ LMod ∧ 𝑈𝐿𝐺𝑈 ) → ( 𝑁𝐺 ) ∈ ( LSubSp ‘ 𝑋 ) )
30 1 4 16 lsslss ( ( 𝑊 ∈ LMod ∧ 𝑈𝐿 ) → ( ( 𝑁𝐺 ) ∈ ( LSubSp ‘ 𝑋 ) ↔ ( ( 𝑁𝐺 ) ∈ 𝐿 ∧ ( 𝑁𝐺 ) ⊆ 𝑈 ) ) )
31 30 3adant3 ( ( 𝑊 ∈ LMod ∧ 𝑈𝐿𝐺𝑈 ) → ( ( 𝑁𝐺 ) ∈ ( LSubSp ‘ 𝑋 ) ↔ ( ( 𝑁𝐺 ) ∈ 𝐿 ∧ ( 𝑁𝐺 ) ⊆ 𝑈 ) ) )
32 29 31 mpbid ( ( 𝑊 ∈ LMod ∧ 𝑈𝐿𝐺𝑈 ) → ( ( 𝑁𝐺 ) ∈ 𝐿 ∧ ( 𝑁𝐺 ) ⊆ 𝑈 ) )
33 32 simpld ( ( 𝑊 ∈ LMod ∧ 𝑈𝐿𝐺𝑈 ) → ( 𝑁𝐺 ) ∈ 𝐿 )
34 27 3 lspssid ( ( 𝑋 ∈ LMod ∧ 𝐺 ⊆ ( Base ‘ 𝑋 ) ) → 𝐺 ⊆ ( 𝑁𝐺 ) )
35 6 26 34 syl2anc ( ( 𝑊 ∈ LMod ∧ 𝑈𝐿𝐺𝑈 ) → 𝐺 ⊆ ( 𝑁𝐺 ) )
36 4 2 lspssp ( ( 𝑊 ∈ LMod ∧ ( 𝑁𝐺 ) ∈ 𝐿𝐺 ⊆ ( 𝑁𝐺 ) ) → ( 𝑀𝐺 ) ⊆ ( 𝑁𝐺 ) )
37 7 33 35 36 syl3anc ( ( 𝑊 ∈ LMod ∧ 𝑈𝐿𝐺𝑈 ) → ( 𝑀𝐺 ) ⊆ ( 𝑁𝐺 ) )
38 23 37 eqssd ( ( 𝑊 ∈ LMod ∧ 𝑈𝐿𝐺𝑈 ) → ( 𝑁𝐺 ) = ( 𝑀𝐺 ) )