cdj3lem2b

Description: Lemma for cdj3i . The first-component function S is bounded if the subspaces are completely disjoint. (Contributed by NM, 26-May-2005) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cdj3lem2.1	$⊢ A \in S_{ℋ}$
	cdj3lem2.2	$⊢ B \in S_{ℋ}$
	cdj3lem2.3	$⊢ S = (x \in (A +_{ℋ} B) ⟼ (ι z \in A \| \exists w \in B x = z +_{ℎ} w))$
Assertion	cdj3lem2b	$⊢ \exists v \in ℝ (0 < v \land \forall x \in A \forall y \in B {norm}_{ℎ} (x) + {norm}_{ℎ} (y) \leq v {norm}_{ℎ} (x +_{ℎ} y)) \to \exists v \in ℝ (0 < v \land \forall u \in (A +_{ℋ} B) {norm}_{ℎ} (S (u)) \leq v {norm}_{ℎ} (u))$

Proof

Step	Hyp	Ref	Expression
1		cdj3lem2.1	$⊢ A \in S_{ℋ}$
2		cdj3lem2.2	$⊢ B \in S_{ℋ}$
3		cdj3lem2.3	$⊢ S = (x \in (A +_{ℋ} B) ⟼ (ι z \in A \| \exists w \in B x = z +_{ℎ} w))$
4	1 2	cdj3lem1	$⊢ \exists v \in ℝ (0 < v \land \forall x \in A \forall y \in B {norm}_{ℎ} (x) + {norm}_{ℎ} (y) \leq v {norm}_{ℎ} (x +_{ℎ} y)) \to A \cap B = 0_{ℋ}$
5	1 2	shseli	$⊢ u \in (A +_{ℋ} B) \leftrightarrow \exists t \in A \exists h \in B u = t +_{ℎ} h$
6	5	biimpi	$⊢ u \in (A +_{ℋ} B) \to \exists t \in A \exists h \in B u = t +_{ℎ} h$
7		fveq2	$⊢ x = t \to {norm}_{ℎ} (x) = {norm}_{ℎ} (t)$
8	7	oveq1d	$⊢ x = t \to {norm}_{ℎ} (x) + {norm}_{ℎ} (y) = {norm}_{ℎ} (t) + {norm}_{ℎ} (y)$
9		fvoveq1	$⊢ x = t \to {norm}_{ℎ} (x +_{ℎ} y) = {norm}_{ℎ} (t +_{ℎ} y)$
10	9	oveq2d	$⊢ x = t \to v {norm}_{ℎ} (x +_{ℎ} y) = v {norm}_{ℎ} (t +_{ℎ} y)$
11	8 10	breq12d	$⊢ x = t \to ({norm}_{ℎ} (x) + {norm}_{ℎ} (y) \leq v {norm}_{ℎ} (x +_{ℎ} y) \leftrightarrow {norm}_{ℎ} (t) + {norm}_{ℎ} (y) \leq v {norm}_{ℎ} (t +_{ℎ} y))$
12		fveq2	$⊢ y = h \to {norm}_{ℎ} (y) = {norm}_{ℎ} (h)$
13	12	oveq2d	$⊢ y = h \to {norm}_{ℎ} (t) + {norm}_{ℎ} (y) = {norm}_{ℎ} (t) + {norm}_{ℎ} (h)$
14		oveq2	$⊢ y = h \to t +_{ℎ} y = t +_{ℎ} h$
15	14	fveq2d	$⊢ y = h \to {norm}_{ℎ} (t +_{ℎ} y) = {norm}_{ℎ} (t +_{ℎ} h)$
16	15	oveq2d	$⊢ y = h \to v {norm}_{ℎ} (t +_{ℎ} y) = v {norm}_{ℎ} (t +_{ℎ} h)$
17	13 16	breq12d	$⊢ y = h \to ({norm}_{ℎ} (t) + {norm}_{ℎ} (y) \leq v {norm}_{ℎ} (t +_{ℎ} y) \leftrightarrow {norm}_{ℎ} (t) + {norm}_{ℎ} (h) \leq v {norm}_{ℎ} (t +_{ℎ} h))$
18	11 17	rspc2v	$⊢ (t \in A \land h \in B) \to (\forall x \in A \forall y \in B {norm}_{ℎ} (x) + {norm}_{ℎ} (y) \leq v {norm}_{ℎ} (x +_{ℎ} y) \to {norm}_{ℎ} (t) + {norm}_{ℎ} (h) \leq v {norm}_{ℎ} (t +_{ℎ} h))$
19	1 2 3	cdj3lem2	$⊢ (t \in A \land h \in B \land A \cap B = 0_{ℋ}) \to S (t +_{ℎ} h) = t$
20	19	3expa	$⊢ ((t \in A \land h \in B) \land A \cap B = 0_{ℋ}) \to S (t +_{ℎ} h) = t$
21	20	fveq2d	$⊢ ((t \in A \land h \in B) \land A \cap B = 0_{ℋ}) \to {norm}_{ℎ} (S (t +_{ℎ} h)) = {norm}_{ℎ} (t)$
22	21	ad2ant2r	$⊢ (((t \in A \land h \in B) \land {norm}_{ℎ} (t) + {norm}_{ℎ} (h) \leq v {norm}_{ℎ} (t +_{ℎ} h)) \land (A \cap B = 0_{ℋ} \land v \in ℝ)) \to {norm}_{ℎ} (S (t +_{ℎ} h)) = {norm}_{ℎ} (t)$
23	2	sheli	$⊢ h \in B \to h \in ℋ$
24		normge0	$⊢ h \in ℋ \to 0 \leq {norm}_{ℎ} (h)$
25	23 24	syl	$⊢ h \in B \to 0 \leq {norm}_{ℎ} (h)$
26	25	adantl	$⊢ (t \in A \land h \in B) \to 0 \leq {norm}_{ℎ} (h)$
27	1	sheli	$⊢ t \in A \to t \in ℋ$
28		normcl	$⊢ t \in ℋ \to {norm}_{ℎ} (t) \in ℝ$
29	27 28	syl	$⊢ t \in A \to {norm}_{ℎ} (t) \in ℝ$
30		normcl	$⊢ h \in ℋ \to {norm}_{ℎ} (h) \in ℝ$
31	23 30	syl	$⊢ h \in B \to {norm}_{ℎ} (h) \in ℝ$
32		addge01	$⊢ ({norm}_{ℎ} (t) \in ℝ \land {norm}_{ℎ} (h) \in ℝ) \to (0 \leq {norm}_{ℎ} (h) \leftrightarrow {norm}_{ℎ} (t) \leq {norm}_{ℎ} (t) + {norm}_{ℎ} (h))$
33	29 31 32	syl2an	$⊢ (t \in A \land h \in B) \to (0 \leq {norm}_{ℎ} (h) \leftrightarrow {norm}_{ℎ} (t) \leq {norm}_{ℎ} (t) + {norm}_{ℎ} (h))$
34	26 33	mpbid	$⊢ (t \in A \land h \in B) \to {norm}_{ℎ} (t) \leq {norm}_{ℎ} (t) + {norm}_{ℎ} (h)$
35	34	adantr	$⊢ ((t \in A \land h \in B) \land v \in ℝ) \to {norm}_{ℎ} (t) \leq {norm}_{ℎ} (t) + {norm}_{ℎ} (h)$
36	29	ad2antrr	$⊢ ((t \in A \land h \in B) \land v \in ℝ) \to {norm}_{ℎ} (t) \in ℝ$
37		readdcl	$⊢ ({norm}_{ℎ} (t) \in ℝ \land {norm}_{ℎ} (h) \in ℝ) \to {norm}_{ℎ} (t) + {norm}_{ℎ} (h) \in ℝ$
38	29 31 37	syl2an	$⊢ (t \in A \land h \in B) \to {norm}_{ℎ} (t) + {norm}_{ℎ} (h) \in ℝ$
39	38	adantr	$⊢ ((t \in A \land h \in B) \land v \in ℝ) \to {norm}_{ℎ} (t) + {norm}_{ℎ} (h) \in ℝ$
40		hvaddcl	$⊢ (t \in ℋ \land h \in ℋ) \to t +_{ℎ} h \in ℋ$
41	27 23 40	syl2an	$⊢ (t \in A \land h \in B) \to t +_{ℎ} h \in ℋ$
42		normcl	$⊢ t +_{ℎ} h \in ℋ \to {norm}_{ℎ} (t +_{ℎ} h) \in ℝ$
43	41 42	syl	$⊢ (t \in A \land h \in B) \to {norm}_{ℎ} (t +_{ℎ} h) \in ℝ$
44		remulcl	$⊢ (v \in ℝ \land {norm}_{ℎ} (t +_{ℎ} h) \in ℝ) \to v {norm}_{ℎ} (t +_{ℎ} h) \in ℝ$
45	43 44	sylan2	$⊢ (v \in ℝ \land (t \in A \land h \in B)) \to v {norm}_{ℎ} (t +_{ℎ} h) \in ℝ$
46	45	ancoms	$⊢ ((t \in A \land h \in B) \land v \in ℝ) \to v {norm}_{ℎ} (t +_{ℎ} h) \in ℝ$
47		letr	$⊢ ({norm}_{ℎ} (t) \in ℝ \land {norm}_{ℎ} (t) + {norm}_{ℎ} (h) \in ℝ \land v {norm}_{ℎ} (t +_{ℎ} h) \in ℝ) \to (({norm}_{ℎ} (t) \leq {norm}_{ℎ} (t) + {norm}_{ℎ} (h) \land {norm}_{ℎ} (t) + {norm}_{ℎ} (h) \leq v {norm}_{ℎ} (t +_{ℎ} h)) \to {norm}_{ℎ} (t) \leq v {norm}_{ℎ} (t +_{ℎ} h))$
48	36 39 46 47	syl3anc	$⊢ ((t \in A \land h \in B) \land v \in ℝ) \to (({norm}_{ℎ} (t) \leq {norm}_{ℎ} (t) + {norm}_{ℎ} (h) \land {norm}_{ℎ} (t) + {norm}_{ℎ} (h) \leq v {norm}_{ℎ} (t +_{ℎ} h)) \to {norm}_{ℎ} (t) \leq v {norm}_{ℎ} (t +_{ℎ} h))$
49	35 48	mpand	$⊢ ((t \in A \land h \in B) \land v \in ℝ) \to ({norm}_{ℎ} (t) + {norm}_{ℎ} (h) \leq v {norm}_{ℎ} (t +_{ℎ} h) \to {norm}_{ℎ} (t) \leq v {norm}_{ℎ} (t +_{ℎ} h))$
50	49	imp	$⊢ (((t \in A \land h \in B) \land v \in ℝ) \land {norm}_{ℎ} (t) + {norm}_{ℎ} (h) \leq v {norm}_{ℎ} (t +_{ℎ} h)) \to {norm}_{ℎ} (t) \leq v {norm}_{ℎ} (t +_{ℎ} h)$
51	50	an32s	$⊢ (((t \in A \land h \in B) \land {norm}_{ℎ} (t) + {norm}_{ℎ} (h) \leq v {norm}_{ℎ} (t +_{ℎ} h)) \land v \in ℝ) \to {norm}_{ℎ} (t) \leq v {norm}_{ℎ} (t +_{ℎ} h)$
52	51	adantrl	$⊢ (((t \in A \land h \in B) \land {norm}_{ℎ} (t) + {norm}_{ℎ} (h) \leq v {norm}_{ℎ} (t +_{ℎ} h)) \land (A \cap B = 0_{ℋ} \land v \in ℝ)) \to {norm}_{ℎ} (t) \leq v {norm}_{ℎ} (t +_{ℎ} h)$
53	22 52	eqbrtrd	$⊢ (((t \in A \land h \in B) \land {norm}_{ℎ} (t) + {norm}_{ℎ} (h) \leq v {norm}_{ℎ} (t +_{ℎ} h)) \land (A \cap B = 0_{ℋ} \land v \in ℝ)) \to {norm}_{ℎ} (S (t +_{ℎ} h)) \leq v {norm}_{ℎ} (t +_{ℎ} h)$
54		2fveq3	$⊢ u = t +_{ℎ} h \to {norm}_{ℎ} (S (u)) = {norm}_{ℎ} (S (t +_{ℎ} h))$
55		fveq2	$⊢ u = t +_{ℎ} h \to {norm}_{ℎ} (u) = {norm}_{ℎ} (t +_{ℎ} h)$
56	55	oveq2d	$⊢ u = t +_{ℎ} h \to v {norm}_{ℎ} (u) = v {norm}_{ℎ} (t +_{ℎ} h)$
57	54 56	breq12d	$⊢ u = t +_{ℎ} h \to ({norm}_{ℎ} (S (u)) \leq v {norm}_{ℎ} (u) \leftrightarrow {norm}_{ℎ} (S (t +_{ℎ} h)) \leq v {norm}_{ℎ} (t +_{ℎ} h))$
58	53 57	syl5ibrcom	$⊢ (((t \in A \land h \in B) \land {norm}_{ℎ} (t) + {norm}_{ℎ} (h) \leq v {norm}_{ℎ} (t +_{ℎ} h)) \land (A \cap B = 0_{ℋ} \land v \in ℝ)) \to (u = t +_{ℎ} h \to {norm}_{ℎ} (S (u)) \leq v {norm}_{ℎ} (u))$
59	58	exp31	$⊢ (t \in A \land h \in B) \to ({norm}_{ℎ} (t) + {norm}_{ℎ} (h) \leq v {norm}_{ℎ} (t +_{ℎ} h) \to ((A \cap B = 0_{ℋ} \land v \in ℝ) \to (u = t +_{ℎ} h \to {norm}_{ℎ} (S (u)) \leq v {norm}_{ℎ} (u))))$
60	18 59	syld	$⊢ (t \in A \land h \in B) \to (\forall x \in A \forall y \in B {norm}_{ℎ} (x) + {norm}_{ℎ} (y) \leq v {norm}_{ℎ} (x +_{ℎ} y) \to ((A \cap B = 0_{ℋ} \land v \in ℝ) \to (u = t +_{ℎ} h \to {norm}_{ℎ} (S (u)) \leq v {norm}_{ℎ} (u))))$
61	60	com14	$⊢ u = t +_{ℎ} h \to (\forall x \in A \forall y \in B {norm}_{ℎ} (x) + {norm}_{ℎ} (y) \leq v {norm}_{ℎ} (x +_{ℎ} y) \to ((A \cap B = 0_{ℋ} \land v \in ℝ) \to ((t \in A \land h \in B) \to {norm}_{ℎ} (S (u)) \leq v {norm}_{ℎ} (u))))$
62	61	com4t	$⊢ (A \cap B = 0_{ℋ} \land v \in ℝ) \to ((t \in A \land h \in B) \to (u = t +_{ℎ} h \to (\forall x \in A \forall y \in B {norm}_{ℎ} (x) + {norm}_{ℎ} (y) \leq v {norm}_{ℎ} (x +_{ℎ} y) \to {norm}_{ℎ} (S (u)) \leq v {norm}_{ℎ} (u))))$
63	62	rexlimdvv	$⊢ (A \cap B = 0_{ℋ} \land v \in ℝ) \to (\exists t \in A \exists h \in B u = t +_{ℎ} h \to (\forall x \in A \forall y \in B {norm}_{ℎ} (x) + {norm}_{ℎ} (y) \leq v {norm}_{ℎ} (x +_{ℎ} y) \to {norm}_{ℎ} (S (u)) \leq v {norm}_{ℎ} (u)))$
64	6 63	syl5com	$⊢ u \in (A +_{ℋ} B) \to ((A \cap B = 0_{ℋ} \land v \in ℝ) \to (\forall x \in A \forall y \in B {norm}_{ℎ} (x) + {norm}_{ℎ} (y) \leq v {norm}_{ℎ} (x +_{ℎ} y) \to {norm}_{ℎ} (S (u)) \leq v {norm}_{ℎ} (u)))$
65	64	com3l	$⊢ (A \cap B = 0_{ℋ} \land v \in ℝ) \to (\forall x \in A \forall y \in B {norm}_{ℎ} (x) + {norm}_{ℎ} (y) \leq v {norm}_{ℎ} (x +_{ℎ} y) \to (u \in (A +_{ℋ} B) \to {norm}_{ℎ} (S (u)) \leq v {norm}_{ℎ} (u)))$
66	65	ralrimdv	$⊢ (A \cap B = 0_{ℋ} \land v \in ℝ) \to (\forall x \in A \forall y \in B {norm}_{ℎ} (x) + {norm}_{ℎ} (y) \leq v {norm}_{ℎ} (x +_{ℎ} y) \to \forall u \in (A +_{ℋ} B) {norm}_{ℎ} (S (u)) \leq v {norm}_{ℎ} (u))$
67	66	anim2d	$⊢ (A \cap B = 0_{ℋ} \land v \in ℝ) \to ((0 < v \land \forall x \in A \forall y \in B {norm}_{ℎ} (x) + {norm}_{ℎ} (y) \leq v {norm}_{ℎ} (x +_{ℎ} y)) \to (0 < v \land \forall u \in (A +_{ℋ} B) {norm}_{ℎ} (S (u)) \leq v {norm}_{ℎ} (u)))$
68	67	reximdva	$⊢ A \cap B = 0_{ℋ} \to (\exists v \in ℝ (0 < v \land \forall x \in A \forall y \in B {norm}_{ℎ} (x) + {norm}_{ℎ} (y) \leq v {norm}_{ℎ} (x +_{ℎ} y)) \to \exists v \in ℝ (0 < v \land \forall u \in (A +_{ℋ} B) {norm}_{ℎ} (S (u)) \leq v {norm}_{ℎ} (u)))$
69	4 68	mpcom	$⊢ \exists v \in ℝ (0 < v \land \forall x \in A \forall y \in B {norm}_{ℎ} (x) + {norm}_{ℎ} (y) \leq v {norm}_{ℎ} (x +_{ℎ} y)) \to \exists v \in ℝ (0 < v \land \forall u \in (A +_{ℋ} B) {norm}_{ℎ} (S (u)) \leq v {norm}_{ℎ} (u))$

Metamath Proof Explorer

Theorem cdj3lem2b

Proof