chscllem4

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

	Ref	Expression
Hypotheses	chscl.1	$⊢ φ \to A \in C_{ℋ}$
	chscl.2	$⊢ φ \to B \in C_{ℋ}$
	chscl.3	$⊢ φ \to B \subseteq ⊥ (A)$
	chscl.4	$⊢ φ \to H : ℕ ⟶ A +_{ℋ} B$
	chscl.5	$⊢ φ \to H \underset{v}{⇝} u$
	chscl.6	$⊢ F = (n \in ℕ ⟼ {proj}_{ℎ} (A) (H (n)))$
	chscl.7	$⊢ G = (n \in ℕ ⟼ {proj}_{ℎ} (B) (H (n)))$
Assertion	chscllem4	$⊢ φ \to u \in (A +_{ℋ} B)$

Proof

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

Metamath Proof Explorer

Theorem chscllem4

Proof