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 ↾_{𝑠} U$
	lsslsp.m	$⊢ M = LSpan (W)$
	lsslsp.n	$⊢ N = LSpan (X)$
	lsslsp.l	$⊢ L = LSubSp (W)$
Assertion	lsslsp	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to N (G) = M (G)$

Proof

Step	Hyp	Ref	Expression
1		lsslsp.x	$⊢ X = W ↾_{𝑠} U$
2		lsslsp.m	$⊢ M = LSpan (W)$
3		lsslsp.n	$⊢ N = LSpan (X)$
4		lsslsp.l	$⊢ L = LSubSp (W)$
5	1 4	lsslmod	$⊢ (W \in LMod \land U \in L) \to X \in LMod$
6	5	3adant3	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to X \in LMod$
7		simp1	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to W \in LMod$
8		simp3	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to G \subseteq U$
9		eqid	$⊢ {Base}_{W} = {Base}_{W}$
10	9 4	lssss	$⊢ U \in L \to U \subseteq {Base}_{W}$
11	10	3ad2ant2	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to U \subseteq {Base}_{W}$
12	8 11	sstrd	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to G \subseteq {Base}_{W}$
13	9 4 2	lspcl	$⊢ (W \in LMod \land G \subseteq {Base}_{W}) \to M (G) \in L$
14	7 12 13	syl2anc	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to M (G) \in L$
15	4 2	lspssp	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to M (G) \subseteq U$
16		eqid	$⊢ LSubSp (X) = LSubSp (X)$
17	1 4 16	lsslss	$⊢ (W \in LMod \land U \in L) \to (M (G) \in LSubSp (X) \leftrightarrow (M (G) \in L \land M (G) \subseteq U))$
18	17	3adant3	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to (M (G) \in LSubSp (X) \leftrightarrow (M (G) \in L \land M (G) \subseteq U))$
19	14 15 18	mpbir2and	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to M (G) \in LSubSp (X)$
20	9 2	lspssid	$⊢ (W \in LMod \land G \subseteq {Base}_{W}) \to G \subseteq M (G)$
21	7 12 20	syl2anc	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to G \subseteq M (G)$
22	16 3	lspssp	$⊢ (X \in LMod \land M (G) \in LSubSp (X) \land G \subseteq M (G)) \to N (G) \subseteq M (G)$
23	6 19 21 22	syl3anc	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to N (G) \subseteq M (G)$
24	1 9	ressbas2	$⊢ U \subseteq {Base}_{W} \to U = {Base}_{X}$
25	11 24	syl	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to U = {Base}_{X}$
26	8 25	sseqtrd	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to G \subseteq {Base}_{X}$
27		eqid	$⊢ {Base}_{X} = {Base}_{X}$
28	27 16 3	lspcl	$⊢ (X \in LMod \land G \subseteq {Base}_{X}) \to N (G) \in LSubSp (X)$
29	6 26 28	syl2anc	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to N (G) \in LSubSp (X)$
30	1 4 16	lsslss	$⊢ (W \in LMod \land U \in L) \to (N (G) \in LSubSp (X) \leftrightarrow (N (G) \in L \land N (G) \subseteq U))$
31	30	3adant3	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to (N (G) \in LSubSp (X) \leftrightarrow (N (G) \in L \land N (G) \subseteq U))$
32	29 31	mpbid	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to (N (G) \in L \land N (G) \subseteq U)$
33	32	simpld	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to N (G) \in L$
34	27 3	lspssid	$⊢ (X \in LMod \land G \subseteq {Base}_{X}) \to G \subseteq N (G)$
35	6 26 34	syl2anc	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to G \subseteq N (G)$
36	4 2	lspssp	$⊢ (W \in LMod \land N (G) \in L \land G \subseteq N (G)) \to M (G) \subseteq N (G)$
37	7 33 35 36	syl3anc	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to M (G) \subseteq N (G)$
38	23 37	eqssd	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to N (G) = M (G)$

Metamath Proof Explorer

Theorem lsslsp

Proof