Step |
Hyp |
Ref |
Expression |
1 |
|
cnlnadjlem.1 |
|- T e. LinOp |
2 |
|
cnlnadjlem.2 |
|- T e. ContOp |
3 |
|
cnlnadjlem.3 |
|- G = ( g e. ~H |-> ( ( T ` g ) .ih y ) ) |
4 |
|
cnlnadjlem.4 |
|- B = ( iota_ w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) ) |
5 |
|
cnlnadjlem.5 |
|- F = ( y e. ~H |-> B ) |
6 |
1 2 3 4
|
cnlnadjlem3 |
|- ( y e. ~H -> B e. ~H ) |
7 |
5 6
|
fmpti |
|- F : ~H --> ~H |
8 |
1
|
lnopfi |
|- T : ~H --> ~H |
9 |
8
|
ffvelrni |
|- ( t e. ~H -> ( T ` t ) e. ~H ) |
10 |
9
|
adantl |
|- ( ( ( ( x e. CC /\ f e. ~H ) /\ z e. ~H ) /\ t e. ~H ) -> ( T ` t ) e. ~H ) |
11 |
|
hvmulcl |
|- ( ( x e. CC /\ f e. ~H ) -> ( x .h f ) e. ~H ) |
12 |
11
|
ad2antrr |
|- ( ( ( ( x e. CC /\ f e. ~H ) /\ z e. ~H ) /\ t e. ~H ) -> ( x .h f ) e. ~H ) |
13 |
|
simplr |
|- ( ( ( ( x e. CC /\ f e. ~H ) /\ z e. ~H ) /\ t e. ~H ) -> z e. ~H ) |
14 |
|
his7 |
|- ( ( ( T ` t ) e. ~H /\ ( x .h f ) e. ~H /\ z e. ~H ) -> ( ( T ` t ) .ih ( ( x .h f ) +h z ) ) = ( ( ( T ` t ) .ih ( x .h f ) ) + ( ( T ` t ) .ih z ) ) ) |
15 |
10 12 13 14
|
syl3anc |
|- ( ( ( ( x e. CC /\ f e. ~H ) /\ z e. ~H ) /\ t e. ~H ) -> ( ( T ` t ) .ih ( ( x .h f ) +h z ) ) = ( ( ( T ` t ) .ih ( x .h f ) ) + ( ( T ` t ) .ih z ) ) ) |
16 |
|
hvaddcl |
|- ( ( ( x .h f ) e. ~H /\ z e. ~H ) -> ( ( x .h f ) +h z ) e. ~H ) |
17 |
11 16
|
sylan |
|- ( ( ( x e. CC /\ f e. ~H ) /\ z e. ~H ) -> ( ( x .h f ) +h z ) e. ~H ) |
18 |
1 2 3 4 5
|
cnlnadjlem5 |
|- ( ( ( ( x .h f ) +h z ) e. ~H /\ t e. ~H ) -> ( ( T ` t ) .ih ( ( x .h f ) +h z ) ) = ( t .ih ( F ` ( ( x .h f ) +h z ) ) ) ) |
19 |
17 18
|
sylan |
|- ( ( ( ( x e. CC /\ f e. ~H ) /\ z e. ~H ) /\ t e. ~H ) -> ( ( T ` t ) .ih ( ( x .h f ) +h z ) ) = ( t .ih ( F ` ( ( x .h f ) +h z ) ) ) ) |
20 |
|
simpll |
|- ( ( ( x e. CC /\ f e. ~H ) /\ t e. ~H ) -> x e. CC ) |
21 |
9
|
adantl |
|- ( ( ( x e. CC /\ f e. ~H ) /\ t e. ~H ) -> ( T ` t ) e. ~H ) |
22 |
|
simplr |
|- ( ( ( x e. CC /\ f e. ~H ) /\ t e. ~H ) -> f e. ~H ) |
23 |
|
his5 |
|- ( ( x e. CC /\ ( T ` t ) e. ~H /\ f e. ~H ) -> ( ( T ` t ) .ih ( x .h f ) ) = ( ( * ` x ) x. ( ( T ` t ) .ih f ) ) ) |
24 |
20 21 22 23
|
syl3anc |
|- ( ( ( x e. CC /\ f e. ~H ) /\ t e. ~H ) -> ( ( T ` t ) .ih ( x .h f ) ) = ( ( * ` x ) x. ( ( T ` t ) .ih f ) ) ) |
25 |
|
simpr |
|- ( ( ( x e. CC /\ f e. ~H ) /\ t e. ~H ) -> t e. ~H ) |
26 |
1 2 3 4 5
|
cnlnadjlem4 |
|- ( f e. ~H -> ( F ` f ) e. ~H ) |
27 |
26
|
ad2antlr |
|- ( ( ( x e. CC /\ f e. ~H ) /\ t e. ~H ) -> ( F ` f ) e. ~H ) |
28 |
|
his5 |
|- ( ( x e. CC /\ t e. ~H /\ ( F ` f ) e. ~H ) -> ( t .ih ( x .h ( F ` f ) ) ) = ( ( * ` x ) x. ( t .ih ( F ` f ) ) ) ) |
29 |
20 25 27 28
|
syl3anc |
|- ( ( ( x e. CC /\ f e. ~H ) /\ t e. ~H ) -> ( t .ih ( x .h ( F ` f ) ) ) = ( ( * ` x ) x. ( t .ih ( F ` f ) ) ) ) |
30 |
1 2 3 4 5
|
cnlnadjlem5 |
|- ( ( f e. ~H /\ t e. ~H ) -> ( ( T ` t ) .ih f ) = ( t .ih ( F ` f ) ) ) |
31 |
30
|
adantll |
|- ( ( ( x e. CC /\ f e. ~H ) /\ t e. ~H ) -> ( ( T ` t ) .ih f ) = ( t .ih ( F ` f ) ) ) |
32 |
31
|
oveq2d |
|- ( ( ( x e. CC /\ f e. ~H ) /\ t e. ~H ) -> ( ( * ` x ) x. ( ( T ` t ) .ih f ) ) = ( ( * ` x ) x. ( t .ih ( F ` f ) ) ) ) |
33 |
29 32
|
eqtr4d |
|- ( ( ( x e. CC /\ f e. ~H ) /\ t e. ~H ) -> ( t .ih ( x .h ( F ` f ) ) ) = ( ( * ` x ) x. ( ( T ` t ) .ih f ) ) ) |
34 |
24 33
|
eqtr4d |
|- ( ( ( x e. CC /\ f e. ~H ) /\ t e. ~H ) -> ( ( T ` t ) .ih ( x .h f ) ) = ( t .ih ( x .h ( F ` f ) ) ) ) |
35 |
34
|
adantlr |
|- ( ( ( ( x e. CC /\ f e. ~H ) /\ z e. ~H ) /\ t e. ~H ) -> ( ( T ` t ) .ih ( x .h f ) ) = ( t .ih ( x .h ( F ` f ) ) ) ) |
36 |
1 2 3 4 5
|
cnlnadjlem5 |
|- ( ( z e. ~H /\ t e. ~H ) -> ( ( T ` t ) .ih z ) = ( t .ih ( F ` z ) ) ) |
37 |
36
|
adantll |
|- ( ( ( ( x e. CC /\ f e. ~H ) /\ z e. ~H ) /\ t e. ~H ) -> ( ( T ` t ) .ih z ) = ( t .ih ( F ` z ) ) ) |
38 |
35 37
|
oveq12d |
|- ( ( ( ( x e. CC /\ f e. ~H ) /\ z e. ~H ) /\ t e. ~H ) -> ( ( ( T ` t ) .ih ( x .h f ) ) + ( ( T ` t ) .ih z ) ) = ( ( t .ih ( x .h ( F ` f ) ) ) + ( t .ih ( F ` z ) ) ) ) |
39 |
|
simpr |
|- ( ( ( ( x e. CC /\ f e. ~H ) /\ z e. ~H ) /\ t e. ~H ) -> t e. ~H ) |
40 |
|
hvmulcl |
|- ( ( x e. CC /\ ( F ` f ) e. ~H ) -> ( x .h ( F ` f ) ) e. ~H ) |
41 |
26 40
|
sylan2 |
|- ( ( x e. CC /\ f e. ~H ) -> ( x .h ( F ` f ) ) e. ~H ) |
42 |
41
|
ad2antrr |
|- ( ( ( ( x e. CC /\ f e. ~H ) /\ z e. ~H ) /\ t e. ~H ) -> ( x .h ( F ` f ) ) e. ~H ) |
43 |
1 2 3 4 5
|
cnlnadjlem4 |
|- ( z e. ~H -> ( F ` z ) e. ~H ) |
44 |
43
|
ad2antlr |
|- ( ( ( ( x e. CC /\ f e. ~H ) /\ z e. ~H ) /\ t e. ~H ) -> ( F ` z ) e. ~H ) |
45 |
|
his7 |
|- ( ( t e. ~H /\ ( x .h ( F ` f ) ) e. ~H /\ ( F ` z ) e. ~H ) -> ( t .ih ( ( x .h ( F ` f ) ) +h ( F ` z ) ) ) = ( ( t .ih ( x .h ( F ` f ) ) ) + ( t .ih ( F ` z ) ) ) ) |
46 |
39 42 44 45
|
syl3anc |
|- ( ( ( ( x e. CC /\ f e. ~H ) /\ z e. ~H ) /\ t e. ~H ) -> ( t .ih ( ( x .h ( F ` f ) ) +h ( F ` z ) ) ) = ( ( t .ih ( x .h ( F ` f ) ) ) + ( t .ih ( F ` z ) ) ) ) |
47 |
38 46
|
eqtr4d |
|- ( ( ( ( x e. CC /\ f e. ~H ) /\ z e. ~H ) /\ t e. ~H ) -> ( ( ( T ` t ) .ih ( x .h f ) ) + ( ( T ` t ) .ih z ) ) = ( t .ih ( ( x .h ( F ` f ) ) +h ( F ` z ) ) ) ) |
48 |
15 19 47
|
3eqtr3d |
|- ( ( ( ( x e. CC /\ f e. ~H ) /\ z e. ~H ) /\ t e. ~H ) -> ( t .ih ( F ` ( ( x .h f ) +h z ) ) ) = ( t .ih ( ( x .h ( F ` f ) ) +h ( F ` z ) ) ) ) |
49 |
48
|
ralrimiva |
|- ( ( ( x e. CC /\ f e. ~H ) /\ z e. ~H ) -> A. t e. ~H ( t .ih ( F ` ( ( x .h f ) +h z ) ) ) = ( t .ih ( ( x .h ( F ` f ) ) +h ( F ` z ) ) ) ) |
50 |
1 2 3 4 5
|
cnlnadjlem4 |
|- ( ( ( x .h f ) +h z ) e. ~H -> ( F ` ( ( x .h f ) +h z ) ) e. ~H ) |
51 |
17 50
|
syl |
|- ( ( ( x e. CC /\ f e. ~H ) /\ z e. ~H ) -> ( F ` ( ( x .h f ) +h z ) ) e. ~H ) |
52 |
|
hvaddcl |
|- ( ( ( x .h ( F ` f ) ) e. ~H /\ ( F ` z ) e. ~H ) -> ( ( x .h ( F ` f ) ) +h ( F ` z ) ) e. ~H ) |
53 |
41 43 52
|
syl2an |
|- ( ( ( x e. CC /\ f e. ~H ) /\ z e. ~H ) -> ( ( x .h ( F ` f ) ) +h ( F ` z ) ) e. ~H ) |
54 |
|
hial2eq2 |
|- ( ( ( F ` ( ( x .h f ) +h z ) ) e. ~H /\ ( ( x .h ( F ` f ) ) +h ( F ` z ) ) e. ~H ) -> ( A. t e. ~H ( t .ih ( F ` ( ( x .h f ) +h z ) ) ) = ( t .ih ( ( x .h ( F ` f ) ) +h ( F ` z ) ) ) <-> ( F ` ( ( x .h f ) +h z ) ) = ( ( x .h ( F ` f ) ) +h ( F ` z ) ) ) ) |
55 |
51 53 54
|
syl2anc |
|- ( ( ( x e. CC /\ f e. ~H ) /\ z e. ~H ) -> ( A. t e. ~H ( t .ih ( F ` ( ( x .h f ) +h z ) ) ) = ( t .ih ( ( x .h ( F ` f ) ) +h ( F ` z ) ) ) <-> ( F ` ( ( x .h f ) +h z ) ) = ( ( x .h ( F ` f ) ) +h ( F ` z ) ) ) ) |
56 |
49 55
|
mpbid |
|- ( ( ( x e. CC /\ f e. ~H ) /\ z e. ~H ) -> ( F ` ( ( x .h f ) +h z ) ) = ( ( x .h ( F ` f ) ) +h ( F ` z ) ) ) |
57 |
56
|
ralrimiva |
|- ( ( x e. CC /\ f e. ~H ) -> A. z e. ~H ( F ` ( ( x .h f ) +h z ) ) = ( ( x .h ( F ` f ) ) +h ( F ` z ) ) ) |
58 |
57
|
rgen2 |
|- A. x e. CC A. f e. ~H A. z e. ~H ( F ` ( ( x .h f ) +h z ) ) = ( ( x .h ( F ` f ) ) +h ( F ` z ) ) |
59 |
|
ellnop |
|- ( F e. LinOp <-> ( F : ~H --> ~H /\ A. x e. CC A. f e. ~H A. z e. ~H ( F ` ( ( x .h f ) +h z ) ) = ( ( x .h ( F ` f ) ) +h ( F ` z ) ) ) ) |
60 |
7 58 59
|
mpbir2an |
|- F e. LinOp |