lspun

Description: The span of union is the span of the union of spans. (Contributed by NM, 22-Feb-2014) (Revised by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypotheses	lspss.v	$⊢ V = {Base}_{W}$
	lspss.n	$⊢ N = LSpan (W)$
Assertion	lspun	$⊢ (W \in LMod \land T \subseteq V \land U \subseteq V) \to N (T \cup U) = N (N (T) \cup N (U))$

Proof

Step	Hyp	Ref	Expression
1		lspss.v	$⊢ V = {Base}_{W}$
2		lspss.n	$⊢ N = LSpan (W)$
3		simp1	$⊢ (W \in LMod \land T \subseteq V \land U \subseteq V) \to W \in LMod$
4		simp2	$⊢ (W \in LMod \land T \subseteq V \land U \subseteq V) \to T \subseteq V$
5		simp3	$⊢ (W \in LMod \land T \subseteq V \land U \subseteq V) \to U \subseteq V$
6	4 5	unssd	$⊢ (W \in LMod \land T \subseteq V \land U \subseteq V) \to T \cup U \subseteq V$
7		ssun1	$⊢ T \subseteq T \cup U$
8	7	a1i	$⊢ (W \in LMod \land T \subseteq V \land U \subseteq V) \to T \subseteq T \cup U$
9	1 2	lspss	$⊢ (W \in LMod \land T \cup U \subseteq V \land T \subseteq T \cup U) \to N (T) \subseteq N (T \cup U)$
10	3 6 8 9	syl3anc	$⊢ (W \in LMod \land T \subseteq V \land U \subseteq V) \to N (T) \subseteq N (T \cup U)$
11		ssun2	$⊢ U \subseteq T \cup U$
12	11	a1i	$⊢ (W \in LMod \land T \subseteq V \land U \subseteq V) \to U \subseteq T \cup U$
13	1 2	lspss	$⊢ (W \in LMod \land T \cup U \subseteq V \land U \subseteq T \cup U) \to N (U) \subseteq N (T \cup U)$
14	3 6 12 13	syl3anc	$⊢ (W \in LMod \land T \subseteq V \land U \subseteq V) \to N (U) \subseteq N (T \cup U)$
15	10 14	unssd	$⊢ (W \in LMod \land T \subseteq V \land U \subseteq V) \to N (T) \cup N (U) \subseteq N (T \cup U)$
16	1 2	lspssv	$⊢ (W \in LMod \land T \cup U \subseteq V) \to N (T \cup U) \subseteq V$
17	3 6 16	syl2anc	$⊢ (W \in LMod \land T \subseteq V \land U \subseteq V) \to N (T \cup U) \subseteq V$
18	15 17	sstrd	$⊢ (W \in LMod \land T \subseteq V \land U \subseteq V) \to N (T) \cup N (U) \subseteq V$
19	1 2	lspssid	$⊢ (W \in LMod \land T \subseteq V) \to T \subseteq N (T)$
20	3 4 19	syl2anc	$⊢ (W \in LMod \land T \subseteq V \land U \subseteq V) \to T \subseteq N (T)$
21	1 2	lspssid	$⊢ (W \in LMod \land U \subseteq V) \to U \subseteq N (U)$
22		unss12	$⊢ (T \subseteq N (T) \land U \subseteq N (U)) \to T \cup U \subseteq N (T) \cup N (U)$
23	20 21 22	3imp3i2an	$⊢ (W \in LMod \land T \subseteq V \land U \subseteq V) \to T \cup U \subseteq N (T) \cup N (U)$
24	1 2	lspss	$⊢ (W \in LMod \land N (T) \cup N (U) \subseteq V \land T \cup U \subseteq N (T) \cup N (U)) \to N (T \cup U) \subseteq N (N (T) \cup N (U))$
25	3 18 23 24	syl3anc	$⊢ (W \in LMod \land T \subseteq V \land U \subseteq V) \to N (T \cup U) \subseteq N (N (T) \cup N (U))$
26	1 2	lspss	$⊢ (W \in LMod \land N (T \cup U) \subseteq V \land N (T) \cup N (U) \subseteq N (T \cup U)) \to N (N (T) \cup N (U)) \subseteq N (N (T \cup U))$
27	3 17 15 26	syl3anc	$⊢ (W \in LMod \land T \subseteq V \land U \subseteq V) \to N (N (T) \cup N (U)) \subseteq N (N (T \cup U))$
28	1 2	lspidm	$⊢ (W \in LMod \land T \cup U \subseteq V) \to N (N (T \cup U)) = N (T \cup U)$
29	3 6 28	syl2anc	$⊢ (W \in LMod \land T \subseteq V \land U \subseteq V) \to N (N (T \cup U)) = N (T \cup U)$
30	27 29	sseqtrd	$⊢ (W \in LMod \land T \subseteq V \land U \subseteq V) \to N (N (T) \cup N (U)) \subseteq N (T \cup U)$
31	25 30	eqssd	$⊢ (W \in LMod \land T \subseteq V \land U \subseteq V) \to N (T \cup U) = N (N (T) \cup N (U))$

Metamath Proof Explorer

Theorem lspun

Proof