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 ∧ 𝑈 ∈ 𝐿 ∧ 𝐺 ⊆ 𝑈 ) → ( 𝑁 ‘ 𝐺 ) = ( 𝑀 ‘ 𝐺 ) )