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 ⊢ 𝑇 ∈ LinOp
imaelsh.2 ⊢ 𝐴 ∈ Sℋ
Assertion imaelshi ( 𝑇 “ 𝐴 ) ∈ Sℋ

Proof

Step Hyp Ref Expression
1 rnelsh.1 ⊢ 𝑇 ∈ LinOp
2 imaelsh.2 ⊢ 𝐴 ∈ Sℋ
3 imassrn ⊢ ( 𝑇 “ 𝐴 ) ⊆ ran 𝑇
4 1 lnopfi ⊢ 𝑇 : ℋ ⟶ ℋ
5 frn ⊢ ( 𝑇 : ℋ ⟶ ℋ → ran 𝑇 ⊆ ℋ )
6 4 5 ax-mp ⊢ ran 𝑇 ⊆ ℋ
7 3 6 sstri ⊢ ( 𝑇 “ 𝐴 ) ⊆ ℋ
8 1 lnop0i ⊢ ( 𝑇 ‘ 0ℎ ) = 0ℎ
9 sh0 ⊢ ( 𝐴 ∈ Sℋ → 0ℎ ∈ 𝐴 )
10 2 9 ax-mp ⊢ 0ℎ ∈ 𝐴
11 ffun ⊢ ( 𝑇 : ℋ ⟶ ℋ → Fun 𝑇 )
12 4 11 ax-mp ⊢ Fun 𝑇
13 2 shssii ⊢ 𝐴 ⊆ ℋ
14 4 fdmi ⊢ dom 𝑇 = ℋ
15 13 14 sseqtrri ⊢ 𝐴 ⊆ dom 𝑇
16 funfvima2 ⊢ ( ( Fun 𝑇 ∧ 𝐴 ⊆ dom 𝑇 ) → ( 0ℎ ∈ 𝐴 → ( 𝑇 ‘ 0ℎ ) ∈ ( 𝑇 “ 𝐴 ) ) )
17 12 15 16 mp2an ⊢ ( 0ℎ ∈ 𝐴 → ( 𝑇 ‘ 0ℎ ) ∈ ( 𝑇 “ 𝐴 ) )
18 10 17 ax-mp ⊢ ( 𝑇 ‘ 0ℎ ) ∈ ( 𝑇 “ 𝐴 )
19 8 18 eqeltrri ⊢ 0ℎ ∈ ( 𝑇 “ 𝐴 )
20 7 19 pm3.2i ⊢ ( ( 𝑇 “ 𝐴 ) ⊆ ℋ ∧ 0ℎ ∈ ( 𝑇 “ 𝐴 ) )
21 ffn ⊢ ( 𝑇 : ℋ ⟶ ℋ → 𝑇 Fn ℋ )
22 4 21 ax-mp ⊢ 𝑇 Fn ℋ
23 oveq1 ⊢ ( 𝑢 = ( 𝑇 ‘ 𝑥 ) → ( 𝑢 +ℎ 𝑣 ) = ( ( 𝑇 ‘ 𝑥 ) +ℎ 𝑣 ) )
24 23 eleq1d ⊢ ( 𝑢 = ( 𝑇 ‘ 𝑥 ) → ( ( 𝑢 +ℎ 𝑣 ) ∈ ( 𝑇 “ 𝐴 ) ↔ ( ( 𝑇 ‘ 𝑥 ) +ℎ 𝑣 ) ∈ ( 𝑇 “ 𝐴 ) ) )
25 24 ralbidv ⊢ ( 𝑢 = ( 𝑇 ‘ 𝑥 ) → ( ∀ 𝑣 ∈ ( 𝑇 “ 𝐴 ) ( 𝑢 +ℎ 𝑣 ) ∈ ( 𝑇 “ 𝐴 ) ↔ ∀ 𝑣 ∈ ( 𝑇 “ 𝐴 ) ( ( 𝑇 ‘ 𝑥 ) +ℎ 𝑣 ) ∈ ( 𝑇 “ 𝐴 ) ) )
26 25 ralima ⊢ ( ( 𝑇 Fn ℋ ∧ 𝐴 ⊆ ℋ ) → ( ∀ 𝑢 ∈ ( 𝑇 “ 𝐴 ) ∀ 𝑣 ∈ ( 𝑇 “ 𝐴 ) ( 𝑢 +ℎ 𝑣 ) ∈ ( 𝑇 “ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑣 ∈ ( 𝑇 “ 𝐴 ) ( ( 𝑇 ‘ 𝑥 ) +ℎ 𝑣 ) ∈ ( 𝑇 “ 𝐴 ) ) )
27 22 13 26 mp2an ⊢ ( ∀ 𝑢 ∈ ( 𝑇 “ 𝐴 ) ∀ 𝑣 ∈ ( 𝑇 “ 𝐴 ) ( 𝑢 +ℎ 𝑣 ) ∈ ( 𝑇 “ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑣 ∈ ( 𝑇 “ 𝐴 ) ( ( 𝑇 ‘ 𝑥 ) +ℎ 𝑣 ) ∈ ( 𝑇 “ 𝐴 ) )
28 2 sheli ⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ℋ )
29 2 sheli ⊢ ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ℋ )
30 1 lnopaddi ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑇 ‘ ( 𝑥 +ℎ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑦 ) ) )
31 28 29 30 syl2an ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑇 ‘ ( 𝑥 +ℎ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑦 ) ) )
32 shaddcl ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 +ℎ 𝑦 ) ∈ 𝐴 )
33 2 32 mp3an1 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 +ℎ 𝑦 ) ∈ 𝐴 )
34 funfvima2 ⊢ ( ( Fun 𝑇 ∧ 𝐴 ⊆ dom 𝑇 ) → ( ( 𝑥 +ℎ 𝑦 ) ∈ 𝐴 → ( 𝑇 ‘ ( 𝑥 +ℎ 𝑦 ) ) ∈ ( 𝑇 “ 𝐴 ) ) )
35 12 15 34 mp2an ⊢ ( ( 𝑥 +ℎ 𝑦 ) ∈ 𝐴 → ( 𝑇 ‘ ( 𝑥 +ℎ 𝑦 ) ) ∈ ( 𝑇 “ 𝐴 ) )
36 33 35 syl ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑇 ‘ ( 𝑥 +ℎ 𝑦 ) ) ∈ ( 𝑇 “ 𝐴 ) )
37 31 36 eqeltrrd ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑇 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑦 ) ) ∈ ( 𝑇 “ 𝐴 ) )
38 37 ralrimiva ⊢ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐴 ( ( 𝑇 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑦 ) ) ∈ ( 𝑇 “ 𝐴 ) )
39 oveq2 ⊢ ( 𝑣 = ( 𝑇 ‘ 𝑦 ) → ( ( 𝑇 ‘ 𝑥 ) +ℎ 𝑣 ) = ( ( 𝑇 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑦 ) ) )
40 39 eleq1d ⊢ ( 𝑣 = ( 𝑇 ‘ 𝑦 ) → ( ( ( 𝑇 ‘ 𝑥 ) +ℎ 𝑣 ) ∈ ( 𝑇 “ 𝐴 ) ↔ ( ( 𝑇 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑦 ) ) ∈ ( 𝑇 “ 𝐴 ) ) )
41 40 ralima ⊢ ( ( 𝑇 Fn ℋ ∧ 𝐴 ⊆ ℋ ) → ( ∀ 𝑣 ∈ ( 𝑇 “ 𝐴 ) ( ( 𝑇 ‘ 𝑥 ) +ℎ 𝑣 ) ∈ ( 𝑇 “ 𝐴 ) ↔ ∀ 𝑦 ∈ 𝐴 ( ( 𝑇 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑦 ) ) ∈ ( 𝑇 “ 𝐴 ) ) )
42 22 13 41 mp2an ⊢ ( ∀ 𝑣 ∈ ( 𝑇 “ 𝐴 ) ( ( 𝑇 ‘ 𝑥 ) +ℎ 𝑣 ) ∈ ( 𝑇 “ 𝐴 ) ↔ ∀ 𝑦 ∈ 𝐴 ( ( 𝑇 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑦 ) ) ∈ ( 𝑇 “ 𝐴 ) )
43 38 42 sylibr ⊢ ( 𝑥 ∈ 𝐴 → ∀ 𝑣 ∈ ( 𝑇 “ 𝐴 ) ( ( 𝑇 ‘ 𝑥 ) +ℎ 𝑣 ) ∈ ( 𝑇 “ 𝐴 ) )
44 27 43 mprgbir ⊢ ∀ 𝑢 ∈ ( 𝑇 “ 𝐴 ) ∀ 𝑣 ∈ ( 𝑇 “ 𝐴 ) ( 𝑢 +ℎ 𝑣 ) ∈ ( 𝑇 “ 𝐴 )
45 1 lnopmuli ⊢ ( ( 𝑢 ∈ ℂ ∧ 𝑦 ∈ ℋ ) → ( 𝑇 ‘ ( 𝑢 ·ℎ 𝑦 ) ) = ( 𝑢 ·ℎ ( 𝑇 ‘ 𝑦 ) ) )
46 29 45 sylan2 ⊢ ( ( 𝑢 ∈ ℂ ∧ 𝑦 ∈ 𝐴 ) → ( 𝑇 ‘ ( 𝑢 ·ℎ 𝑦 ) ) = ( 𝑢 ·ℎ ( 𝑇 ‘ 𝑦 ) ) )
47 shmulcl ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝑢 ∈ ℂ ∧ 𝑦 ∈ 𝐴 ) → ( 𝑢 ·ℎ 𝑦 ) ∈ 𝐴 )
48 2 47 mp3an1 ⊢ ( ( 𝑢 ∈ ℂ ∧ 𝑦 ∈ 𝐴 ) → ( 𝑢 ·ℎ 𝑦 ) ∈ 𝐴 )
49 funfvima2 ⊢ ( ( Fun 𝑇 ∧ 𝐴 ⊆ dom 𝑇 ) → ( ( 𝑢 ·ℎ 𝑦 ) ∈ 𝐴 → ( 𝑇 ‘ ( 𝑢 ·ℎ 𝑦 ) ) ∈ ( 𝑇 “ 𝐴 ) ) )
50 12 15 49 mp2an ⊢ ( ( 𝑢 ·ℎ 𝑦 ) ∈ 𝐴 → ( 𝑇 ‘ ( 𝑢 ·ℎ 𝑦 ) ) ∈ ( 𝑇 “ 𝐴 ) )
51 48 50 syl ⊢ ( ( 𝑢 ∈ ℂ ∧ 𝑦 ∈ 𝐴 ) → ( 𝑇 ‘ ( 𝑢 ·ℎ 𝑦 ) ) ∈ ( 𝑇 “ 𝐴 ) )
52 46 51 eqeltrrd ⊢ ( ( 𝑢 ∈ ℂ ∧ 𝑦 ∈ 𝐴 ) → ( 𝑢 ·ℎ ( 𝑇 ‘ 𝑦 ) ) ∈ ( 𝑇 “ 𝐴 ) )
53 52 ralrimiva ⊢ ( 𝑢 ∈ ℂ → ∀ 𝑦 ∈ 𝐴 ( 𝑢 ·ℎ ( 𝑇 ‘ 𝑦 ) ) ∈ ( 𝑇 “ 𝐴 ) )
54 oveq2 ⊢ ( 𝑣 = ( 𝑇 ‘ 𝑦 ) → ( 𝑢 ·ℎ 𝑣 ) = ( 𝑢 ·ℎ ( 𝑇 ‘ 𝑦 ) ) )
55 54 eleq1d ⊢ ( 𝑣 = ( 𝑇 ‘ 𝑦 ) → ( ( 𝑢 ·ℎ 𝑣 ) ∈ ( 𝑇 “ 𝐴 ) ↔ ( 𝑢 ·ℎ ( 𝑇 ‘ 𝑦 ) ) ∈ ( 𝑇 “ 𝐴 ) ) )
56 55 ralima ⊢ ( ( 𝑇 Fn ℋ ∧ 𝐴 ⊆ ℋ ) → ( ∀ 𝑣 ∈ ( 𝑇 “ 𝐴 ) ( 𝑢 ·ℎ 𝑣 ) ∈ ( 𝑇 “ 𝐴 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑢 ·ℎ ( 𝑇 ‘ 𝑦 ) ) ∈ ( 𝑇 “ 𝐴 ) ) )
57 22 13 56 mp2an ⊢ ( ∀ 𝑣 ∈ ( 𝑇 “ 𝐴 ) ( 𝑢 ·ℎ 𝑣 ) ∈ ( 𝑇 “ 𝐴 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑢 ·ℎ ( 𝑇 ‘ 𝑦 ) ) ∈ ( 𝑇 “ 𝐴 ) )
58 53 57 sylibr ⊢ ( 𝑢 ∈ ℂ → ∀ 𝑣 ∈ ( 𝑇 “ 𝐴 ) ( 𝑢 ·ℎ 𝑣 ) ∈ ( 𝑇 “ 𝐴 ) )
59 58 rgen ⊢ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ( 𝑇 “ 𝐴 ) ( 𝑢 ·ℎ 𝑣 ) ∈ ( 𝑇 “ 𝐴 )
60 44 59 pm3.2i ⊢ ( ∀ 𝑢 ∈ ( 𝑇 “ 𝐴 ) ∀ 𝑣 ∈ ( 𝑇 “ 𝐴 ) ( 𝑢 +ℎ 𝑣 ) ∈ ( 𝑇 “ 𝐴 ) ∧ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ( 𝑇 “ 𝐴 ) ( 𝑢 ·ℎ 𝑣 ) ∈ ( 𝑇 “ 𝐴 ) )
61 issh2 ⊢ ( ( 𝑇 “ 𝐴 ) ∈ Sℋ ↔ ( ( ( 𝑇 “ 𝐴 ) ⊆ ℋ ∧ 0ℎ ∈ ( 𝑇 “ 𝐴 ) ) ∧ ( ∀ 𝑢 ∈ ( 𝑇 “ 𝐴 ) ∀ 𝑣 ∈ ( 𝑇 “ 𝐴 ) ( 𝑢 +ℎ 𝑣 ) ∈ ( 𝑇 “ 𝐴 ) ∧ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ( 𝑇 “ 𝐴 ) ( 𝑢 ·ℎ 𝑣 ) ∈ ( 𝑇 “ 𝐴 ) ) ) )
62 20 60 61 mpbir2an ⊢ ( 𝑇 “ 𝐴 ) ∈ Sℋ