shscli

Description: Closure of subspace sum. (Contributed by NM, 15-Oct-1999) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	shscl.1	$⊢ A \in S_{ℋ}$
	shscl.2	$⊢ B \in S_{ℋ}$
Assertion	shscli	$⊢ A +_{ℋ} B \in S_{ℋ}$

Proof

Step	Hyp	Ref	Expression
1		shscl.1	$⊢ A \in S_{ℋ}$
2		shscl.2	$⊢ B \in S_{ℋ}$
3		shsss	$⊢ (A \in S_{ℋ} \land B \in S_{ℋ}) \to A +_{ℋ} B \subseteq ℋ$
4	1 2 3	mp2an	$⊢ A +_{ℋ} B \subseteq ℋ$
5		sh0	$⊢ A \in S_{ℋ} \to 0_{ℎ} \in A$
6	1 5	ax-mp	$⊢ 0_{ℎ} \in A$
7		sh0	$⊢ B \in S_{ℋ} \to 0_{ℎ} \in B$
8	2 7	ax-mp	$⊢ 0_{ℎ} \in B$
9		ax-hv0cl	$⊢ 0_{ℎ} \in ℋ$
10	9	hvaddlidi	$⊢ 0_{ℎ} +_{ℎ} 0_{ℎ} = 0_{ℎ}$
11	10	eqcomi	$⊢ 0_{ℎ} = 0_{ℎ} +_{ℎ} 0_{ℎ}$
12		rspceov	$⊢ (0_{ℎ} \in A \land 0_{ℎ} \in B \land 0_{ℎ} = 0_{ℎ} +_{ℎ} 0_{ℎ}) \to \exists x \in A \exists y \in B 0_{ℎ} = x +_{ℎ} y$
13	6 8 11 12	mp3an	$⊢ \exists x \in A \exists y \in B 0_{ℎ} = x +_{ℎ} y$
14	1 2	shseli	$⊢ 0_{ℎ} \in (A +_{ℋ} B) \leftrightarrow \exists x \in A \exists y \in B 0_{ℎ} = x +_{ℎ} y$
15	13 14	mpbir	$⊢ 0_{ℎ} \in (A +_{ℋ} B)$
16	4 15	pm3.2i	$⊢ (A +_{ℋ} B \subseteq ℋ \land 0_{ℎ} \in (A +_{ℋ} B))$
17	1 2	shseli	$⊢ x \in (A +_{ℋ} B) \leftrightarrow \exists z \in A \exists w \in B x = z +_{ℎ} w$
18	1 2	shseli	$⊢ y \in (A +_{ℋ} B) \leftrightarrow \exists v \in A \exists u \in B y = v +_{ℎ} u$
19		shaddcl	$⊢ (A \in S_{ℋ} \land z \in A \land v \in A) \to z +_{ℎ} v \in A$
20	1 19	mp3an1	$⊢ (z \in A \land v \in A) \to z +_{ℎ} v \in A$
21	20	ad2ant2r	$⊢ ((z \in A \land w \in B) \land (v \in A \land u \in B)) \to z +_{ℎ} v \in A$
22	21	ad2ant2r	$⊢ (((z \in A \land w \in B) \land x = z +_{ℎ} w) \land ((v \in A \land u \in B) \land y = v +_{ℎ} u)) \to z +_{ℎ} v \in A$
23		shaddcl	$⊢ (B \in S_{ℋ} \land w \in B \land u \in B) \to w +_{ℎ} u \in B$
24	2 23	mp3an1	$⊢ (w \in B \land u \in B) \to w +_{ℎ} u \in B$
25	24	ad2ant2l	$⊢ ((z \in A \land w \in B) \land (v \in A \land u \in B)) \to w +_{ℎ} u \in B$
26	25	ad2ant2r	$⊢ (((z \in A \land w \in B) \land x = z +_{ℎ} w) \land ((v \in A \land u \in B) \land y = v +_{ℎ} u)) \to w +_{ℎ} u \in B$
27		oveq12	$⊢ (x = z +_{ℎ} w \land y = v +_{ℎ} u) \to x +_{ℎ} y = (z +_{ℎ} w) +_{ℎ} (v +_{ℎ} u)$
28	27	ad2ant2l	$⊢ (((z \in A \land w \in B) \land x = z +_{ℎ} w) \land ((v \in A \land u \in B) \land y = v +_{ℎ} u)) \to x +_{ℎ} y = (z +_{ℎ} w) +_{ℎ} (v +_{ℎ} u)$
29	1	sheli	$⊢ z \in A \to z \in ℋ$
30	1	sheli	$⊢ v \in A \to v \in ℋ$
31	29 30	anim12i	$⊢ (z \in A \land v \in A) \to (z \in ℋ \land v \in ℋ)$
32	2	sheli	$⊢ w \in B \to w \in ℋ$
33	2	sheli	$⊢ u \in B \to u \in ℋ$
34	32 33	anim12i	$⊢ (w \in B \land u \in B) \to (w \in ℋ \land u \in ℋ)$
35		hvadd4	$⊢ ((z \in ℋ \land v \in ℋ) \land (w \in ℋ \land u \in ℋ)) \to (z +_{ℎ} v) +_{ℎ} (w +_{ℎ} u) = (z +_{ℎ} w) +_{ℎ} (v +_{ℎ} u)$
36	31 34 35	syl2an	$⊢ ((z \in A \land v \in A) \land (w \in B \land u \in B)) \to (z +_{ℎ} v) +_{ℎ} (w +_{ℎ} u) = (z +_{ℎ} w) +_{ℎ} (v +_{ℎ} u)$
37	36	an4s	$⊢ ((z \in A \land w \in B) \land (v \in A \land u \in B)) \to (z +_{ℎ} v) +_{ℎ} (w +_{ℎ} u) = (z +_{ℎ} w) +_{ℎ} (v +_{ℎ} u)$
38	37	ad2ant2r	$⊢ (((z \in A \land w \in B) \land x = z +_{ℎ} w) \land ((v \in A \land u \in B) \land y = v +_{ℎ} u)) \to (z +_{ℎ} v) +_{ℎ} (w +_{ℎ} u) = (z +_{ℎ} w) +_{ℎ} (v +_{ℎ} u)$
39	28 38	eqtr4d	$⊢ (((z \in A \land w \in B) \land x = z +_{ℎ} w) \land ((v \in A \land u \in B) \land y = v +_{ℎ} u)) \to x +_{ℎ} y = (z +_{ℎ} v) +_{ℎ} (w +_{ℎ} u)$
40		rspceov	$⊢ (z +_{ℎ} v \in A \land w +_{ℎ} u \in B \land x +_{ℎ} y = (z +_{ℎ} v) +_{ℎ} (w +_{ℎ} u)) \to \exists f \in A \exists g \in B x +_{ℎ} y = f +_{ℎ} g$
41	22 26 39 40	syl3anc	$⊢ (((z \in A \land w \in B) \land x = z +_{ℎ} w) \land ((v \in A \land u \in B) \land y = v +_{ℎ} u)) \to \exists f \in A \exists g \in B x +_{ℎ} y = f +_{ℎ} g$
42	41	ancoms	$⊢ (((v \in A \land u \in B) \land y = v +_{ℎ} u) \land ((z \in A \land w \in B) \land x = z +_{ℎ} w)) \to \exists f \in A \exists g \in B x +_{ℎ} y = f +_{ℎ} g$
43	42	exp43	$⊢ (v \in A \land u \in B) \to (y = v +_{ℎ} u \to ((z \in A \land w \in B) \to (x = z +_{ℎ} w \to \exists f \in A \exists g \in B x +_{ℎ} y = f +_{ℎ} g)))$
44	43	rexlimivv	$⊢ \exists v \in A \exists u \in B y = v +_{ℎ} u \to ((z \in A \land w \in B) \to (x = z +_{ℎ} w \to \exists f \in A \exists g \in B x +_{ℎ} y = f +_{ℎ} g))$
45	44	com3l	$⊢ (z \in A \land w \in B) \to (x = z +_{ℎ} w \to (\exists v \in A \exists u \in B y = v +_{ℎ} u \to \exists f \in A \exists g \in B x +_{ℎ} y = f +_{ℎ} g))$
46	45	rexlimivv	$⊢ \exists z \in A \exists w \in B x = z +_{ℎ} w \to (\exists v \in A \exists u \in B y = v +_{ℎ} u \to \exists f \in A \exists g \in B x +_{ℎ} y = f +_{ℎ} g)$
47	46	imp	$⊢ (\exists z \in A \exists w \in B x = z +_{ℎ} w \land \exists v \in A \exists u \in B y = v +_{ℎ} u) \to \exists f \in A \exists g \in B x +_{ℎ} y = f +_{ℎ} g$
48	17 18 47	syl2anb	$⊢ (x \in (A +_{ℋ} B) \land y \in (A +_{ℋ} B)) \to \exists f \in A \exists g \in B x +_{ℎ} y = f +_{ℎ} g$
49	1 2	shseli	$⊢ x +_{ℎ} y \in (A +_{ℋ} B) \leftrightarrow \exists f \in A \exists g \in B x +_{ℎ} y = f +_{ℎ} g$
50	48 49	sylibr	$⊢ (x \in (A +_{ℋ} B) \land y \in (A +_{ℋ} B)) \to x +_{ℎ} y \in (A +_{ℋ} B)$
51	50	rgen2	$⊢ \forall x \in (A +_{ℋ} B) \forall y \in (A +_{ℋ} B) x +_{ℎ} y \in (A +_{ℋ} B)$
52		shmulcl	$⊢ (A \in S_{ℋ} \land x \in ℂ \land v \in A) \to x \cdot_{ℎ} v \in A$
53	1 52	mp3an1	$⊢ (x \in ℂ \land v \in A) \to x \cdot_{ℎ} v \in A$
54	53	adantrr	$⊢ (x \in ℂ \land (v \in A \land (u \in B \land y = v +_{ℎ} u))) \to x \cdot_{ℎ} v \in A$
55		shmulcl	$⊢ (B \in S_{ℋ} \land x \in ℂ \land u \in B) \to x \cdot_{ℎ} u \in B$
56	2 55	mp3an1	$⊢ (x \in ℂ \land u \in B) \to x \cdot_{ℎ} u \in B$
57	56	adantrr	$⊢ (x \in ℂ \land (u \in B \land y = v +_{ℎ} u)) \to x \cdot_{ℎ} u \in B$
58	57	adantrl	$⊢ (x \in ℂ \land (v \in A \land (u \in B \land y = v +_{ℎ} u))) \to x \cdot_{ℎ} u \in B$
59		oveq2	$⊢ y = v +_{ℎ} u \to x \cdot_{ℎ} y = x \cdot_{ℎ} (v +_{ℎ} u)$
60	59	adantl	$⊢ (u \in B \land y = v +_{ℎ} u) \to x \cdot_{ℎ} y = x \cdot_{ℎ} (v +_{ℎ} u)$
61	60	ad2antll	$⊢ (x \in ℂ \land (v \in A \land (u \in B \land y = v +_{ℎ} u))) \to x \cdot_{ℎ} y = x \cdot_{ℎ} (v +_{ℎ} u)$
62		id	$⊢ x \in ℂ \to x \in ℂ$
63		ax-hvdistr1	$⊢ (x \in ℂ \land v \in ℋ \land u \in ℋ) \to x \cdot_{ℎ} (v +_{ℎ} u) = (x \cdot_{ℎ} v) +_{ℎ} (x \cdot_{ℎ} u)$
64	62 30 33 63	syl3an	$⊢ (x \in ℂ \land v \in A \land u \in B) \to x \cdot_{ℎ} (v +_{ℎ} u) = (x \cdot_{ℎ} v) +_{ℎ} (x \cdot_{ℎ} u)$
65	64	3expb	$⊢ (x \in ℂ \land (v \in A \land u \in B)) \to x \cdot_{ℎ} (v +_{ℎ} u) = (x \cdot_{ℎ} v) +_{ℎ} (x \cdot_{ℎ} u)$
66	65	adantrrr	$⊢ (x \in ℂ \land (v \in A \land (u \in B \land y = v +_{ℎ} u))) \to x \cdot_{ℎ} (v +_{ℎ} u) = (x \cdot_{ℎ} v) +_{ℎ} (x \cdot_{ℎ} u)$
67	61 66	eqtrd	$⊢ (x \in ℂ \land (v \in A \land (u \in B \land y = v +_{ℎ} u))) \to x \cdot_{ℎ} y = (x \cdot_{ℎ} v) +_{ℎ} (x \cdot_{ℎ} u)$
68		rspceov	$⊢ (x \cdot_{ℎ} v \in A \land x \cdot_{ℎ} u \in B \land x \cdot_{ℎ} y = (x \cdot_{ℎ} v) +_{ℎ} (x \cdot_{ℎ} u)) \to \exists f \in A \exists g \in B x \cdot_{ℎ} y = f +_{ℎ} g$
69	54 58 67 68	syl3anc	$⊢ (x \in ℂ \land (v \in A \land (u \in B \land y = v +_{ℎ} u))) \to \exists f \in A \exists g \in B x \cdot_{ℎ} y = f +_{ℎ} g$
70	69	ancoms	$⊢ ((v \in A \land (u \in B \land y = v +_{ℎ} u)) \land x \in ℂ) \to \exists f \in A \exists g \in B x \cdot_{ℎ} y = f +_{ℎ} g$
71	70	exp42	$⊢ v \in A \to (u \in B \to (y = v +_{ℎ} u \to (x \in ℂ \to \exists f \in A \exists g \in B x \cdot_{ℎ} y = f +_{ℎ} g)))$
72	71	imp	$⊢ (v \in A \land u \in B) \to (y = v +_{ℎ} u \to (x \in ℂ \to \exists f \in A \exists g \in B x \cdot_{ℎ} y = f +_{ℎ} g))$
73	72	rexlimivv	$⊢ \exists v \in A \exists u \in B y = v +_{ℎ} u \to (x \in ℂ \to \exists f \in A \exists g \in B x \cdot_{ℎ} y = f +_{ℎ} g)$
74	73	impcom	$⊢ (x \in ℂ \land \exists v \in A \exists u \in B y = v +_{ℎ} u) \to \exists f \in A \exists g \in B x \cdot_{ℎ} y = f +_{ℎ} g$
75	18 74	sylan2b	$⊢ (x \in ℂ \land y \in (A +_{ℋ} B)) \to \exists f \in A \exists g \in B x \cdot_{ℎ} y = f +_{ℎ} g$
76	1 2	shseli	$⊢ x \cdot_{ℎ} y \in (A +_{ℋ} B) \leftrightarrow \exists f \in A \exists g \in B x \cdot_{ℎ} y = f +_{ℎ} g$
77	75 76	sylibr	$⊢ (x \in ℂ \land y \in (A +_{ℋ} B)) \to x \cdot_{ℎ} y \in (A +_{ℋ} B)$
78	77	rgen2	$⊢ \forall x \in ℂ \forall y \in (A +_{ℋ} B) x \cdot_{ℎ} y \in (A +_{ℋ} B)$
79	51 78	pm3.2i	$⊢ (\forall x \in (A +_{ℋ} B) \forall y \in (A +_{ℋ} B) x +_{ℎ} y \in (A +_{ℋ} B) \land \forall x \in ℂ \forall y \in (A +_{ℋ} B) x \cdot_{ℎ} y \in (A +_{ℋ} B))$
80		issh2	$⊢ A +_{ℋ} B \in S_{ℋ} \leftrightarrow ((A +_{ℋ} B \subseteq ℋ \land 0_{ℎ} \in (A +_{ℋ} B)) \land (\forall x \in (A +_{ℋ} B) \forall y \in (A +_{ℋ} B) x +_{ℎ} y \in (A +_{ℋ} B) \land \forall x \in ℂ \forall y \in (A +_{ℋ} B) x \cdot_{ℎ} y \in (A +_{ℋ} B)))$
81	16 79 80	mpbir2an	$⊢ A +_{ℋ} B \in S_{ℋ}$

Metamath Proof Explorer

Theorem shscli

Proof