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	$⊢ 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 M (G) = N (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		simp1	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to W \in LMod$
6	1 4	lsslmod	$⊢ (W \in LMod \land U \in L) \to X \in LMod$
7	6	3adant3	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to X \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	1 9	ressbas2	$⊢ U \subseteq {Base}_{W} \to U = {Base}_{X}$
13	11 12	syl	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to U = {Base}_{X}$
14	8 13	sseqtrd	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to G \subseteq {Base}_{X}$
15		eqid	$⊢ {Base}_{X} = {Base}_{X}$
16		eqid	$⊢ LSubSp (X) = LSubSp (X)$
17	15 16 3	lspcl	$⊢ (X \in LMod \land G \subseteq {Base}_{X}) \to N (G) \in LSubSp (X)$
18	7 14 17	syl2anc	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to N (G) \in LSubSp (X)$
19	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))$
20	19	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))$
21	18 20	mpbid	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to (N (G) \in L \land N (G) \subseteq U)$
22	21	simpld	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to N (G) \in L$
23	15 3	lspssid	$⊢ (X \in LMod \land G \subseteq {Base}_{X}) \to G \subseteq N (G)$
24	7 14 23	syl2anc	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to G \subseteq N (G)$
25	4 2	lspssp	$⊢ (W \in LMod \land N (G) \in L \land G \subseteq N (G)) \to M (G) \subseteq N (G)$
26	5 22 24 25	syl3anc	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to M (G) \subseteq N (G)$
27	8 11	sstrd	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to G \subseteq {Base}_{W}$
28	9 4 2	lspcl	$⊢ (W \in LMod \land G \subseteq {Base}_{W}) \to M (G) \in L$
29	5 27 28	syl2anc	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to M (G) \in L$
30	4 2	lspssp	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to M (G) \subseteq U$
31	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))$
32	31	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))$
33	29 30 32	mpbir2and	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to M (G) \in LSubSp (X)$
34	9 2	lspssid	$⊢ (W \in LMod \land G \subseteq {Base}_{W}) \to G \subseteq M (G)$
35	5 27 34	syl2anc	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to G \subseteq M (G)$
36	16 3	lspssp	$⊢ (X \in LMod \land M (G) \in LSubSp (X) \land G \subseteq M (G)) \to N (G) \subseteq M (G)$
37	7 33 35 36	syl3anc	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to N (G) \subseteq M (G)$
38	26 37	eqssd	$⊢ (W \in LMod \land U \in L \land G \subseteq U) \to M (G) = N (G)$

Metamath Proof Explorer

Theorem lsslsp

Proof