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 
|- T e. LinOp
cnlnadjlem.2 
|- T e. ContOp
cnlnadjlem.3 
|- G = ( g e. ~H |-> ( ( T ` g ) .ih y ) )
cnlnadjlem.4 
|- B = ( iota_ w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) )
cnlnadjlem.5 
|- F = ( y e. ~H |-> B )
Assertion cnlnadjlem6 
|- F e. LinOp

Proof

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 ffvelcdmi 
 |-  ( 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