Theorem shsval2i

Description: An alternate way to express subspace sum. (Contributed by NM, 25-Nov-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	shlesb1.1	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}$$
	shlesb1.2	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}$$
Assertion	shsval2i	$$⊢A{+}_{\mathscr{H}}B=\bigcap \left\{x\in {\mathbf{S}}_{\mathscr{H}}|A\cup B\subseteq x\right\}$$

Proof

Step	Hyp	Ref	Expression
1		shlesb1.1	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}$$
2		shlesb1.2	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}$$
3		ssun1	$$⊢A\subseteq A\cup B$$
4		ssintub	$$⊢A\cup B\subseteq \bigcap \left\{x\in {\mathbf{S}}_{\mathscr{H}}|A\cup B\subseteq x\right\}$$
5	3 4	sstri	$$⊢A\subseteq \bigcap \left\{x\in {\mathbf{S}}_{\mathscr{H}}|A\cup B\subseteq x\right\}$$
6		ssun2	$$⊢B\subseteq A\cup B$$
7	6 4	sstri	$$⊢B\subseteq \bigcap \left\{x\in {\mathbf{S}}_{\mathscr{H}}|A\cup B\subseteq x\right\}$$
8	5 7	pm3.2i	$$⊢\left(A\subseteq \bigcap \left\{x\in {\mathbf{S}}_{\mathscr{H}}|A\cup B\subseteq x\right\}\wedge B\subseteq \bigcap \left\{x\in {\mathbf{S}}_{\mathscr{H}}|A\cup B\subseteq x\right\}\right)$$
9		ssrab2	$$⊢\left\{x\in {\mathbf{S}}_{\mathscr{H}}|A\cup B\subseteq x\right\}\subseteq {\mathbf{S}}_{\mathscr{H}}$$
10	1 2	shscli	$$⊢A{+}_{\mathscr{H}}B\in {\mathbf{S}}_{\mathscr{H}}$$
11	1 2	shunssi	$$⊢A\cup B\subseteq A{+}_{\mathscr{H}}B$$
12		sseq2	$$⊢x=A{+}_{\mathscr{H}}B\to \left(A\cup B\subseteq x\leftrightarrow A\cup B\subseteq A{+}_{\mathscr{H}}B\right)$$
13	12	rspcev	$$⊢\left(A{+}_{\mathscr{H}}B\in {\mathbf{S}}_{\mathscr{H}}\wedge A\cup B\subseteq A{+}_{\mathscr{H}}B\right)\to \exists x\in {\mathbf{S}}_{\mathscr{H}}A\cup B\subseteq x$$
14	10 11 13	mp2an	$$⊢\exists x\in {\mathbf{S}}_{\mathscr{H}}A\cup B\subseteq x$$
15		rabn0	$$⊢\left\{x\in {\mathbf{S}}_{\mathscr{H}}|A\cup B\subseteq x\right\}\ne \varnothing \leftrightarrow \exists x\in {\mathbf{S}}_{\mathscr{H}}A\cup B\subseteq x$$
16	14 15	mpbir	$$⊢\left\{x\in {\mathbf{S}}_{\mathscr{H}}|A\cup B\subseteq x\right\}\ne \varnothing$$
17		shintcl	$$⊢\left(\left\{x\in {\mathbf{S}}_{\mathscr{H}}|A\cup B\subseteq x\right\}\subseteq {\mathbf{S}}_{\mathscr{H}}\wedge \left\{x\in {\mathbf{S}}_{\mathscr{H}}|A\cup B\subseteq x\right\}\ne \varnothing \right)\to \bigcap \left\{x\in {\mathbf{S}}_{\mathscr{H}}|A\cup B\subseteq x\right\}\in {\mathbf{S}}_{\mathscr{H}}$$
18	9 16 17	mp2an	$$⊢\bigcap \left\{x\in {\mathbf{S}}_{\mathscr{H}}|A\cup B\subseteq x\right\}\in {\mathbf{S}}_{\mathscr{H}}$$
19	1 2 18	shslubi	$$⊢\left(A\subseteq \bigcap \left\{x\in {\mathbf{S}}_{\mathscr{H}}|A\cup B\subseteq x\right\}\wedge B\subseteq \bigcap \left\{x\in {\mathbf{S}}_{\mathscr{H}}|A\cup B\subseteq x\right\}\right)\leftrightarrow A{+}_{\mathscr{H}}B\subseteq \bigcap \left\{x\in {\mathbf{S}}_{\mathscr{H}}|A\cup B\subseteq x\right\}$$
20	8 19	mpbi	$$⊢A{+}_{\mathscr{H}}B\subseteq \bigcap \left\{x\in {\mathbf{S}}_{\mathscr{H}}|A\cup B\subseteq x\right\}$$
21	12	elrab	$$⊢A{+}_{\mathscr{H}}B\in \left\{x\in {\mathbf{S}}_{\mathscr{H}}|A\cup B\subseteq x\right\}\leftrightarrow \left(A{+}_{\mathscr{H}}B\in {\mathbf{S}}_{\mathscr{H}}\wedge A\cup B\subseteq A{+}_{\mathscr{H}}B\right)$$
22	10 11 21	mpbir2an	$$⊢A{+}_{\mathscr{H}}B\in \left\{x\in {\mathbf{S}}_{\mathscr{H}}|A\cup B\subseteq x\right\}$$
23		intss1	$$⊢A{+}_{\mathscr{H}}B\in \left\{x\in {\mathbf{S}}_{\mathscr{H}}|A\cup B\subseteq x\right\}\to \bigcap \left\{x\in {\mathbf{S}}_{\mathscr{H}}|A\cup B\subseteq x\right\}\subseteq A{+}_{\mathscr{H}}B$$
24	22 23	ax-mp	$$⊢\bigcap \left\{x\in {\mathbf{S}}_{\mathscr{H}}|A\cup B\subseteq x\right\}\subseteq A{+}_{\mathscr{H}}B$$
25	20 24	eqssi	$$⊢A{+}_{\mathscr{H}}B=\bigcap \left\{x\in {\mathbf{S}}_{\mathscr{H}}|A\cup B\subseteq x\right\}$$