cnlnadjlem6

Description: Lemma for cnlnadji . F is linear. (Contributed by NM, 17-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cnlnadjlem.1	$⊢ T \in LinOp$
	cnlnadjlem.2	$⊢ T \in ContOp$
	cnlnadjlem.3	$⊢ G = (g \in ℋ ⟼ T (g) \cdot_{ih} y)$
	cnlnadjlem.4	$⊢ B = (ι w \in ℋ \| \forall v \in ℋ T (v) \cdot_{ih} y = v \cdot_{ih} w)$
	cnlnadjlem.5	$⊢ F = (y \in ℋ ⟼ B)$
Assertion	cnlnadjlem6	$⊢ F \in LinOp$

Proof

Step	Hyp	Ref	Expression
1		cnlnadjlem.1	$⊢ T \in LinOp$
2		cnlnadjlem.2	$⊢ T \in ContOp$
3		cnlnadjlem.3	$⊢ G = (g \in ℋ ⟼ T (g) \cdot_{ih} y)$
4		cnlnadjlem.4	$⊢ B = (ι w \in ℋ \| \forall v \in ℋ T (v) \cdot_{ih} y = v \cdot_{ih} w)$
5		cnlnadjlem.5	$⊢ F = (y \in ℋ ⟼ B)$
6	1 2 3 4	cnlnadjlem3	$⊢ y \in ℋ \to B \in ℋ$
7	5 6	fmpti	$⊢ F : ℋ ⟶ ℋ$
8	1	lnopfi	$⊢ T : ℋ ⟶ ℋ$
9	8	ffvelrni	$⊢ t \in ℋ \to T (t) \in ℋ$
10	9	adantl	$⊢ (((x \in ℂ \land f \in ℋ) \land z \in ℋ) \land t \in ℋ) \to T (t) \in ℋ$
11		hvmulcl	$⊢ (x \in ℂ \land f \in ℋ) \to x \cdot_{ℎ} f \in ℋ$
12	11	ad2antrr	$⊢ (((x \in ℂ \land f \in ℋ) \land z \in ℋ) \land t \in ℋ) \to x \cdot_{ℎ} f \in ℋ$
13		simplr	$⊢ (((x \in ℂ \land f \in ℋ) \land z \in ℋ) \land t \in ℋ) \to z \in ℋ$
14		his7	$⊢ (T (t) \in ℋ \land x \cdot_{ℎ} f \in ℋ \land z \in ℋ) \to T (t) \cdot_{ih} ((x \cdot_{ℎ} f) +_{ℎ} z) = (T (t) \cdot_{ih} (x \cdot_{ℎ} f)) + (T (t) \cdot_{ih} z)$
15	10 12 13 14	syl3anc	$⊢ (((x \in ℂ \land f \in ℋ) \land z \in ℋ) \land t \in ℋ) \to T (t) \cdot_{ih} ((x \cdot_{ℎ} f) +_{ℎ} z) = (T (t) \cdot_{ih} (x \cdot_{ℎ} f)) + (T (t) \cdot_{ih} z)$
16		hvaddcl	$⊢ (x \cdot_{ℎ} f \in ℋ \land z \in ℋ) \to (x \cdot_{ℎ} f) +_{ℎ} z \in ℋ$
17	11 16	sylan	$⊢ ((x \in ℂ \land f \in ℋ) \land z \in ℋ) \to (x \cdot_{ℎ} f) +_{ℎ} z \in ℋ$
18	1 2 3 4 5	cnlnadjlem5	$⊢ ((x \cdot_{ℎ} f) +_{ℎ} z \in ℋ \land t \in ℋ) \to T (t) \cdot_{ih} ((x \cdot_{ℎ} f) +_{ℎ} z) = t \cdot_{ih} F ((x \cdot_{ℎ} f) +_{ℎ} z)$
19	17 18	sylan	$⊢ (((x \in ℂ \land f \in ℋ) \land z \in ℋ) \land t \in ℋ) \to T (t) \cdot_{ih} ((x \cdot_{ℎ} f) +_{ℎ} z) = t \cdot_{ih} F ((x \cdot_{ℎ} f) +_{ℎ} z)$
20		simpll	$⊢ ((x \in ℂ \land f \in ℋ) \land t \in ℋ) \to x \in ℂ$
21	9	adantl	$⊢ ((x \in ℂ \land f \in ℋ) \land t \in ℋ) \to T (t) \in ℋ$
22		simplr	$⊢ ((x \in ℂ \land f \in ℋ) \land t \in ℋ) \to f \in ℋ$
23		his5	$⊢ (x \in ℂ \land T (t) \in ℋ \land f \in ℋ) \to T (t) \cdot_{ih} (x \cdot_{ℎ} f) = \overline{x} (T (t) \cdot_{ih} f)$
24	20 21 22 23	syl3anc	$⊢ ((x \in ℂ \land f \in ℋ) \land t \in ℋ) \to T (t) \cdot_{ih} (x \cdot_{ℎ} f) = \overline{x} (T (t) \cdot_{ih} f)$
25		simpr	$⊢ ((x \in ℂ \land f \in ℋ) \land t \in ℋ) \to t \in ℋ$
26	1 2 3 4 5	cnlnadjlem4	$⊢ f \in ℋ \to F (f) \in ℋ$
27	26	ad2antlr	$⊢ ((x \in ℂ \land f \in ℋ) \land t \in ℋ) \to F (f) \in ℋ$
28		his5	$⊢ (x \in ℂ \land t \in ℋ \land F (f) \in ℋ) \to t \cdot_{ih} (x \cdot_{ℎ} F (f)) = \overline{x} (t \cdot_{ih} F (f))$
29	20 25 27 28	syl3anc	$⊢ ((x \in ℂ \land f \in ℋ) \land t \in ℋ) \to t \cdot_{ih} (x \cdot_{ℎ} F (f)) = \overline{x} (t \cdot_{ih} F (f))$
30	1 2 3 4 5	cnlnadjlem5	$⊢ (f \in ℋ \land t \in ℋ) \to T (t) \cdot_{ih} f = t \cdot_{ih} F (f)$
31	30	adantll	$⊢ ((x \in ℂ \land f \in ℋ) \land t \in ℋ) \to T (t) \cdot_{ih} f = t \cdot_{ih} F (f)$
32	31	oveq2d	$⊢ ((x \in ℂ \land f \in ℋ) \land t \in ℋ) \to \overline{x} (T (t) \cdot_{ih} f) = \overline{x} (t \cdot_{ih} F (f))$
33	29 32	eqtr4d	$⊢ ((x \in ℂ \land f \in ℋ) \land t \in ℋ) \to t \cdot_{ih} (x \cdot_{ℎ} F (f)) = \overline{x} (T (t) \cdot_{ih} f)$
34	24 33	eqtr4d	$⊢ ((x \in ℂ \land f \in ℋ) \land t \in ℋ) \to T (t) \cdot_{ih} (x \cdot_{ℎ} f) = t \cdot_{ih} (x \cdot_{ℎ} F (f))$
35	34	adantlr	$⊢ (((x \in ℂ \land f \in ℋ) \land z \in ℋ) \land t \in ℋ) \to T (t) \cdot_{ih} (x \cdot_{ℎ} f) = t \cdot_{ih} (x \cdot_{ℎ} F (f))$
36	1 2 3 4 5	cnlnadjlem5	$⊢ (z \in ℋ \land t \in ℋ) \to T (t) \cdot_{ih} z = t \cdot_{ih} F (z)$
37	36	adantll	$⊢ (((x \in ℂ \land f \in ℋ) \land z \in ℋ) \land t \in ℋ) \to T (t) \cdot_{ih} z = t \cdot_{ih} F (z)$
38	35 37	oveq12d	$⊢ (((x \in ℂ \land f \in ℋ) \land z \in ℋ) \land t \in ℋ) \to (T (t) \cdot_{ih} (x \cdot_{ℎ} f)) + (T (t) \cdot_{ih} z) = (t \cdot_{ih} (x \cdot_{ℎ} F (f))) + (t \cdot_{ih} F (z))$
39		simpr	$⊢ (((x \in ℂ \land f \in ℋ) \land z \in ℋ) \land t \in ℋ) \to t \in ℋ$
40		hvmulcl	$⊢ (x \in ℂ \land F (f) \in ℋ) \to x \cdot_{ℎ} F (f) \in ℋ$
41	26 40	sylan2	$⊢ (x \in ℂ \land f \in ℋ) \to x \cdot_{ℎ} F (f) \in ℋ$
42	41	ad2antrr	$⊢ (((x \in ℂ \land f \in ℋ) \land z \in ℋ) \land t \in ℋ) \to x \cdot_{ℎ} F (f) \in ℋ$
43	1 2 3 4 5	cnlnadjlem4	$⊢ z \in ℋ \to F (z) \in ℋ$
44	43	ad2antlr	$⊢ (((x \in ℂ \land f \in ℋ) \land z \in ℋ) \land t \in ℋ) \to F (z) \in ℋ$
45		his7	$⊢ (t \in ℋ \land x \cdot_{ℎ} F (f) \in ℋ \land F (z) \in ℋ) \to t \cdot_{ih} ((x \cdot_{ℎ} F (f)) +_{ℎ} F (z)) = (t \cdot_{ih} (x \cdot_{ℎ} F (f))) + (t \cdot_{ih} F (z))$
46	39 42 44 45	syl3anc	$⊢ (((x \in ℂ \land f \in ℋ) \land z \in ℋ) \land t \in ℋ) \to t \cdot_{ih} ((x \cdot_{ℎ} F (f)) +_{ℎ} F (z)) = (t \cdot_{ih} (x \cdot_{ℎ} F (f))) + (t \cdot_{ih} F (z))$
47	38 46	eqtr4d	$⊢ (((x \in ℂ \land f \in ℋ) \land z \in ℋ) \land t \in ℋ) \to (T (t) \cdot_{ih} (x \cdot_{ℎ} f)) + (T (t) \cdot_{ih} z) = t \cdot_{ih} ((x \cdot_{ℎ} F (f)) +_{ℎ} F (z))$
48	15 19 47	3eqtr3d	$⊢ (((x \in ℂ \land f \in ℋ) \land z \in ℋ) \land t \in ℋ) \to t \cdot_{ih} F ((x \cdot_{ℎ} f) +_{ℎ} z) = t \cdot_{ih} ((x \cdot_{ℎ} F (f)) +_{ℎ} F (z))$
49	48	ralrimiva	$⊢ ((x \in ℂ \land f \in ℋ) \land z \in ℋ) \to \forall t \in ℋ t \cdot_{ih} F ((x \cdot_{ℎ} f) +_{ℎ} z) = t \cdot_{ih} ((x \cdot_{ℎ} F (f)) +_{ℎ} F (z))$
50	1 2 3 4 5	cnlnadjlem4	$⊢ (x \cdot_{ℎ} f) +_{ℎ} z \in ℋ \to F ((x \cdot_{ℎ} f) +_{ℎ} z) \in ℋ$
51	17 50	syl	$⊢ ((x \in ℂ \land f \in ℋ) \land z \in ℋ) \to F ((x \cdot_{ℎ} f) +_{ℎ} z) \in ℋ$
52		hvaddcl	$⊢ (x \cdot_{ℎ} F (f) \in ℋ \land F (z) \in ℋ) \to (x \cdot_{ℎ} F (f)) +_{ℎ} F (z) \in ℋ$
53	41 43 52	syl2an	$⊢ ((x \in ℂ \land f \in ℋ) \land z \in ℋ) \to (x \cdot_{ℎ} F (f)) +_{ℎ} F (z) \in ℋ$
54		hial2eq2	$⊢ (F ((x \cdot_{ℎ} f) +_{ℎ} z) \in ℋ \land (x \cdot_{ℎ} F (f)) +_{ℎ} F (z) \in ℋ) \to (\forall t \in ℋ t \cdot_{ih} F ((x \cdot_{ℎ} f) +_{ℎ} z) = t \cdot_{ih} ((x \cdot_{ℎ} F (f)) +_{ℎ} F (z)) \leftrightarrow F ((x \cdot_{ℎ} f) +_{ℎ} z) = (x \cdot_{ℎ} F (f)) +_{ℎ} F (z))$
55	51 53 54	syl2anc	$⊢ ((x \in ℂ \land f \in ℋ) \land z \in ℋ) \to (\forall t \in ℋ t \cdot_{ih} F ((x \cdot_{ℎ} f) +_{ℎ} z) = t \cdot_{ih} ((x \cdot_{ℎ} F (f)) +_{ℎ} F (z)) \leftrightarrow F ((x \cdot_{ℎ} f) +_{ℎ} z) = (x \cdot_{ℎ} F (f)) +_{ℎ} F (z))$
56	49 55	mpbid	$⊢ ((x \in ℂ \land f \in ℋ) \land z \in ℋ) \to F ((x \cdot_{ℎ} f) +_{ℎ} z) = (x \cdot_{ℎ} F (f)) +_{ℎ} F (z)$
57	56	ralrimiva	$⊢ (x \in ℂ \land f \in ℋ) \to \forall z \in ℋ F ((x \cdot_{ℎ} f) +_{ℎ} z) = (x \cdot_{ℎ} F (f)) +_{ℎ} F (z)$
58	57	rgen2	$⊢ \forall x \in ℂ \forall f \in ℋ \forall z \in ℋ F ((x \cdot_{ℎ} f) +_{ℎ} z) = (x \cdot_{ℎ} F (f)) +_{ℎ} F (z)$
59		ellnop	$⊢ F \in LinOp \leftrightarrow (F : ℋ ⟶ ℋ \land \forall x \in ℂ \forall f \in ℋ \forall z \in ℋ F ((x \cdot_{ℎ} f) +_{ℎ} z) = (x \cdot_{ℎ} F (f)) +_{ℎ} F (z))$
60	7 58 59	mpbir2an	$⊢ F \in LinOp$

Metamath Proof Explorer

Theorem cnlnadjlem6

Proof