Metamath Proof Explorer

Theorem imaelshi

Description: The image of a subspace under a linear operator is a subspace. (Contributed by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses rnelsh.1 
|- T e. LinOp
imaelsh.2 
|- A e. SH
Assertion imaelshi 
|- ( T " A ) e. SH

Proof

Step Hyp Ref Expression
1 rnelsh.1 
 |-  T e. LinOp
2 imaelsh.2 
 |-  A e. SH
3 imassrn 
 |-  ( T " A ) C_ ran T
4 1 lnopfi 
 |-  T : ~H --> ~H
5 frn 
 |-  ( T : ~H --> ~H -> ran T C_ ~H )
6 4 5 ax-mp 
 |-  ran T C_ ~H
7 3 6 sstri 
 |-  ( T " A ) C_ ~H
8 1 lnop0i 
 |-  ( T ` 0h ) = 0h
9 sh0 
 |-  ( A e. SH -> 0h e. A )
10 2 9 ax-mp 
 |-  0h e. A
11 ffun 
 |-  ( T : ~H --> ~H -> Fun T )
12 4 11 ax-mp 
 |-  Fun T
13 2 shssii 
 |-  A C_ ~H
14 4 fdmi 
 |-  dom T = ~H
15 13 14 sseqtrri 
 |-  A C_ dom T
16 funfvima2 
 |-  ( ( Fun T /\ A C_ dom T ) -> ( 0h e. A -> ( T ` 0h ) e. ( T " A ) ) )
17 12 15 16 mp2an 
 |-  ( 0h e. A -> ( T ` 0h ) e. ( T " A ) )
18 10 17 ax-mp 
 |-  ( T ` 0h ) e. ( T " A )
19 8 18 eqeltrri 
 |-  0h e. ( T " A )
20 7 19 pm3.2i 
 |-  ( ( T " A ) C_ ~H /\ 0h e. ( T " A ) )
21 ffn 
 |-  ( T : ~H --> ~H -> T Fn ~H )
22 4 21 ax-mp 
 |-  T Fn ~H
23 oveq1 
 |-  ( u = ( T ` x ) -> ( u +h v ) = ( ( T ` x ) +h v ) )
24 23 eleq1d 
 |-  ( u = ( T ` x ) -> ( ( u +h v ) e. ( T " A ) <-> ( ( T ` x ) +h v ) e. ( T " A ) ) )
25 24 ralbidv 
 |-  ( u = ( T ` x ) -> ( A. v e. ( T " A ) ( u +h v ) e. ( T " A ) <-> A. v e. ( T " A ) ( ( T ` x ) +h v ) e. ( T " A ) ) )
26 25 ralima 
 |-  ( ( T Fn ~H /\ A C_ ~H ) -> ( A. u e. ( T " A ) A. v e. ( T " A ) ( u +h v ) e. ( T " A ) <-> A. x e. A A. v e. ( T " A ) ( ( T ` x ) +h v ) e. ( T " A ) ) )
27 22 13 26 mp2an 
 |-  ( A. u e. ( T " A ) A. v e. ( T " A ) ( u +h v ) e. ( T " A ) <-> A. x e. A A. v e. ( T " A ) ( ( T ` x ) +h v ) e. ( T " A ) )
28 2 sheli 
 |-  ( x e. A -> x e. ~H )
29 2 sheli 
 |-  ( y e. A -> y e. ~H )
30 1 lnopaddi 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( T ` ( x +h y ) ) = ( ( T ` x ) +h ( T ` y ) ) )
31 28 29 30 syl2an 
 |-  ( ( x e. A /\ y e. A ) -> ( T ` ( x +h y ) ) = ( ( T ` x ) +h ( T ` y ) ) )
32 shaddcl 
 |-  ( ( A e. SH /\ x e. A /\ y e. A ) -> ( x +h y ) e. A )
33 2 32 mp3an1 
 |-  ( ( x e. A /\ y e. A ) -> ( x +h y ) e. A )
34 funfvima2 
 |-  ( ( Fun T /\ A C_ dom T ) -> ( ( x +h y ) e. A -> ( T ` ( x +h y ) ) e. ( T " A ) ) )
35 12 15 34 mp2an 
 |-  ( ( x +h y ) e. A -> ( T ` ( x +h y ) ) e. ( T " A ) )
36 33 35 syl 
 |-  ( ( x e. A /\ y e. A ) -> ( T ` ( x +h y ) ) e. ( T " A ) )
37 31 36 eqeltrrd 
 |-  ( ( x e. A /\ y e. A ) -> ( ( T ` x ) +h ( T ` y ) ) e. ( T " A ) )
38 37 ralrimiva 
 |-  ( x e. A -> A. y e. A ( ( T ` x ) +h ( T ` y ) ) e. ( T " A ) )
39 oveq2 
 |-  ( v = ( T ` y ) -> ( ( T ` x ) +h v ) = ( ( T ` x ) +h ( T ` y ) ) )
40 39 eleq1d 
 |-  ( v = ( T ` y ) -> ( ( ( T ` x ) +h v ) e. ( T " A ) <-> ( ( T ` x ) +h ( T ` y ) ) e. ( T " A ) ) )
41 40 ralima 
 |-  ( ( T Fn ~H /\ A C_ ~H ) -> ( A. v e. ( T " A ) ( ( T ` x ) +h v ) e. ( T " A ) <-> A. y e. A ( ( T ` x ) +h ( T ` y ) ) e. ( T " A ) ) )
42 22 13 41 mp2an 
 |-  ( A. v e. ( T " A ) ( ( T ` x ) +h v ) e. ( T " A ) <-> A. y e. A ( ( T ` x ) +h ( T ` y ) ) e. ( T " A ) )
43 38 42 sylibr 
 |-  ( x e. A -> A. v e. ( T " A ) ( ( T ` x ) +h v ) e. ( T " A ) )
44 27 43 mprgbir 
 |-  A. u e. ( T " A ) A. v e. ( T " A ) ( u +h v ) e. ( T " A )
45 1 lnopmuli 
 |-  ( ( u e. CC /\ y e. ~H ) -> ( T ` ( u .h y ) ) = ( u .h ( T ` y ) ) )
46 29 45 sylan2 
 |-  ( ( u e. CC /\ y e. A ) -> ( T ` ( u .h y ) ) = ( u .h ( T ` y ) ) )
47 shmulcl 
 |-  ( ( A e. SH /\ u e. CC /\ y e. A ) -> ( u .h y ) e. A )
48 2 47 mp3an1 
 |-  ( ( u e. CC /\ y e. A ) -> ( u .h y ) e. A )
49 funfvima2 
 |-  ( ( Fun T /\ A C_ dom T ) -> ( ( u .h y ) e. A -> ( T ` ( u .h y ) ) e. ( T " A ) ) )
50 12 15 49 mp2an 
 |-  ( ( u .h y ) e. A -> ( T ` ( u .h y ) ) e. ( T " A ) )
51 48 50 syl 
 |-  ( ( u e. CC /\ y e. A ) -> ( T ` ( u .h y ) ) e. ( T " A ) )
52 46 51 eqeltrrd 
 |-  ( ( u e. CC /\ y e. A ) -> ( u .h ( T ` y ) ) e. ( T " A ) )
53 52 ralrimiva 
 |-  ( u e. CC -> A. y e. A ( u .h ( T ` y ) ) e. ( T " A ) )
54 oveq2 
 |-  ( v = ( T ` y ) -> ( u .h v ) = ( u .h ( T ` y ) ) )
55 54 eleq1d 
 |-  ( v = ( T ` y ) -> ( ( u .h v ) e. ( T " A ) <-> ( u .h ( T ` y ) ) e. ( T " A ) ) )
56 55 ralima 
 |-  ( ( T Fn ~H /\ A C_ ~H ) -> ( A. v e. ( T " A ) ( u .h v ) e. ( T " A ) <-> A. y e. A ( u .h ( T ` y ) ) e. ( T " A ) ) )
57 22 13 56 mp2an 
 |-  ( A. v e. ( T " A ) ( u .h v ) e. ( T " A ) <-> A. y e. A ( u .h ( T ` y ) ) e. ( T " A ) )
58 53 57 sylibr 
 |-  ( u e. CC -> A. v e. ( T " A ) ( u .h v ) e. ( T " A ) )
59 58 rgen 
 |-  A. u e. CC A. v e. ( T " A ) ( u .h v ) e. ( T " A )
60 44 59 pm3.2i 
 |-  ( A. u e. ( T " A ) A. v e. ( T " A ) ( u +h v ) e. ( T " A ) /\ A. u e. CC A. v e. ( T " A ) ( u .h v ) e. ( T " A ) )
61 issh2 
 |-  ( ( T " A ) e. SH <-> ( ( ( T " A ) C_ ~H /\ 0h e. ( T " A ) ) /\ ( A. u e. ( T " A ) A. v e. ( T " A ) ( u +h v ) e. ( T " A ) /\ A. u e. CC A. v e. ( T " A ) ( u .h v ) e. ( T " A ) ) ) )
62 20 60 61 mpbir2an 
 |-  ( T " A ) e. SH