Theorem chscllem1

Description: Lemma for chscl . (Contributed by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	chscl.1	$$⊢\phi \to A\in {\mathbf{C}}_{\mathscr{H}}$$
	chscl.2	$$⊢\phi \to B\in {\mathbf{C}}_{\mathscr{H}}$$
	chscl.3	$$⊢\phi \to B\subseteq \perp \left(A\right)$$
	chscl.4	$$⊢\phi \to H:\mathbb{N}⟶A{+}_{\mathscr{H}}B$$
	chscl.5	$$⊢\phi \to H\underset{v}{⇝}u$$
	chscl.6	$$⊢F=\left(n\in \mathbb{N}⟼{\mathrm{proj}}_{ℎ}\left(A\right)\left(H\left(n\right)\right)\right)$$
Assertion	chscllem1	$$⊢\phi \to F:\mathbb{N}⟶A$$

Proof

Step	Hyp	Ref	Expression
1		chscl.1	$$⊢\phi \to A\in {\mathbf{C}}_{\mathscr{H}}$$
2		chscl.2	$$⊢\phi \to B\in {\mathbf{C}}_{\mathscr{H}}$$
3		chscl.3	$$⊢\phi \to B\subseteq \perp \left(A\right)$$
4		chscl.4	$$⊢\phi \to H:\mathbb{N}⟶A{+}_{\mathscr{H}}B$$
5		chscl.5	$$⊢\phi \to H\underset{v}{⇝}u$$
6		chscl.6	$$⊢F=\left(n\in \mathbb{N}⟼{\mathrm{proj}}_{ℎ}\left(A\right)\left(H\left(n\right)\right)\right)$$
7		eqid	$$⊢{\mathrm{proj}}_{ℎ}\left(A\right)\left(H\left(n\right)\right)={\mathrm{proj}}_{ℎ}\left(A\right)\left(H\left(n\right)\right)$$
8	1	adantr	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to A\in {\mathbf{C}}_{\mathscr{H}}$$
9	4	ffvelrnda	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to H\left(n\right)\in \left(A{+}_{\mathscr{H}}B\right)$$
10		chsh	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}\to B\in {\mathbf{S}}_{\mathscr{H}}$$
11	2 10	syl	$$⊢\phi \to B\in {\mathbf{S}}_{\mathscr{H}}$$
12		chsh	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to A\in {\mathbf{S}}_{\mathscr{H}}$$
13	1 12	syl	$$⊢\phi \to A\in {\mathbf{S}}_{\mathscr{H}}$$
14		shocsh	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}\to \perp \left(A\right)\in {\mathbf{S}}_{\mathscr{H}}$$
15	13 14	syl	$$⊢\phi \to \perp \left(A\right)\in {\mathbf{S}}_{\mathscr{H}}$$
16		shless	$$⊢\left(\left(B\in {\mathbf{S}}_{\mathscr{H}}\wedge \perp \left(A\right)\in {\mathbf{S}}_{\mathscr{H}}\wedge A\in {\mathbf{S}}_{\mathscr{H}}\right)\wedge B\subseteq \perp \left(A\right)\right)\to B{+}_{\mathscr{H}}A\subseteq \perp \left(A\right){+}_{\mathscr{H}}A$$
17	11 15 13 3 16	syl31anc	$$⊢\phi \to B{+}_{\mathscr{H}}A\subseteq \perp \left(A\right){+}_{\mathscr{H}}A$$
18		shscom	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\to A{+}_{\mathscr{H}}B=B{+}_{\mathscr{H}}A$$
19	13 11 18	syl2anc	$$⊢\phi \to A{+}_{\mathscr{H}}B=B{+}_{\mathscr{H}}A$$
20		shscom	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge \perp \left(A\right)\in {\mathbf{S}}_{\mathscr{H}}\right)\to A{+}_{\mathscr{H}}\perp \left(A\right)=\perp \left(A\right){+}_{\mathscr{H}}A$$
21	13 15 20	syl2anc	$$⊢\phi \to A{+}_{\mathscr{H}}\perp \left(A\right)=\perp \left(A\right){+}_{\mathscr{H}}A$$
22	17 19 21	3sstr4d	$$⊢\phi \to A{+}_{\mathscr{H}}B\subseteq A{+}_{\mathscr{H}}\perp \left(A\right)$$
23	22	sselda	$$⊢\left(\phi \wedge H\left(n\right)\in \left(A{+}_{\mathscr{H}}B\right)\right)\to H\left(n\right)\in \left(A{+}_{\mathscr{H}}\perp \left(A\right)\right)$$
24	9 23	syldan	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to H\left(n\right)\in \left(A{+}_{\mathscr{H}}\perp \left(A\right)\right)$$
25		pjpreeq	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge H\left(n\right)\in \left(A{+}_{\mathscr{H}}\perp \left(A\right)\right)\right)\to \left({\mathrm{proj}}_{ℎ}\left(A\right)\left(H\left(n\right)\right)={\mathrm{proj}}_{ℎ}\left(A\right)\left(H\left(n\right)\right)\leftrightarrow \left({\mathrm{proj}}_{ℎ}\left(A\right)\left(H\left(n\right)\right)\in A\wedge \exists x\in \perp \left(A\right)H\left(n\right)={\mathrm{proj}}_{ℎ}\left(A\right)\left(H\left(n\right)\right){+}_{ℎ}x\right)\right)$$
26	8 24 25	syl2anc	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to \left({\mathrm{proj}}_{ℎ}\left(A\right)\left(H\left(n\right)\right)={\mathrm{proj}}_{ℎ}\left(A\right)\left(H\left(n\right)\right)\leftrightarrow \left({\mathrm{proj}}_{ℎ}\left(A\right)\left(H\left(n\right)\right)\in A\wedge \exists x\in \perp \left(A\right)H\left(n\right)={\mathrm{proj}}_{ℎ}\left(A\right)\left(H\left(n\right)\right){+}_{ℎ}x\right)\right)$$
27	7 26	mpbii	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to \left({\mathrm{proj}}_{ℎ}\left(A\right)\left(H\left(n\right)\right)\in A\wedge \exists x\in \perp \left(A\right)H\left(n\right)={\mathrm{proj}}_{ℎ}\left(A\right)\left(H\left(n\right)\right){+}_{ℎ}x\right)$$
28	27	simpld	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to {\mathrm{proj}}_{ℎ}\left(A\right)\left(H\left(n\right)\right)\in A$$
29	28 6	fmptd	$$⊢\phi \to F:\mathbb{N}⟶A$$