spanuni

Description: The span of a union is the subspace sum of spans. (Contributed by NM, 2-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	spanun.1	$⊢ A \subseteq ℋ$
	spanun.2	$⊢ B \subseteq ℋ$
Assertion	spanuni	$⊢ span (A \cup B) = span (A) +_{ℋ} span (B)$

Proof

Step	Hyp	Ref	Expression
1		spanun.1	$⊢ A \subseteq ℋ$
2		spanun.2	$⊢ B \subseteq ℋ$
3		spancl	$⊢ A \subseteq ℋ \to span (A) \in S_{ℋ}$
4	1 3	ax-mp	$⊢ span (A) \in S_{ℋ}$
5		spancl	$⊢ B \subseteq ℋ \to span (B) \in S_{ℋ}$
6	2 5	ax-mp	$⊢ span (B) \in S_{ℋ}$
7	4 6	shscli	$⊢ span (A) +_{ℋ} span (B) \in S_{ℋ}$
8	7	shssii	$⊢ span (A) +_{ℋ} span (B) \subseteq ℋ$
9		spanss2	$⊢ A \subseteq ℋ \to A \subseteq span (A)$
10	1 9	ax-mp	$⊢ A \subseteq span (A)$
11		spanss2	$⊢ B \subseteq ℋ \to B \subseteq span (B)$
12	2 11	ax-mp	$⊢ B \subseteq span (B)$
13		unss12	$⊢ (A \subseteq span (A) \land B \subseteq span (B)) \to A \cup B \subseteq span (A) \cup span (B)$
14	10 12 13	mp2an	$⊢ A \cup B \subseteq span (A) \cup span (B)$
15	4 6	shunssi	$⊢ span (A) \cup span (B) \subseteq span (A) +_{ℋ} span (B)$
16	14 15	sstri	$⊢ A \cup B \subseteq span (A) +_{ℋ} span (B)$
17		spanss	$⊢ (span (A) +_{ℋ} span (B) \subseteq ℋ \land A \cup B \subseteq span (A) +_{ℋ} span (B)) \to span (A \cup B) \subseteq span (span (A) +_{ℋ} span (B))$
18	8 16 17	mp2an	$⊢ span (A \cup B) \subseteq span (span (A) +_{ℋ} span (B))$
19		spanid	$⊢ span (A) +_{ℋ} span (B) \in S_{ℋ} \to span (span (A) +_{ℋ} span (B)) = span (A) +_{ℋ} span (B)$
20	7 19	ax-mp	$⊢ span (span (A) +_{ℋ} span (B)) = span (A) +_{ℋ} span (B)$
21	18 20	sseqtri	$⊢ span (A \cup B) \subseteq span (A) +_{ℋ} span (B)$
22	4 6	shseli	$⊢ x \in (span (A) +_{ℋ} span (B)) \leftrightarrow \exists z \in span (A) \exists w \in span (B) x = z +_{ℎ} w$
23		r2ex	$⊢ \exists z \in span (A) \exists w \in span (B) x = z +_{ℎ} w \leftrightarrow \exists z \exists w ((z \in span (A) \land w \in span (B)) \land x = z +_{ℎ} w)$
24	22 23	bitri	$⊢ x \in (span (A) +_{ℋ} span (B)) \leftrightarrow \exists z \exists w ((z \in span (A) \land w \in span (B)) \land x = z +_{ℎ} w)$
25		vex	$⊢ z \in V$
26	25	elspani	$⊢ A \subseteq ℋ \to (z \in span (A) \leftrightarrow \forall y \in S_{ℋ} (A \subseteq y \to z \in y))$
27	1 26	ax-mp	$⊢ z \in span (A) \leftrightarrow \forall y \in S_{ℋ} (A \subseteq y \to z \in y)$
28		vex	$⊢ w \in V$
29	28	elspani	$⊢ B \subseteq ℋ \to (w \in span (B) \leftrightarrow \forall y \in S_{ℋ} (B \subseteq y \to w \in y))$
30	2 29	ax-mp	$⊢ w \in span (B) \leftrightarrow \forall y \in S_{ℋ} (B \subseteq y \to w \in y)$
31	27 30	anbi12i	$⊢ (z \in span (A) \land w \in span (B)) \leftrightarrow (\forall y \in S_{ℋ} (A \subseteq y \to z \in y) \land \forall y \in S_{ℋ} (B \subseteq y \to w \in y))$
32		r19.26	$⊢ \forall y \in S_{ℋ} ((A \subseteq y \to z \in y) \land (B \subseteq y \to w \in y)) \leftrightarrow (\forall y \in S_{ℋ} (A \subseteq y \to z \in y) \land \forall y \in S_{ℋ} (B \subseteq y \to w \in y))$
33	31 32	bitr4i	$⊢ (z \in span (A) \land w \in span (B)) \leftrightarrow \forall y \in S_{ℋ} ((A \subseteq y \to z \in y) \land (B \subseteq y \to w \in y))$
34		r19.27v	$⊢ (\forall y \in S_{ℋ} ((A \subseteq y \to z \in y) \land (B \subseteq y \to w \in y)) \land x = z +_{ℎ} w) \to \forall y \in S_{ℋ} (((A \subseteq y \to z \in y) \land (B \subseteq y \to w \in y)) \land x = z +_{ℎ} w)$
35	33 34	sylanb	$⊢ ((z \in span (A) \land w \in span (B)) \land x = z +_{ℎ} w) \to \forall y \in S_{ℋ} (((A \subseteq y \to z \in y) \land (B \subseteq y \to w \in y)) \land x = z +_{ℎ} w)$
36		unss	$⊢ (A \subseteq y \land B \subseteq y) \leftrightarrow A \cup B \subseteq y$
37		anim12	$⊢ ((A \subseteq y \to z \in y) \land (B \subseteq y \to w \in y)) \to ((A \subseteq y \land B \subseteq y) \to (z \in y \land w \in y))$
38	36 37	biimtrrid	$⊢ ((A \subseteq y \to z \in y) \land (B \subseteq y \to w \in y)) \to (A \cup B \subseteq y \to (z \in y \land w \in y))$
39		shaddcl	$⊢ (y \in S_{ℋ} \land z \in y \land w \in y) \to z +_{ℎ} w \in y$
40	39	3expib	$⊢ y \in S_{ℋ} \to ((z \in y \land w \in y) \to z +_{ℎ} w \in y)$
41	38 40	sylan9r	$⊢ (y \in S_{ℋ} \land ((A \subseteq y \to z \in y) \land (B \subseteq y \to w \in y))) \to (A \cup B \subseteq y \to z +_{ℎ} w \in y)$
42		eleq1	$⊢ x = z +_{ℎ} w \to (x \in y \leftrightarrow z +_{ℎ} w \in y)$
43	42	biimprd	$⊢ x = z +_{ℎ} w \to (z +_{ℎ} w \in y \to x \in y)$
44	41 43	sylan9	$⊢ ((y \in S_{ℋ} \land ((A \subseteq y \to z \in y) \land (B \subseteq y \to w \in y))) \land x = z +_{ℎ} w) \to (A \cup B \subseteq y \to x \in y)$
45	44	expl	$⊢ y \in S_{ℋ} \to ((((A \subseteq y \to z \in y) \land (B \subseteq y \to w \in y)) \land x = z +_{ℎ} w) \to (A \cup B \subseteq y \to x \in y))$
46	45	ralimia	$⊢ \forall y \in S_{ℋ} (((A \subseteq y \to z \in y) \land (B \subseteq y \to w \in y)) \land x = z +_{ℎ} w) \to \forall y \in S_{ℋ} (A \cup B \subseteq y \to x \in y)$
47	1 2	unssi	$⊢ A \cup B \subseteq ℋ$
48		vex	$⊢ x \in V$
49	48	elspani	$⊢ A \cup B \subseteq ℋ \to (x \in span (A \cup B) \leftrightarrow \forall y \in S_{ℋ} (A \cup B \subseteq y \to x \in y))$
50	47 49	ax-mp	$⊢ x \in span (A \cup B) \leftrightarrow \forall y \in S_{ℋ} (A \cup B \subseteq y \to x \in y)$
51	46 50	sylibr	$⊢ \forall y \in S_{ℋ} (((A \subseteq y \to z \in y) \land (B \subseteq y \to w \in y)) \land x = z +_{ℎ} w) \to x \in span (A \cup B)$
52	35 51	syl	$⊢ ((z \in span (A) \land w \in span (B)) \land x = z +_{ℎ} w) \to x \in span (A \cup B)$
53	52	exlimivv	$⊢ \exists z \exists w ((z \in span (A) \land w \in span (B)) \land x = z +_{ℎ} w) \to x \in span (A \cup B)$
54	24 53	sylbi	$⊢ x \in (span (A) +_{ℋ} span (B)) \to x \in span (A \cup B)$
55	54	ssriv	$⊢ span (A) +_{ℋ} span (B) \subseteq span (A \cup B)$
56	21 55	eqssi	$⊢ span (A \cup B) = span (A) +_{ℋ} span (B)$

Metamath Proof Explorer

Theorem spanuni

Proof