# Metamath Proof Explorer

## Theorem 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 {\mathbf{S}}_{ℋ}$
shscl.2 ${⊢}{B}\in {\mathbf{S}}_{ℋ}$
Assertion shscli ${⊢}{A}{+}_{ℋ}{B}\in {\mathbf{S}}_{ℋ}$

### Proof

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