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 \in LinOp$
	imaelsh.2	$⊢ A \in S_{ℋ}$
Assertion	imaelshi	$⊢ T [A] \in S_{ℋ}$

Proof

Step	Hyp	Ref	Expression
1		rnelsh.1	$⊢ T \in LinOp$
2		imaelsh.2	$⊢ A \in S_{ℋ}$
3		imassrn	$⊢ T [A] \subseteq ran T$
4	1	lnopfi	$⊢ T : ℋ ⟶ ℋ$
5		frn	$⊢ T : ℋ ⟶ ℋ \to ran T \subseteq ℋ$
6	4 5	ax-mp	$⊢ ran T \subseteq ℋ$
7	3 6	sstri	$⊢ T [A] \subseteq ℋ$
8	1	lnop0i	$⊢ T (0_{ℎ}) = 0_{ℎ}$
9		sh0	$⊢ A \in S_{ℋ} \to 0_{ℎ} \in A$
10	2 9	ax-mp	$⊢ 0_{ℎ} \in A$
11		ffun	$⊢ T : ℋ ⟶ ℋ \to Fun T$
12	4 11	ax-mp	$⊢ Fun T$
13	2	shssii	$⊢ A \subseteq ℋ$
14	4	fdmi	$⊢ dom T = ℋ$
15	13 14	sseqtrri	$⊢ A \subseteq dom T$
16		funfvima2	$⊢ (Fun T \land A \subseteq dom T) \to (0_{ℎ} \in A \to T (0_{ℎ}) \in T [A])$
17	12 15 16	mp2an	$⊢ 0_{ℎ} \in A \to T (0_{ℎ}) \in T [A]$
18	10 17	ax-mp	$⊢ T (0_{ℎ}) \in T [A]$
19	8 18	eqeltrri	$⊢ 0_{ℎ} \in T [A]$
20	7 19	pm3.2i	$⊢ (T [A] \subseteq ℋ \land 0_{ℎ} \in T [A])$
21		ffn	$⊢ T : ℋ ⟶ ℋ \to T Fn ℋ$
22	4 21	ax-mp	$⊢ T Fn ℋ$
23		oveq1	$⊢ u = T (x) \to u +_{ℎ} v = T (x) +_{ℎ} v$
24	23	eleq1d	$⊢ u = T (x) \to (u +_{ℎ} v \in T [A] \leftrightarrow T (x) +_{ℎ} v \in T [A])$
25	24	ralbidv	$⊢ u = T (x) \to (\forall v \in T [A] u +_{ℎ} v \in T [A] \leftrightarrow \forall v \in T [A] T (x) +_{ℎ} v \in T [A])$
26	25	ralima	$⊢ (T Fn ℋ \land A \subseteq ℋ) \to (\forall u \in T [A] \forall v \in T [A] u +_{ℎ} v \in T [A] \leftrightarrow \forall x \in A \forall v \in T [A] T (x) +_{ℎ} v \in T [A])$
27	22 13 26	mp2an	$⊢ \forall u \in T [A] \forall v \in T [A] u +_{ℎ} v \in T [A] \leftrightarrow \forall x \in A \forall v \in T [A] T (x) +_{ℎ} v \in T [A]$
28	2	sheli	$⊢ x \in A \to x \in ℋ$
29	2	sheli	$⊢ y \in A \to y \in ℋ$
30	1	lnopaddi	$⊢ (x \in ℋ \land y \in ℋ) \to T (x +_{ℎ} y) = T (x) +_{ℎ} T (y)$
31	28 29 30	syl2an	$⊢ (x \in A \land y \in A) \to T (x +_{ℎ} y) = T (x) +_{ℎ} T (y)$
32		shaddcl	$⊢ (A \in S_{ℋ} \land x \in A \land y \in A) \to x +_{ℎ} y \in A$
33	2 32	mp3an1	$⊢ (x \in A \land y \in A) \to x +_{ℎ} y \in A$
34		funfvima2	$⊢ (Fun T \land A \subseteq dom T) \to (x +_{ℎ} y \in A \to T (x +_{ℎ} y) \in T [A])$
35	12 15 34	mp2an	$⊢ x +_{ℎ} y \in A \to T (x +_{ℎ} y) \in T [A]$
36	33 35	syl	$⊢ (x \in A \land y \in A) \to T (x +_{ℎ} y) \in T [A]$
37	31 36	eqeltrrd	$⊢ (x \in A \land y \in A) \to T (x) +_{ℎ} T (y) \in T [A]$
38	37	ralrimiva	$⊢ x \in A \to \forall y \in A T (x) +_{ℎ} T (y) \in T [A]$
39		oveq2	$⊢ v = T (y) \to T (x) +_{ℎ} v = T (x) +_{ℎ} T (y)$
40	39	eleq1d	$⊢ v = T (y) \to (T (x) +_{ℎ} v \in T [A] \leftrightarrow T (x) +_{ℎ} T (y) \in T [A])$
41	40	ralima	$⊢ (T Fn ℋ \land A \subseteq ℋ) \to (\forall v \in T [A] T (x) +_{ℎ} v \in T [A] \leftrightarrow \forall y \in A T (x) +_{ℎ} T (y) \in T [A])$
42	22 13 41	mp2an	$⊢ \forall v \in T [A] T (x) +_{ℎ} v \in T [A] \leftrightarrow \forall y \in A T (x) +_{ℎ} T (y) \in T [A]$
43	38 42	sylibr	$⊢ x \in A \to \forall v \in T [A] T (x) +_{ℎ} v \in T [A]$
44	27 43	mprgbir	$⊢ \forall u \in T [A] \forall v \in T [A] u +_{ℎ} v \in T [A]$
45	1	lnopmuli	$⊢ (u \in ℂ \land y \in ℋ) \to T (u \cdot_{ℎ} y) = u \cdot_{ℎ} T (y)$
46	29 45	sylan2	$⊢ (u \in ℂ \land y \in A) \to T (u \cdot_{ℎ} y) = u \cdot_{ℎ} T (y)$
47		shmulcl	$⊢ (A \in S_{ℋ} \land u \in ℂ \land y \in A) \to u \cdot_{ℎ} y \in A$
48	2 47	mp3an1	$⊢ (u \in ℂ \land y \in A) \to u \cdot_{ℎ} y \in A$
49		funfvima2	$⊢ (Fun T \land A \subseteq dom T) \to (u \cdot_{ℎ} y \in A \to T (u \cdot_{ℎ} y) \in T [A])$
50	12 15 49	mp2an	$⊢ u \cdot_{ℎ} y \in A \to T (u \cdot_{ℎ} y) \in T [A]$
51	48 50	syl	$⊢ (u \in ℂ \land y \in A) \to T (u \cdot_{ℎ} y) \in T [A]$
52	46 51	eqeltrrd	$⊢ (u \in ℂ \land y \in A) \to u \cdot_{ℎ} T (y) \in T [A]$
53	52	ralrimiva	$⊢ u \in ℂ \to \forall y \in A u \cdot_{ℎ} T (y) \in T [A]$
54		oveq2	$⊢ v = T (y) \to u \cdot_{ℎ} v = u \cdot_{ℎ} T (y)$
55	54	eleq1d	$⊢ v = T (y) \to (u \cdot_{ℎ} v \in T [A] \leftrightarrow u \cdot_{ℎ} T (y) \in T [A])$
56	55	ralima	$⊢ (T Fn ℋ \land A \subseteq ℋ) \to (\forall v \in T [A] u \cdot_{ℎ} v \in T [A] \leftrightarrow \forall y \in A u \cdot_{ℎ} T (y) \in T [A])$
57	22 13 56	mp2an	$⊢ \forall v \in T [A] u \cdot_{ℎ} v \in T [A] \leftrightarrow \forall y \in A u \cdot_{ℎ} T (y) \in T [A]$
58	53 57	sylibr	$⊢ u \in ℂ \to \forall v \in T [A] u \cdot_{ℎ} v \in T [A]$
59	58	rgen	$⊢ \forall u \in ℂ \forall v \in T [A] u \cdot_{ℎ} v \in T [A]$
60	44 59	pm3.2i	$⊢ (\forall u \in T [A] \forall v \in T [A] u +_{ℎ} v \in T [A] \land \forall u \in ℂ \forall v \in T [A] u \cdot_{ℎ} v \in T [A])$
61		issh2	$⊢ T [A] \in S_{ℋ} \leftrightarrow ((T [A] \subseteq ℋ \land 0_{ℎ} \in T [A]) \land (\forall u \in T [A] \forall v \in T [A] u +_{ℎ} v \in T [A] \land \forall u \in ℂ \forall v \in T [A] u \cdot_{ℎ} v \in T [A]))$
62	20 60 61	mpbir2an	$⊢ T [A] \in S_{ℋ}$

Metamath Proof Explorer

Theorem imaelshi

Proof