Theorem sumdmdlem2

Description: Lemma for sumdmdi . (Contributed by NM, 23-Dec-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	sumdmdi.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	sumdmdi.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	sumdmdlem2	$$⊢\forall x\in \mathrm{HAtoms}\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\to A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B$$

Proof

Step	Hyp	Ref	Expression
1		sumdmdi.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		sumdmdi.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3	1 2	chjcli	$$⊢A{\vee }_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}$$
4	3	cheli	$$⊢y\in \left(A{\vee }_{\mathscr{H}}B\right)\to y\in \mathscr{H}$$
5		spansnsh	$$⊢y\in \mathscr{H}\to \mathrm{span}\left(\left\{y\right\}\right)\in {\mathbf{S}}_{\mathscr{H}}$$
6	2	chshii	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}$$
7		shsub2	$$⊢\left(\mathrm{span}\left(\left\{y\right\}\right)\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\to \mathrm{span}\left(\left\{y\right\}\right)\subseteq B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)$$
8	5 6 7	sylancl	$$⊢y\in \mathscr{H}\to \mathrm{span}\left(\left\{y\right\}\right)\subseteq B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)$$
9		spansnid	$$⊢y\in \mathscr{H}\to y\in \mathrm{span}\left(\left\{y\right\}\right)$$
10	8 9	sseldd	$$⊢y\in \mathscr{H}\to y\in \left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)$$
11	10	ad2antrl	$$⊢\left(\forall x\in \mathrm{HAtoms}\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\wedge \left(y\in \mathscr{H}\wedge \neg y\in \left(A{+}_{\mathscr{H}}B\right)\right)\right)\to y\in \left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)$$
12		elin	$$⊢y\in \left(\left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\leftrightarrow \left(y\in \left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\wedge y\in \left(A{\vee }_{\mathscr{H}}B\right)\right)$$
13		df-ne	$$⊢y\ne 0_{ℎ}\leftrightarrow \neg y=0_{ℎ}$$
14		spansna	$$⊢\left(y\in \mathscr{H}\wedge y\ne 0_{ℎ}\right)\to \mathrm{span}\left(\left\{y\right\}\right)\in \mathrm{HAtoms}$$
15	13 14	sylan2br	$$⊢\left(y\in \mathscr{H}\wedge \neg y=0_{ℎ}\right)\to \mathrm{span}\left(\left\{y\right\}\right)\in \mathrm{HAtoms}$$
16		oveq1	$$⊢x=\mathrm{span}\left(\left\{y\right\}\right)\to x{\vee }_{\mathscr{H}}B=\mathrm{span}\left(\left\{y\right\}\right){\vee }_{\mathscr{H}}B$$
17	16	ineq1d	$$⊢x=\mathrm{span}\left(\left\{y\right\}\right)\to \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)=\left(\mathrm{span}\left(\left\{y\right\}\right){\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)$$
18	16	ineq1d	$$⊢x=\mathrm{span}\left(\left\{y\right\}\right)\to \left(x{\vee }_{\mathscr{H}}B\right)\cap A=\left(\mathrm{span}\left(\left\{y\right\}\right){\vee }_{\mathscr{H}}B\right)\cap A$$
19	18	oveq1d	$$⊢x=\mathrm{span}\left(\left\{y\right\}\right)\to \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B=\left(\left(\mathrm{span}\left(\left\{y\right\}\right){\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B$$
20	17 19	sseq12d	$$⊢x=\mathrm{span}\left(\left\{y\right\}\right)\to \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\leftrightarrow \left(\mathrm{span}\left(\left\{y\right\}\right){\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(\mathrm{span}\left(\left\{y\right\}\right){\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)$$
21	20	rspcv	$$⊢\mathrm{span}\left(\left\{y\right\}\right)\in \mathrm{HAtoms}\to \left(\forall x\in \mathrm{HAtoms}\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\to \left(\mathrm{span}\left(\left\{y\right\}\right){\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(\mathrm{span}\left(\left\{y\right\}\right){\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)$$
22	15 21	syl	$$⊢\left(y\in \mathscr{H}\wedge \neg y=0_{ℎ}\right)\to \left(\forall x\in \mathrm{HAtoms}\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\to \left(\mathrm{span}\left(\left\{y\right\}\right){\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(\mathrm{span}\left(\left\{y\right\}\right){\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)$$
23		spansnj	$$⊢\left(B\in {\mathbf{C}}_{\mathscr{H}}\wedge y\in \mathscr{H}\right)\to B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)=B{\vee }_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)$$
24		spansnch	$$⊢y\in \mathscr{H}\to \mathrm{span}\left(\left\{y\right\}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
25		chjcom	$$⊢\left(B\in {\mathbf{C}}_{\mathscr{H}}\wedge \mathrm{span}\left(\left\{y\right\}\right)\in {\mathbf{C}}_{\mathscr{H}}\right)\to B{\vee }_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)=\mathrm{span}\left(\left\{y\right\}\right){\vee }_{\mathscr{H}}B$$
26	24 25	sylan2	$$⊢\left(B\in {\mathbf{C}}_{\mathscr{H}}\wedge y\in \mathscr{H}\right)\to B{\vee }_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)=\mathrm{span}\left(\left\{y\right\}\right){\vee }_{\mathscr{H}}B$$
27	23 26	eqtrd	$$⊢\left(B\in {\mathbf{C}}_{\mathscr{H}}\wedge y\in \mathscr{H}\right)\to B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)=\mathrm{span}\left(\left\{y\right\}\right){\vee }_{\mathscr{H}}B$$
28	2 27	mpan	$$⊢y\in \mathscr{H}\to B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)=\mathrm{span}\left(\left\{y\right\}\right){\vee }_{\mathscr{H}}B$$
29	28	ineq1d	$$⊢y\in \mathscr{H}\to \left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)=\left(\mathrm{span}\left(\left\{y\right\}\right){\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)$$
30	28	ineq1d	$$⊢y\in \mathscr{H}\to \left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\cap A=\left(\mathrm{span}\left(\left\{y\right\}\right){\vee }_{\mathscr{H}}B\right)\cap A$$
31	30	oveq1d	$$⊢y\in \mathscr{H}\to \left(\left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\cap A\right){\vee }_{\mathscr{H}}B=\left(\left(\mathrm{span}\left(\left\{y\right\}\right){\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B$$
32	29 31	sseq12d	$$⊢y\in \mathscr{H}\to \left(\left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\cap A\right){\vee }_{\mathscr{H}}B\leftrightarrow \left(\mathrm{span}\left(\left\{y\right\}\right){\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(\mathrm{span}\left(\left\{y\right\}\right){\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)$$
33	32	adantr	$$⊢\left(y\in \mathscr{H}\wedge \neg y=0_{ℎ}\right)\to \left(\left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\cap A\right){\vee }_{\mathscr{H}}B\leftrightarrow \left(\mathrm{span}\left(\left\{y\right\}\right){\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(\mathrm{span}\left(\left\{y\right\}\right){\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)$$
34	22 33	sylibrd	$$⊢\left(y\in \mathscr{H}\wedge \neg y=0_{ℎ}\right)\to \left(\forall x\in \mathrm{HAtoms}\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\to \left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\cap A\right){\vee }_{\mathscr{H}}B\right)$$
35	34	com12	$$⊢\forall x\in \mathrm{HAtoms}\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\to \left(\left(y\in \mathscr{H}\wedge \neg y=0_{ℎ}\right)\to \left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\cap A\right){\vee }_{\mathscr{H}}B\right)$$
36	35	expdimp	$$⊢\left(\forall x\in \mathrm{HAtoms}\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\wedge y\in \mathscr{H}\right)\to \left(\neg y=0_{ℎ}\to \left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\cap A\right){\vee }_{\mathscr{H}}B\right)$$
37		ssid	$$⊢B\subseteq B$$
38		sneq	$$⊢y=0_{ℎ}\to \left\{y\right\}=\left\{0_{ℎ}\right\}$$
39	38	fveq2d	$$⊢y=0_{ℎ}\to \mathrm{span}\left(\left\{y\right\}\right)=\mathrm{span}\left(\left\{0_{ℎ}\right\}\right)$$
40		spansn0	$$⊢\mathrm{span}\left(\left\{0_{ℎ}\right\}\right)=0_{\mathscr{H}}$$
41	39 40	eqtrdi	$$⊢y=0_{ℎ}\to \mathrm{span}\left(\left\{y\right\}\right)=0_{\mathscr{H}}$$
42	41	oveq2d	$$⊢y=0_{ℎ}\to B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)=B{+}_{\mathscr{H}}{0}_{\mathscr{H}}$$
43	6	shs0i	$$⊢B{+}_{\mathscr{H}}{0}_{\mathscr{H}}=B$$
44	42 43	eqtrdi	$$⊢y=0_{ℎ}\to B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)=B$$
45	44	ineq1d	$$⊢y=0_{ℎ}\to \left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)=B\cap \left(A{\vee }_{\mathscr{H}}B\right)$$
46		inss1	$$⊢B\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq B$$
47	2 1	chub2i	$$⊢B\subseteq A{\vee }_{\mathscr{H}}B$$
48	37 47	ssini	$$⊢B\subseteq B\cap \left(A{\vee }_{\mathscr{H}}B\right)$$
49	46 48	eqssi	$$⊢B\cap \left(A{\vee }_{\mathscr{H}}B\right)=B$$
50	45 49	eqtrdi	$$⊢y=0_{ℎ}\to \left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)=B$$
51	44	ineq1d	$$⊢y=0_{ℎ}\to \left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\cap A=B\cap A$$
52	51	oveq1d	$$⊢y=0_{ℎ}\to \left(\left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\cap A\right){\vee }_{\mathscr{H}}B=\left(B\cap A\right){\vee }_{\mathscr{H}}B$$
53	2 1	chincli	$$⊢B\cap A\in {\mathbf{C}}_{\mathscr{H}}$$
54	53 2	chjcomi	$$⊢\left(B\cap A\right){\vee }_{\mathscr{H}}B=B{\vee }_{\mathscr{H}}\left(B\cap A\right)$$
55	2 1	chabs1i	$$⊢B{\vee }_{\mathscr{H}}\left(B\cap A\right)=B$$
56	54 55	eqtri	$$⊢\left(B\cap A\right){\vee }_{\mathscr{H}}B=B$$
57	52 56	eqtrdi	$$⊢y=0_{ℎ}\to \left(\left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\cap A\right){\vee }_{\mathscr{H}}B=B$$
58	50 57	sseq12d	$$⊢y=0_{ℎ}\to \left(\left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\cap A\right){\vee }_{\mathscr{H}}B\leftrightarrow B\subseteq B\right)$$
59	37 58	mpbiri	$$⊢y=0_{ℎ}\to \left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\cap A\right){\vee }_{\mathscr{H}}B$$
60	36 59	pm2.61d2	$$⊢\left(\forall x\in \mathrm{HAtoms}\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\wedge y\in \mathscr{H}\right)\to \left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\cap A\right){\vee }_{\mathscr{H}}B$$
61	60	adantrr	$$⊢\left(\forall x\in \mathrm{HAtoms}\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\wedge \left(y\in \mathscr{H}\wedge \neg y\in \left(A{+}_{\mathscr{H}}B\right)\right)\right)\to \left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\cap A\right){\vee }_{\mathscr{H}}B$$
62	1 2	sumdmdlem	$$⊢\left(y\in \mathscr{H}\wedge \neg y\in \left(A{+}_{\mathscr{H}}B\right)\right)\to \left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\cap A=B\cap A$$
63	62	oveq1d	$$⊢\left(y\in \mathscr{H}\wedge \neg y\in \left(A{+}_{\mathscr{H}}B\right)\right)\to \left(\left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\cap A\right){\vee }_{\mathscr{H}}B=\left(B\cap A\right){\vee }_{\mathscr{H}}B$$
64	63 56	eqtrdi	$$⊢\left(y\in \mathscr{H}\wedge \neg y\in \left(A{+}_{\mathscr{H}}B\right)\right)\to \left(\left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\cap A\right){\vee }_{\mathscr{H}}B=B$$
65	1	chshii	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}$$
66	6 65	shsub2i	$$⊢B\subseteq A{+}_{\mathscr{H}}B$$
67	64 66	eqsstrdi	$$⊢\left(y\in \mathscr{H}\wedge \neg y\in \left(A{+}_{\mathscr{H}}B\right)\right)\to \left(\left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\cap A\right){\vee }_{\mathscr{H}}B\subseteq A{+}_{\mathscr{H}}B$$
68	67	adantl	$$⊢\left(\forall x\in \mathrm{HAtoms}\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\wedge \left(y\in \mathscr{H}\wedge \neg y\in \left(A{+}_{\mathscr{H}}B\right)\right)\right)\to \left(\left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\cap A\right){\vee }_{\mathscr{H}}B\subseteq A{+}_{\mathscr{H}}B$$
69	61 68	sstrd	$$⊢\left(\forall x\in \mathrm{HAtoms}\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\wedge \left(y\in \mathscr{H}\wedge \neg y\in \left(A{+}_{\mathscr{H}}B\right)\right)\right)\to \left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A{+}_{\mathscr{H}}B$$
70	69	sseld	$$⊢\left(\forall x\in \mathrm{HAtoms}\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\wedge \left(y\in \mathscr{H}\wedge \neg y\in \left(A{+}_{\mathscr{H}}B\right)\right)\right)\to \left(y\in \left(\left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\to y\in \left(A{+}_{\mathscr{H}}B\right)\right)$$
71	12 70	syl5bir	$$⊢\left(\forall x\in \mathrm{HAtoms}\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\wedge \left(y\in \mathscr{H}\wedge \neg y\in \left(A{+}_{\mathscr{H}}B\right)\right)\right)\to \left(\left(y\in \left(B{+}_{\mathscr{H}}\mathrm{span}\left(\left\{y\right\}\right)\right)\wedge y\in \left(A{\vee }_{\mathscr{H}}B\right)\right)\to y\in \left(A{+}_{\mathscr{H}}B\right)\right)$$
72	11 71	mpand	$$⊢\left(\forall x\in \mathrm{HAtoms}\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\wedge \left(y\in \mathscr{H}\wedge \neg y\in \left(A{+}_{\mathscr{H}}B\right)\right)\right)\to \left(y\in \left(A{\vee }_{\mathscr{H}}B\right)\to y\in \left(A{+}_{\mathscr{H}}B\right)\right)$$
73	72	exp32	$$⊢\forall x\in \mathrm{HAtoms}\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\to \left(y\in \mathscr{H}\to \left(\neg y\in \left(A{+}_{\mathscr{H}}B\right)\to \left(y\in \left(A{\vee }_{\mathscr{H}}B\right)\to y\in \left(A{+}_{\mathscr{H}}B\right)\right)\right)\right)$$
74	73	com34	$$⊢\forall x\in \mathrm{HAtoms}\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\to \left(y\in \mathscr{H}\to \left(y\in \left(A{\vee }_{\mathscr{H}}B\right)\to \left(\neg y\in \left(A{+}_{\mathscr{H}}B\right)\to y\in \left(A{+}_{\mathscr{H}}B\right)\right)\right)\right)$$
75		pm2.18	$$⊢\left(\neg y\in \left(A{+}_{\mathscr{H}}B\right)\to y\in \left(A{+}_{\mathscr{H}}B\right)\right)\to y\in \left(A{+}_{\mathscr{H}}B\right)$$
76	74 75	syl8	$$⊢\forall x\in \mathrm{HAtoms}\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\to \left(y\in \mathscr{H}\to \left(y\in \left(A{\vee }_{\mathscr{H}}B\right)\to y\in \left(A{+}_{\mathscr{H}}B\right)\right)\right)$$
77	4 76	syl5	$$⊢\forall x\in \mathrm{HAtoms}\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\to \left(y\in \left(A{\vee }_{\mathscr{H}}B\right)\to \left(y\in \left(A{\vee }_{\mathscr{H}}B\right)\to y\in \left(A{+}_{\mathscr{H}}B\right)\right)\right)$$
78	77	pm2.43d	$$⊢\forall x\in \mathrm{HAtoms}\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\to \left(y\in \left(A{\vee }_{\mathscr{H}}B\right)\to y\in \left(A{+}_{\mathscr{H}}B\right)\right)$$
79	78	ssrdv	$$⊢\forall x\in \mathrm{HAtoms}\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\to A{\vee }_{\mathscr{H}}B\subseteq A{+}_{\mathscr{H}}B$$
80	1 2	chsleji	$$⊢A{+}_{\mathscr{H}}B\subseteq A{\vee }_{\mathscr{H}}B$$
81	79 80	jctil	$$⊢\forall x\in \mathrm{HAtoms}\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\to \left(A{+}_{\mathscr{H}}B\subseteq A{\vee }_{\mathscr{H}}B\wedge A{\vee }_{\mathscr{H}}B\subseteq A{+}_{\mathscr{H}}B\right)$$
82		eqss	$$⊢A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B\leftrightarrow \left(A{+}_{\mathscr{H}}B\subseteq A{\vee }_{\mathscr{H}}B\wedge A{\vee }_{\mathscr{H}}B\subseteq A{+}_{\mathscr{H}}B\right)$$
83	81 82	sylibr	$$⊢\forall x\in \mathrm{HAtoms}\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\to A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B$$