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 ⊢ 𝑋 = ( 𝑊 ↾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 simp1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ∧ 𝐺 ⊆ 𝑈 ) → 𝑊 ∈ LMod )
6 1 4 lsslmod ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ) → 𝑋 ∈ LMod )
7 6 3adant3 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ∧ 𝐺 ⊆ 𝑈 ) → 𝑋 ∈ LMod )
8 simp3 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ∧ 𝐺 ⊆ 𝑈 ) → 𝐺 ⊆ 𝑈 )
9 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
10 9 4 lssss ⊢ ( 𝑈 ∈ 𝐿 → 𝑈 ⊆ ( Base ‘ 𝑊 ) )
11 10 3ad2ant2 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ∧ 𝐺 ⊆ 𝑈 ) → 𝑈 ⊆ ( Base ‘ 𝑊 ) )
12 1 9 ressbas2 ⊢ ( 𝑈 ⊆ ( Base ‘ 𝑊 ) → 𝑈 = ( Base ‘ 𝑋 ) )
13 11 12 syl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ∧ 𝐺 ⊆ 𝑈 ) → 𝑈 = ( Base ‘ 𝑋 ) )
14 8 13 sseqtrd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ∧ 𝐺 ⊆ 𝑈 ) → 𝐺 ⊆ ( Base ‘ 𝑋 ) )
15 eqid ⊢ ( Base ‘ 𝑋 ) = ( Base ‘ 𝑋 )
16 eqid ⊢ ( LSubSp ‘ 𝑋 ) = ( LSubSp ‘ 𝑋 )
17 15 16 3 lspcl ⊢ ( ( 𝑋 ∈ LMod ∧ 𝐺 ⊆ ( Base ‘ 𝑋 ) ) → ( 𝑁 ‘ 𝐺 ) ∈ ( LSubSp ‘ 𝑋 ) )
18 7 14 17 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ∧ 𝐺 ⊆ 𝑈 ) → ( 𝑁 ‘ 𝐺 ) ∈ ( LSubSp ‘ 𝑋 ) )
19 1 4 16 lsslss ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ) → ( ( 𝑁 ‘ 𝐺 ) ∈ ( LSubSp ‘ 𝑋 ) ↔ ( ( 𝑁 ‘ 𝐺 ) ∈ 𝐿 ∧ ( 𝑁 ‘ 𝐺 ) ⊆ 𝑈 ) ) )
20 19 3adant3 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ∧ 𝐺 ⊆ 𝑈 ) → ( ( 𝑁 ‘ 𝐺 ) ∈ ( LSubSp ‘ 𝑋 ) ↔ ( ( 𝑁 ‘ 𝐺 ) ∈ 𝐿 ∧ ( 𝑁 ‘ 𝐺 ) ⊆ 𝑈 ) ) )
21 18 20 mpbid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ∧ 𝐺 ⊆ 𝑈 ) → ( ( 𝑁 ‘ 𝐺 ) ∈ 𝐿 ∧ ( 𝑁 ‘ 𝐺 ) ⊆ 𝑈 ) )
22 21 simpld ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ∧ 𝐺 ⊆ 𝑈 ) → ( 𝑁 ‘ 𝐺 ) ∈ 𝐿 )
23 15 3 lspssid ⊢ ( ( 𝑋 ∈ LMod ∧ 𝐺 ⊆ ( Base ‘ 𝑋 ) ) → 𝐺 ⊆ ( 𝑁 ‘ 𝐺 ) )
24 7 14 23 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ∧ 𝐺 ⊆ 𝑈 ) → 𝐺 ⊆ ( 𝑁 ‘ 𝐺 ) )
25 4 2 lspssp ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ 𝐺 ) ∈ 𝐿 ∧ 𝐺 ⊆ ( 𝑁 ‘ 𝐺 ) ) → ( 𝑀 ‘ 𝐺 ) ⊆ ( 𝑁 ‘ 𝐺 ) )
26 5 22 24 25 syl3anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ∧ 𝐺 ⊆ 𝑈 ) → ( 𝑀 ‘ 𝐺 ) ⊆ ( 𝑁 ‘ 𝐺 ) )
27 8 11 sstrd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ∧ 𝐺 ⊆ 𝑈 ) → 𝐺 ⊆ ( Base ‘ 𝑊 ) )
28 9 4 2 lspcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ⊆ ( Base ‘ 𝑊 ) ) → ( 𝑀 ‘ 𝐺 ) ∈ 𝐿 )
29 5 27 28 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ∧ 𝐺 ⊆ 𝑈 ) → ( 𝑀 ‘ 𝐺 ) ∈ 𝐿 )
30 4 2 lspssp ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ∧ 𝐺 ⊆ 𝑈 ) → ( 𝑀 ‘ 𝐺 ) ⊆ 𝑈 )
31 1 4 16 lsslss ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ) → ( ( 𝑀 ‘ 𝐺 ) ∈ ( LSubSp ‘ 𝑋 ) ↔ ( ( 𝑀 ‘ 𝐺 ) ∈ 𝐿 ∧ ( 𝑀 ‘ 𝐺 ) ⊆ 𝑈 ) ) )
32 31 3adant3 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ∧ 𝐺 ⊆ 𝑈 ) → ( ( 𝑀 ‘ 𝐺 ) ∈ ( LSubSp ‘ 𝑋 ) ↔ ( ( 𝑀 ‘ 𝐺 ) ∈ 𝐿 ∧ ( 𝑀 ‘ 𝐺 ) ⊆ 𝑈 ) ) )
33 29 30 32 mpbir2and ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ∧ 𝐺 ⊆ 𝑈 ) → ( 𝑀 ‘ 𝐺 ) ∈ ( LSubSp ‘ 𝑋 ) )
34 9 2 lspssid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ⊆ ( Base ‘ 𝑊 ) ) → 𝐺 ⊆ ( 𝑀 ‘ 𝐺 ) )
35 5 27 34 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ∧ 𝐺 ⊆ 𝑈 ) → 𝐺 ⊆ ( 𝑀 ‘ 𝐺 ) )
36 16 3 lspssp ⊢ ( ( 𝑋 ∈ LMod ∧ ( 𝑀 ‘ 𝐺 ) ∈ ( LSubSp ‘ 𝑋 ) ∧ 𝐺 ⊆ ( 𝑀 ‘ 𝐺 ) ) → ( 𝑁 ‘ 𝐺 ) ⊆ ( 𝑀 ‘ 𝐺 ) )
37 7 33 35 36 syl3anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ∧ 𝐺 ⊆ 𝑈 ) → ( 𝑁 ‘ 𝐺 ) ⊆ ( 𝑀 ‘ 𝐺 ) )
38 26 37 eqssd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ∧ 𝐺 ⊆ 𝑈 ) → ( 𝑀 ‘ 𝐺 ) = ( 𝑁 ‘ 𝐺 ) )