islno

Description: The predicate "is a linear operator." (Contributed by NM, 4-Dec-2007) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lnoval.1	$⊢ X = BaseSet (U)$
	lnoval.2	$⊢ Y = BaseSet (W)$
	lnoval.3	$⊢ G = +_{v} (U)$
	lnoval.4	$⊢ H = +_{v} (W)$
	lnoval.5	$⊢ R = \cdot_{𝑠OLD} (U)$
	lnoval.6	$⊢ S = \cdot_{𝑠OLD} (W)$
	lnoval.7	$⊢ L = U LnOp W$
Assertion	islno	$⊢ (U \in NrmCVec \land W \in NrmCVec) \to (T \in L \leftrightarrow (T : X ⟶ Y \land \forall x \in ℂ \forall y \in X \forall z \in X T ((x R y) G z) = (x S T (y)) H T (z)))$

Proof

Step	Hyp	Ref	Expression
1		lnoval.1	$⊢ X = BaseSet (U)$
2		lnoval.2	$⊢ Y = BaseSet (W)$
3		lnoval.3	$⊢ G = +_{v} (U)$
4		lnoval.4	$⊢ H = +_{v} (W)$
5		lnoval.5	$⊢ R = \cdot_{𝑠OLD} (U)$
6		lnoval.6	$⊢ S = \cdot_{𝑠OLD} (W)$
7		lnoval.7	$⊢ L = U LnOp W$
8	1 2 3 4 5 6 7	lnoval	$⊢ (U \in NrmCVec \land W \in NrmCVec) \to L = \{w \in (Y^{X}) \| \forall x \in ℂ \forall y \in X \forall z \in X w ((x R y) G z) = (x S w (y)) H w (z)\}$
9	8	eleq2d	$⊢ (U \in NrmCVec \land W \in NrmCVec) \to (T \in L \leftrightarrow T \in \{w \in (Y^{X}) \| \forall x \in ℂ \forall y \in X \forall z \in X w ((x R y) G z) = (x S w (y)) H w (z)\})$
10		fveq1	$⊢ w = T \to w ((x R y) G z) = T ((x R y) G z)$
11		fveq1	$⊢ w = T \to w (y) = T (y)$
12	11	oveq2d	$⊢ w = T \to x S w (y) = x S T (y)$
13		fveq1	$⊢ w = T \to w (z) = T (z)$
14	12 13	oveq12d	$⊢ w = T \to (x S w (y)) H w (z) = (x S T (y)) H T (z)$
15	10 14	eqeq12d	$⊢ w = T \to (w ((x R y) G z) = (x S w (y)) H w (z) \leftrightarrow T ((x R y) G z) = (x S T (y)) H T (z))$
16	15	2ralbidv	$⊢ w = T \to (\forall y \in X \forall z \in X w ((x R y) G z) = (x S w (y)) H w (z) \leftrightarrow \forall y \in X \forall z \in X T ((x R y) G z) = (x S T (y)) H T (z))$
17	16	ralbidv	$⊢ w = T \to (\forall x \in ℂ \forall y \in X \forall z \in X w ((x R y) G z) = (x S w (y)) H w (z) \leftrightarrow \forall x \in ℂ \forall y \in X \forall z \in X T ((x R y) G z) = (x S T (y)) H T (z))$
18	17	elrab	$⊢ T \in \{w \in (Y^{X}) \| \forall x \in ℂ \forall y \in X \forall z \in X w ((x R y) G z) = (x S w (y)) H w (z)\} \leftrightarrow (T \in (Y^{X}) \land \forall x \in ℂ \forall y \in X \forall z \in X T ((x R y) G z) = (x S T (y)) H T (z))$
19	2	fvexi	$⊢ Y \in V$
20	1	fvexi	$⊢ X \in V$
21	19 20	elmap	$⊢ T \in (Y^{X}) \leftrightarrow T : X ⟶ Y$
22	21	anbi1i	$⊢ (T \in (Y^{X}) \land \forall x \in ℂ \forall y \in X \forall z \in X T ((x R y) G z) = (x S T (y)) H T (z)) \leftrightarrow (T : X ⟶ Y \land \forall x \in ℂ \forall y \in X \forall z \in X T ((x R y) G z) = (x S T (y)) H T (z))$
23	18 22	bitri	$⊢ T \in \{w \in (Y^{X}) \| \forall x \in ℂ \forall y \in X \forall z \in X w ((x R y) G z) = (x S w (y)) H w (z)\} \leftrightarrow (T : X ⟶ Y \land \forall x \in ℂ \forall y \in X \forall z \in X T ((x R y) G z) = (x S T (y)) H T (z))$
24	9 23	bitrdi	$⊢ (U \in NrmCVec \land W \in NrmCVec) \to (T \in L \leftrightarrow (T : X ⟶ Y \land \forall x \in ℂ \forall y \in X \forall z \in X T ((x R y) G z) = (x S T (y)) H T (z)))$

Metamath Proof Explorer

Theorem islno

Proof