# Metamath Proof Explorer

## Theorem chscllem4

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}}_{ℋ}$
chscl.2 ${⊢}{\phi }\to {B}\in {\mathbf{C}}_{ℋ}$
chscl.3 ${⊢}{\phi }\to {B}\subseteq \perp \left({A}\right)$
chscl.4 ${⊢}{\phi }\to {H}:ℕ⟶{A}{+}_{ℋ}{B}$
chscl.5
chscl.6 ${⊢}{F}=\left({n}\in ℕ⟼{\mathrm{proj}}_{ℎ}\left({A}\right)\left({H}\left({n}\right)\right)\right)$
chscl.7 ${⊢}{G}=\left({n}\in ℕ⟼{\mathrm{proj}}_{ℎ}\left({B}\right)\left({H}\left({n}\right)\right)\right)$
Assertion chscllem4 ${⊢}{\phi }\to {u}\in \left({A}{+}_{ℋ}{B}\right)$

### Proof

Step Hyp Ref Expression
1 chscl.1 ${⊢}{\phi }\to {A}\in {\mathbf{C}}_{ℋ}$
2 chscl.2 ${⊢}{\phi }\to {B}\in {\mathbf{C}}_{ℋ}$
3 chscl.3 ${⊢}{\phi }\to {B}\subseteq \perp \left({A}\right)$
4 chscl.4 ${⊢}{\phi }\to {H}:ℕ⟶{A}{+}_{ℋ}{B}$
5 chscl.5
6 chscl.6 ${⊢}{F}=\left({n}\in ℕ⟼{\mathrm{proj}}_{ℎ}\left({A}\right)\left({H}\left({n}\right)\right)\right)$
7 chscl.7 ${⊢}{G}=\left({n}\in ℕ⟼{\mathrm{proj}}_{ℎ}\left({B}\right)\left({H}\left({n}\right)\right)\right)$
8 hlimf
9 ffun
10 8 9 ax-mp
11 funbrfv
12 10 5 11 mpsyl
13 4 feqmptd ${⊢}{\phi }\to {H}=\left({k}\in ℕ⟼{H}\left({k}\right)\right)$
14 4 ffvelrnda ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {H}\left({k}\right)\in \left({A}{+}_{ℋ}{B}\right)$
15 chsh ${⊢}{A}\in {\mathbf{C}}_{ℋ}\to {A}\in {\mathbf{S}}_{ℋ}$
16 1 15 syl ${⊢}{\phi }\to {A}\in {\mathbf{S}}_{ℋ}$
17 chsh ${⊢}{B}\in {\mathbf{C}}_{ℋ}\to {B}\in {\mathbf{S}}_{ℋ}$
18 2 17 syl ${⊢}{\phi }\to {B}\in {\mathbf{S}}_{ℋ}$
19 shsel ${⊢}\left({A}\in {\mathbf{S}}_{ℋ}\wedge {B}\in {\mathbf{S}}_{ℋ}\right)\to \left({H}\left({k}\right)\in \left({A}{+}_{ℋ}{B}\right)↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{H}\left({k}\right)={x}{+}_{ℎ}{y}\right)$
20 16 18 19 syl2anc ${⊢}{\phi }\to \left({H}\left({k}\right)\in \left({A}{+}_{ℋ}{B}\right)↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{H}\left({k}\right)={x}{+}_{ℎ}{y}\right)$
21 20 biimpa ${⊢}\left({\phi }\wedge {H}\left({k}\right)\in \left({A}{+}_{ℋ}{B}\right)\right)\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{H}\left({k}\right)={x}{+}_{ℎ}{y}$
22 14 21 syldan ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{H}\left({k}\right)={x}{+}_{ℎ}{y}$
23 simp3 ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\wedge {H}\left({k}\right)={x}{+}_{ℎ}{y}\right)\to {H}\left({k}\right)={x}{+}_{ℎ}{y}$
24 simp1l ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\wedge {H}\left({k}\right)={x}{+}_{ℎ}{y}\right)\to {\phi }$
25 24 1 syl ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\wedge {H}\left({k}\right)={x}{+}_{ℎ}{y}\right)\to {A}\in {\mathbf{C}}_{ℋ}$
26 24 2 syl ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\wedge {H}\left({k}\right)={x}{+}_{ℎ}{y}\right)\to {B}\in {\mathbf{C}}_{ℋ}$
27 24 3 syl ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\wedge {H}\left({k}\right)={x}{+}_{ℎ}{y}\right)\to {B}\subseteq \perp \left({A}\right)$
28 24 4 syl ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\wedge {H}\left({k}\right)={x}{+}_{ℎ}{y}\right)\to {H}:ℕ⟶{A}{+}_{ℋ}{B}$
29 24 5 syl
30 simp1r ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\wedge {H}\left({k}\right)={x}{+}_{ℎ}{y}\right)\to {k}\in ℕ$
31 simp2l ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\wedge {H}\left({k}\right)={x}{+}_{ℎ}{y}\right)\to {x}\in {A}$
32 simp2r ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\wedge {H}\left({k}\right)={x}{+}_{ℎ}{y}\right)\to {y}\in {B}$
33 25 26 27 28 29 6 30 31 32 23 chscllem3 ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\wedge {H}\left({k}\right)={x}{+}_{ℎ}{y}\right)\to {x}={F}\left({k}\right)$
34 chsscon2 ${⊢}\left({B}\in {\mathbf{C}}_{ℋ}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to \left({B}\subseteq \perp \left({A}\right)↔{A}\subseteq \perp \left({B}\right)\right)$
35 2 1 34 syl2anc ${⊢}{\phi }\to \left({B}\subseteq \perp \left({A}\right)↔{A}\subseteq \perp \left({B}\right)\right)$
36 3 35 mpbid ${⊢}{\phi }\to {A}\subseteq \perp \left({B}\right)$
37 24 36 syl ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\wedge {H}\left({k}\right)={x}{+}_{ℎ}{y}\right)\to {A}\subseteq \perp \left({B}\right)$
38 shscom ${⊢}\left({A}\in {\mathbf{S}}_{ℋ}\wedge {B}\in {\mathbf{S}}_{ℋ}\right)\to {A}{+}_{ℋ}{B}={B}{+}_{ℋ}{A}$
39 16 18 38 syl2anc ${⊢}{\phi }\to {A}{+}_{ℋ}{B}={B}{+}_{ℋ}{A}$
40 39 feq3d ${⊢}{\phi }\to \left({H}:ℕ⟶{A}{+}_{ℋ}{B}↔{H}:ℕ⟶{B}{+}_{ℋ}{A}\right)$
41 4 40 mpbid ${⊢}{\phi }\to {H}:ℕ⟶{B}{+}_{ℋ}{A}$
42 24 41 syl ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\wedge {H}\left({k}\right)={x}{+}_{ℎ}{y}\right)\to {H}:ℕ⟶{B}{+}_{ℋ}{A}$
43 shss ${⊢}{A}\in {\mathbf{S}}_{ℋ}\to {A}\subseteq ℋ$
44 16 43 syl ${⊢}{\phi }\to {A}\subseteq ℋ$
45 24 44 syl ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\wedge {H}\left({k}\right)={x}{+}_{ℎ}{y}\right)\to {A}\subseteq ℋ$
46 45 31 sseldd ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\wedge {H}\left({k}\right)={x}{+}_{ℎ}{y}\right)\to {x}\in ℋ$
47 shss ${⊢}{B}\in {\mathbf{S}}_{ℋ}\to {B}\subseteq ℋ$
48 18 47 syl ${⊢}{\phi }\to {B}\subseteq ℋ$
49 24 48 syl ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\wedge {H}\left({k}\right)={x}{+}_{ℎ}{y}\right)\to {B}\subseteq ℋ$
50 49 32 sseldd ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\wedge {H}\left({k}\right)={x}{+}_{ℎ}{y}\right)\to {y}\in ℋ$
51 ax-hvcom ${⊢}\left({x}\in ℋ\wedge {y}\in ℋ\right)\to {x}{+}_{ℎ}{y}={y}{+}_{ℎ}{x}$
52 46 50 51 syl2anc ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\wedge {H}\left({k}\right)={x}{+}_{ℎ}{y}\right)\to {x}{+}_{ℎ}{y}={y}{+}_{ℎ}{x}$
53 23 52 eqtrd ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\wedge {H}\left({k}\right)={x}{+}_{ℎ}{y}\right)\to {H}\left({k}\right)={y}{+}_{ℎ}{x}$
54 26 25 37 42 29 7 30 32 31 53 chscllem3 ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\wedge {H}\left({k}\right)={x}{+}_{ℎ}{y}\right)\to {y}={G}\left({k}\right)$
55 33 54 oveq12d ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\wedge {H}\left({k}\right)={x}{+}_{ℎ}{y}\right)\to {x}{+}_{ℎ}{y}={F}\left({k}\right){+}_{ℎ}{G}\left({k}\right)$
56 23 55 eqtrd ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\wedge {H}\left({k}\right)={x}{+}_{ℎ}{y}\right)\to {H}\left({k}\right)={F}\left({k}\right){+}_{ℎ}{G}\left({k}\right)$
57 56 3exp ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to \left(\left({x}\in {A}\wedge {y}\in {B}\right)\to \left({H}\left({k}\right)={x}{+}_{ℎ}{y}\to {H}\left({k}\right)={F}\left({k}\right){+}_{ℎ}{G}\left({k}\right)\right)\right)$
58 57 rexlimdvv ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{H}\left({k}\right)={x}{+}_{ℎ}{y}\to {H}\left({k}\right)={F}\left({k}\right){+}_{ℎ}{G}\left({k}\right)\right)$
59 22 58 mpd ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {H}\left({k}\right)={F}\left({k}\right){+}_{ℎ}{G}\left({k}\right)$
60 59 mpteq2dva ${⊢}{\phi }\to \left({k}\in ℕ⟼{H}\left({k}\right)\right)=\left({k}\in ℕ⟼{F}\left({k}\right){+}_{ℎ}{G}\left({k}\right)\right)$
61 13 60 eqtrd ${⊢}{\phi }\to {H}=\left({k}\in ℕ⟼{F}\left({k}\right){+}_{ℎ}{G}\left({k}\right)\right)$
62 1 2 3 4 5 6 chscllem1 ${⊢}{\phi }\to {F}:ℕ⟶{A}$
63 62 44 fssd ${⊢}{\phi }\to {F}:ℕ⟶ℋ$
64 2 1 36 41 5 7 chscllem1 ${⊢}{\phi }\to {G}:ℕ⟶{B}$
65 64 48 fssd ${⊢}{\phi }\to {G}:ℕ⟶ℋ$
66 1 2 3 4 5 6 chscllem2
67 funfvbrb
68 10 67 ax-mp
69 66 68 sylib
70 2 1 36 41 5 7 chscllem2
71 funfvbrb
72 10 71 ax-mp
73 70 72 sylib
74 eqid ${⊢}\left({k}\in ℕ⟼{F}\left({k}\right){+}_{ℎ}{G}\left({k}\right)\right)=\left({k}\in ℕ⟼{F}\left({k}\right){+}_{ℎ}{G}\left({k}\right)\right)$
75 63 65 69 73 74 hlimadd
76 61 75 eqbrtrd
77 funbrfv
78 10 76 77 mpsyl
79 12 78 eqtr3d
80 fvex
81 80 chlimi
82 1 62 69 81 syl3anc
83 fvex
84 83 chlimi
85 2 64 73 84 syl3anc
86 shsva
87 16 18 86 syl2anc
88 82 85 87 mp2and
89 79 88 eqeltrd ${⊢}{\phi }\to {u}\in \left({A}{+}_{ℋ}{B}\right)$