Theorem lsslspOLD

Description: Obsolete version of lsslsp as of 25-Apr-2025. 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. (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lsslsp.x	⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
	lsslsp.m	⊢ 𝑀 = ( LSpan ‘ 𝑊 )
	lsslsp.n	⊢ 𝑁 = ( LSpan ‘ 𝑋 )
	lsslsp.l	⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
Assertion	lsslspOLD	⊢ ( ( 𝑊 ∈ 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 ∧ 𝑈 ∈ 𝐿 ∧ 𝐺 ⊆ 𝑈 ) → ( 𝑀 ‘ 𝐺 ) = ( 𝑁 ‘ 𝐺 ) )