chscllem3

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)))$
	chscllem3.7	$⊢ φ \to N \in ℕ$
	chscllem3.8	$⊢ φ \to C \in A$
	chscllem3.9	$⊢ φ \to D \in B$
	chscllem3.10	$⊢ φ \to H (N) = C +_{ℎ} D$
Assertion	chscllem3	$⊢ φ \to C = F (N)$

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		chscllem3.7	$⊢ φ \to N \in ℕ$
8		chscllem3.8	$⊢ φ \to C \in A$
9		chscllem3.9	$⊢ φ \to D \in B$
10		chscllem3.10	$⊢ φ \to H (N) = C +_{ℎ} D$
11		2fveq3	$⊢ n = N \to {proj}_{ℎ} (A) (H (n)) = {proj}_{ℎ} (A) (H (N))$
12		fvex	$⊢ {proj}_{ℎ} (A) (H (N)) \in V$
13	11 6 12	fvmpt	$⊢ N \in ℕ \to F (N) = {proj}_{ℎ} (A) (H (N))$
14	7 13	syl	$⊢ φ \to F (N) = {proj}_{ℎ} (A) (H (N))$
15	14	eqcomd	$⊢ φ \to {proj}_{ℎ} (A) (H (N)) = F (N)$
16		chsh	$⊢ B \in C_{ℋ} \to B \in S_{ℋ}$
17	2 16	syl	$⊢ φ \to B \in S_{ℋ}$
18		chsh	$⊢ A \in C_{ℋ} \to A \in S_{ℋ}$
19	1 18	syl	$⊢ φ \to A \in S_{ℋ}$
20		shocsh	$⊢ A \in S_{ℋ} \to ⊥ (A) \in S_{ℋ}$
21	19 20	syl	$⊢ φ \to ⊥ (A) \in S_{ℋ}$
22		shless	$⊢ ((B \in S_{ℋ} \land ⊥ (A) \in S_{ℋ} \land A \in S_{ℋ}) \land B \subseteq ⊥ (A)) \to B +_{ℋ} A \subseteq ⊥ (A) +_{ℋ} A$
23	17 21 19 3 22	syl31anc	$⊢ φ \to B +_{ℋ} A \subseteq ⊥ (A) +_{ℋ} A$
24		shscom	$⊢ (A \in S_{ℋ} \land B \in S_{ℋ}) \to A +_{ℋ} B = B +_{ℋ} A$
25	19 17 24	syl2anc	$⊢ φ \to A +_{ℋ} B = B +_{ℋ} A$
26		shscom	$⊢ (A \in S_{ℋ} \land ⊥ (A) \in S_{ℋ}) \to A +_{ℋ} ⊥ (A) = ⊥ (A) +_{ℋ} A$
27	19 21 26	syl2anc	$⊢ φ \to A +_{ℋ} ⊥ (A) = ⊥ (A) +_{ℋ} A$
28	23 25 27	3sstr4d	$⊢ φ \to A +_{ℋ} B \subseteq A +_{ℋ} ⊥ (A)$
29	4 7	ffvelrnd	$⊢ φ \to H (N) \in (A +_{ℋ} B)$
30	28 29	sseldd	$⊢ φ \to H (N) \in (A +_{ℋ} ⊥ (A))$
31		pjpreeq	$⊢ (A \in C_{ℋ} \land H (N) \in (A +_{ℋ} ⊥ (A))) \to ({proj}_{ℎ} (A) (H (N)) = F (N) \leftrightarrow (F (N) \in A \land \exists z \in ⊥ (A) H (N) = F (N) +_{ℎ} z))$
32	1 30 31	syl2anc	$⊢ φ \to ({proj}_{ℎ} (A) (H (N)) = F (N) \leftrightarrow (F (N) \in A \land \exists z \in ⊥ (A) H (N) = F (N) +_{ℎ} z))$
33	15 32	mpbid	$⊢ φ \to (F (N) \in A \land \exists z \in ⊥ (A) H (N) = F (N) +_{ℎ} z)$
34	33	simprd	$⊢ φ \to \exists z \in ⊥ (A) H (N) = F (N) +_{ℎ} z$
35	19	adantr	$⊢ (φ \land (z \in ⊥ (A) \land H (N) = F (N) +_{ℎ} z)) \to A \in S_{ℋ}$
36	21	adantr	$⊢ (φ \land (z \in ⊥ (A) \land H (N) = F (N) +_{ℎ} z)) \to ⊥ (A) \in S_{ℋ}$
37		ocin	$⊢ A \in S_{ℋ} \to A \cap ⊥ (A) = 0_{ℋ}$
38	19 37	syl	$⊢ φ \to A \cap ⊥ (A) = 0_{ℋ}$
39	38	adantr	$⊢ (φ \land (z \in ⊥ (A) \land H (N) = F (N) +_{ℎ} z)) \to A \cap ⊥ (A) = 0_{ℋ}$
40	8	adantr	$⊢ (φ \land (z \in ⊥ (A) \land H (N) = F (N) +_{ℎ} z)) \to C \in A$
41	3	adantr	$⊢ (φ \land (z \in ⊥ (A) \land H (N) = F (N) +_{ℎ} z)) \to B \subseteq ⊥ (A)$
42	9	adantr	$⊢ (φ \land (z \in ⊥ (A) \land H (N) = F (N) +_{ℎ} z)) \to D \in B$
43	41 42	sseldd	$⊢ (φ \land (z \in ⊥ (A) \land H (N) = F (N) +_{ℎ} z)) \to D \in ⊥ (A)$
44	1 2 3 4 5 6	chscllem1	$⊢ φ \to F : ℕ ⟶ A$
45	44 7	ffvelrnd	$⊢ φ \to F (N) \in A$
46	45	adantr	$⊢ (φ \land (z \in ⊥ (A) \land H (N) = F (N) +_{ℎ} z)) \to F (N) \in A$
47		simprl	$⊢ (φ \land (z \in ⊥ (A) \land H (N) = F (N) +_{ℎ} z)) \to z \in ⊥ (A)$
48	10	adantr	$⊢ (φ \land (z \in ⊥ (A) \land H (N) = F (N) +_{ℎ} z)) \to H (N) = C +_{ℎ} D$
49		simprr	$⊢ (φ \land (z \in ⊥ (A) \land H (N) = F (N) +_{ℎ} z)) \to H (N) = F (N) +_{ℎ} z$
50	48 49	eqtr3d	$⊢ (φ \land (z \in ⊥ (A) \land H (N) = F (N) +_{ℎ} z)) \to C +_{ℎ} D = F (N) +_{ℎ} z$
51	35 36 39 40 43 46 47 50	shuni	$⊢ (φ \land (z \in ⊥ (A) \land H (N) = F (N) +_{ℎ} z)) \to (C = F (N) \land D = z)$
52	51	simpld	$⊢ (φ \land (z \in ⊥ (A) \land H (N) = F (N) +_{ℎ} z)) \to C = F (N)$
53	34 52	rexlimddv	$⊢ φ \to C = F (N)$

Metamath Proof Explorer

Theorem chscllem3

Proof