Metamath Proof Explorer

Theorem cnlnadjlem6

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

Ref Expression
Hypotheses cnlnadjlem.1 ⊢ 𝑇 ∈ LinOp
cnlnadjlem.2 ⊢ 𝑇 ∈ ContOp
cnlnadjlem.3 ⊢ 𝐺 = ( 𝑔 ∈ ℋ ↦ ( ( 𝑇 ‘ 𝑔 ) ·ih 𝑦 ) )
cnlnadjlem.4 ⊢ 𝐵 = ( ℩ 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑦 ) = ( 𝑣 ·ih 𝑤 ) )
cnlnadjlem.5 ⊢ 𝐹 = ( 𝑦 ∈ ℋ ↦ 𝐵 )
Assertion cnlnadjlem6 𝐹 ∈ LinOp

Proof

Step Hyp Ref Expression
1 cnlnadjlem.1 ⊢ 𝑇 ∈ LinOp
2 cnlnadjlem.2 ⊢ 𝑇 ∈ ContOp
3 cnlnadjlem.3 ⊢ 𝐺 = ( 𝑔 ∈ ℋ ↦ ( ( 𝑇 ‘ 𝑔 ) ·ih 𝑦 ) )
4 cnlnadjlem.4 ⊢ 𝐵 = ( ℩ 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑦 ) = ( 𝑣 ·ih 𝑤 ) )
5 cnlnadjlem.5 ⊢ 𝐹 = ( 𝑦 ∈ ℋ ↦ 𝐵 )
6 1 2 3 4 cnlnadjlem3 ⊢ ( 𝑦 ∈ ℋ → 𝐵 ∈ ℋ )
7 5 6 fmpti ⊢ 𝐹 : ℋ ⟶ ℋ
8 1 lnopfi ⊢ 𝑇 : ℋ ⟶ ℋ
9 8 ffvelcdmi ⊢ ( 𝑡 ∈ ℋ → ( 𝑇 ‘ 𝑡 ) ∈ ℋ )
10 9 adantl ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ∧ 𝑡 ∈ ℋ ) → ( 𝑇 ‘ 𝑡 ) ∈ ℋ )
11 hvmulcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ ) → ( 𝑥 ·ℎ 𝑓 ) ∈ ℋ )
12 11 ad2antrr ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ∧ 𝑡 ∈ ℋ ) → ( 𝑥 ·ℎ 𝑓 ) ∈ ℋ )
13 simplr ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ∧ 𝑡 ∈ ℋ ) → 𝑧 ∈ ℋ )
14 his7 ⊢ ( ( ( 𝑇 ‘ 𝑡 ) ∈ ℋ ∧ ( 𝑥 ·ℎ 𝑓 ) ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑡 ) ·ih ( ( 𝑥 ·ℎ 𝑓 ) +ℎ 𝑧 ) ) = ( ( ( 𝑇 ‘ 𝑡 ) ·ih ( 𝑥 ·ℎ 𝑓 ) ) + ( ( 𝑇 ‘ 𝑡 ) ·ih 𝑧 ) ) )
15 10 12 13 14 syl3anc ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ∧ 𝑡 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑡 ) ·ih ( ( 𝑥 ·ℎ 𝑓 ) +ℎ 𝑧 ) ) = ( ( ( 𝑇 ‘ 𝑡 ) ·ih ( 𝑥 ·ℎ 𝑓 ) ) + ( ( 𝑇 ‘ 𝑡 ) ·ih 𝑧 ) ) )
16 hvaddcl ⊢ ( ( ( 𝑥 ·ℎ 𝑓 ) ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 ·ℎ 𝑓 ) +ℎ 𝑧 ) ∈ ℋ )
17 11 16 sylan ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 ·ℎ 𝑓 ) +ℎ 𝑧 ) ∈ ℋ )
18 1 2 3 4 5 cnlnadjlem5 ⊢ ( ( ( ( 𝑥 ·ℎ 𝑓 ) +ℎ 𝑧 ) ∈ ℋ ∧ 𝑡 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑡 ) ·ih ( ( 𝑥 ·ℎ 𝑓 ) +ℎ 𝑧 ) ) = ( 𝑡 ·ih ( 𝐹 ‘ ( ( 𝑥 ·ℎ 𝑓 ) +ℎ 𝑧 ) ) ) )
19 17 18 sylan ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ∧ 𝑡 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑡 ) ·ih ( ( 𝑥 ·ℎ 𝑓 ) +ℎ 𝑧 ) ) = ( 𝑡 ·ih ( 𝐹 ‘ ( ( 𝑥 ·ℎ 𝑓 ) +ℎ 𝑧 ) ) ) )
20 simpll ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ ) ∧ 𝑡 ∈ ℋ ) → 𝑥 ∈ ℂ )
21 9 adantl ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ ) ∧ 𝑡 ∈ ℋ ) → ( 𝑇 ‘ 𝑡 ) ∈ ℋ )
22 simplr ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ ) ∧ 𝑡 ∈ ℋ ) → 𝑓 ∈ ℋ )
23 his5 ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑇 ‘ 𝑡 ) ∈ ℋ ∧ 𝑓 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑡 ) ·ih ( 𝑥 ·ℎ 𝑓 ) ) = ( ( ∗ ‘ 𝑥 ) · ( ( 𝑇 ‘ 𝑡 ) ·ih 𝑓 ) ) )
24 20 21 22 23 syl3anc ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ ) ∧ 𝑡 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑡 ) ·ih ( 𝑥 ·ℎ 𝑓 ) ) = ( ( ∗ ‘ 𝑥 ) · ( ( 𝑇 ‘ 𝑡 ) ·ih 𝑓 ) ) )
25 simpr ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ ) ∧ 𝑡 ∈ ℋ ) → 𝑡 ∈ ℋ )
26 1 2 3 4 5 cnlnadjlem4 ⊢ ( 𝑓 ∈ ℋ → ( 𝐹 ‘ 𝑓 ) ∈ ℋ )
27 26 ad2antlr ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ ) ∧ 𝑡 ∈ ℋ ) → ( 𝐹 ‘ 𝑓 ) ∈ ℋ )
28 his5 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑡 ∈ ℋ ∧ ( 𝐹 ‘ 𝑓 ) ∈ ℋ ) → ( 𝑡 ·ih ( 𝑥 ·ℎ ( 𝐹 ‘ 𝑓 ) ) ) = ( ( ∗ ‘ 𝑥 ) · ( 𝑡 ·ih ( 𝐹 ‘ 𝑓 ) ) ) )
29 20 25 27 28 syl3anc ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ ) ∧ 𝑡 ∈ ℋ ) → ( 𝑡 ·ih ( 𝑥 ·ℎ ( 𝐹 ‘ 𝑓 ) ) ) = ( ( ∗ ‘ 𝑥 ) · ( 𝑡 ·ih ( 𝐹 ‘ 𝑓 ) ) ) )
30 1 2 3 4 5 cnlnadjlem5 ⊢ ( ( 𝑓 ∈ ℋ ∧ 𝑡 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑡 ) ·ih 𝑓 ) = ( 𝑡 ·ih ( 𝐹 ‘ 𝑓 ) ) )
31 30 adantll ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ ) ∧ 𝑡 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑡 ) ·ih 𝑓 ) = ( 𝑡 ·ih ( 𝐹 ‘ 𝑓 ) ) )
32 31 oveq2d ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ ) ∧ 𝑡 ∈ ℋ ) → ( ( ∗ ‘ 𝑥 ) · ( ( 𝑇 ‘ 𝑡 ) ·ih 𝑓 ) ) = ( ( ∗ ‘ 𝑥 ) · ( 𝑡 ·ih ( 𝐹 ‘ 𝑓 ) ) ) )
33 29 32 eqtr4d ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ ) ∧ 𝑡 ∈ ℋ ) → ( 𝑡 ·ih ( 𝑥 ·ℎ ( 𝐹 ‘ 𝑓 ) ) ) = ( ( ∗ ‘ 𝑥 ) · ( ( 𝑇 ‘ 𝑡 ) ·ih 𝑓 ) ) )
34 24 33 eqtr4d ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ ) ∧ 𝑡 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑡 ) ·ih ( 𝑥 ·ℎ 𝑓 ) ) = ( 𝑡 ·ih ( 𝑥 ·ℎ ( 𝐹 ‘ 𝑓 ) ) ) )
35 34 adantlr ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ∧ 𝑡 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑡 ) ·ih ( 𝑥 ·ℎ 𝑓 ) ) = ( 𝑡 ·ih ( 𝑥 ·ℎ ( 𝐹 ‘ 𝑓 ) ) ) )
36 1 2 3 4 5 cnlnadjlem5 ⊢ ( ( 𝑧 ∈ ℋ ∧ 𝑡 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑡 ) ·ih 𝑧 ) = ( 𝑡 ·ih ( 𝐹 ‘ 𝑧 ) ) )
37 36 adantll ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ∧ 𝑡 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑡 ) ·ih 𝑧 ) = ( 𝑡 ·ih ( 𝐹 ‘ 𝑧 ) ) )
38 35 37 oveq12d ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ∧ 𝑡 ∈ ℋ ) → ( ( ( 𝑇 ‘ 𝑡 ) ·ih ( 𝑥 ·ℎ 𝑓 ) ) + ( ( 𝑇 ‘ 𝑡 ) ·ih 𝑧 ) ) = ( ( 𝑡 ·ih ( 𝑥 ·ℎ ( 𝐹 ‘ 𝑓 ) ) ) + ( 𝑡 ·ih ( 𝐹 ‘ 𝑧 ) ) ) )
39 simpr ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ∧ 𝑡 ∈ ℋ ) → 𝑡 ∈ ℋ )
40 hvmulcl ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝐹 ‘ 𝑓 ) ∈ ℋ ) → ( 𝑥 ·ℎ ( 𝐹 ‘ 𝑓 ) ) ∈ ℋ )
41 26 40 sylan2 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ ) → ( 𝑥 ·ℎ ( 𝐹 ‘ 𝑓 ) ) ∈ ℋ )
42 41 ad2antrr ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ∧ 𝑡 ∈ ℋ ) → ( 𝑥 ·ℎ ( 𝐹 ‘ 𝑓 ) ) ∈ ℋ )
43 1 2 3 4 5 cnlnadjlem4 ⊢ ( 𝑧 ∈ ℋ → ( 𝐹 ‘ 𝑧 ) ∈ ℋ )
44 43 ad2antlr ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ∧ 𝑡 ∈ ℋ ) → ( 𝐹 ‘ 𝑧 ) ∈ ℋ )
45 his7 ⊢ ( ( 𝑡 ∈ ℋ ∧ ( 𝑥 ·ℎ ( 𝐹 ‘ 𝑓 ) ) ∈ ℋ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℋ ) → ( 𝑡 ·ih ( ( 𝑥 ·ℎ ( 𝐹 ‘ 𝑓 ) ) +ℎ ( 𝐹 ‘ 𝑧 ) ) ) = ( ( 𝑡 ·ih ( 𝑥 ·ℎ ( 𝐹 ‘ 𝑓 ) ) ) + ( 𝑡 ·ih ( 𝐹 ‘ 𝑧 ) ) ) )
46 39 42 44 45 syl3anc ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ∧ 𝑡 ∈ ℋ ) → ( 𝑡 ·ih ( ( 𝑥 ·ℎ ( 𝐹 ‘ 𝑓 ) ) +ℎ ( 𝐹 ‘ 𝑧 ) ) ) = ( ( 𝑡 ·ih ( 𝑥 ·ℎ ( 𝐹 ‘ 𝑓 ) ) ) + ( 𝑡 ·ih ( 𝐹 ‘ 𝑧 ) ) ) )
47 38 46 eqtr4d ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ∧ 𝑡 ∈ ℋ ) → ( ( ( 𝑇 ‘ 𝑡 ) ·ih ( 𝑥 ·ℎ 𝑓 ) ) + ( ( 𝑇 ‘ 𝑡 ) ·ih 𝑧 ) ) = ( 𝑡 ·ih ( ( 𝑥 ·ℎ ( 𝐹 ‘ 𝑓 ) ) +ℎ ( 𝐹 ‘ 𝑧 ) ) ) )
48 15 19 47 3eqtr3d ⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ∧ 𝑡 ∈ ℋ ) → ( 𝑡 ·ih ( 𝐹 ‘ ( ( 𝑥 ·ℎ 𝑓 ) +ℎ 𝑧 ) ) ) = ( 𝑡 ·ih ( ( 𝑥 ·ℎ ( 𝐹 ‘ 𝑓 ) ) +ℎ ( 𝐹 ‘ 𝑧 ) ) ) )
49 48 ralrimiva ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ∀ 𝑡 ∈ ℋ ( 𝑡 ·ih ( 𝐹 ‘ ( ( 𝑥 ·ℎ 𝑓 ) +ℎ 𝑧 ) ) ) = ( 𝑡 ·ih ( ( 𝑥 ·ℎ ( 𝐹 ‘ 𝑓 ) ) +ℎ ( 𝐹 ‘ 𝑧 ) ) ) )
50 1 2 3 4 5 cnlnadjlem4 ⊢ ( ( ( 𝑥 ·ℎ 𝑓 ) +ℎ 𝑧 ) ∈ ℋ → ( 𝐹 ‘ ( ( 𝑥 ·ℎ 𝑓 ) +ℎ 𝑧 ) ) ∈ ℋ )
51 17 50 syl ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( 𝐹 ‘ ( ( 𝑥 ·ℎ 𝑓 ) +ℎ 𝑧 ) ) ∈ ℋ )
52 hvaddcl ⊢ ( ( ( 𝑥 ·ℎ ( 𝐹 ‘ 𝑓 ) ) ∈ ℋ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℋ ) → ( ( 𝑥 ·ℎ ( 𝐹 ‘ 𝑓 ) ) +ℎ ( 𝐹 ‘ 𝑧 ) ) ∈ ℋ )
53 41 43 52 syl2an ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 ·ℎ ( 𝐹 ‘ 𝑓 ) ) +ℎ ( 𝐹 ‘ 𝑧 ) ) ∈ ℋ )
54 hial2eq2 ⊢ ( ( ( 𝐹 ‘ ( ( 𝑥 ·ℎ 𝑓 ) +ℎ 𝑧 ) ) ∈ ℋ ∧ ( ( 𝑥 ·ℎ ( 𝐹 ‘ 𝑓 ) ) +ℎ ( 𝐹 ‘ 𝑧 ) ) ∈ ℋ ) → ( ∀ 𝑡 ∈ ℋ ( 𝑡 ·ih ( 𝐹 ‘ ( ( 𝑥 ·ℎ 𝑓 ) +ℎ 𝑧 ) ) ) = ( 𝑡 ·ih ( ( 𝑥 ·ℎ ( 𝐹 ‘ 𝑓 ) ) +ℎ ( 𝐹 ‘ 𝑧 ) ) ) ↔ ( 𝐹 ‘ ( ( 𝑥 ·ℎ 𝑓 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝐹 ‘ 𝑓 ) ) +ℎ ( 𝐹 ‘ 𝑧 ) ) ) )
55 51 53 54 syl2anc ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ∀ 𝑡 ∈ ℋ ( 𝑡 ·ih ( 𝐹 ‘ ( ( 𝑥 ·ℎ 𝑓 ) +ℎ 𝑧 ) ) ) = ( 𝑡 ·ih ( ( 𝑥 ·ℎ ( 𝐹 ‘ 𝑓 ) ) +ℎ ( 𝐹 ‘ 𝑧 ) ) ) ↔ ( 𝐹 ‘ ( ( 𝑥 ·ℎ 𝑓 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝐹 ‘ 𝑓 ) ) +ℎ ( 𝐹 ‘ 𝑧 ) ) ) )
56 49 55 mpbid ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( 𝐹 ‘ ( ( 𝑥 ·ℎ 𝑓 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝐹 ‘ 𝑓 ) ) +ℎ ( 𝐹 ‘ 𝑧 ) ) )
57 56 ralrimiva ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑓 ∈ ℋ ) → ∀ 𝑧 ∈ ℋ ( 𝐹 ‘ ( ( 𝑥 ·ℎ 𝑓 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝐹 ‘ 𝑓 ) ) +ℎ ( 𝐹 ‘ 𝑧 ) ) )
58 57 rgen2 ⊢ ∀ 𝑥 ∈ ℂ ∀ 𝑓 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝐹 ‘ ( ( 𝑥 ·ℎ 𝑓 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝐹 ‘ 𝑓 ) ) +ℎ ( 𝐹 ‘ 𝑧 ) )
59 ellnop ⊢ ( 𝐹 ∈ LinOp ↔ ( 𝐹 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑓 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝐹 ‘ ( ( 𝑥 ·ℎ 𝑓 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝐹 ‘ 𝑓 ) ) +ℎ ( 𝐹 ‘ 𝑧 ) ) ) )
60 7 58 59 mpbir2an ⊢ 𝐹 ∈ LinOp