sspmlem

Description: Lemma for sspm and others. (Contributed by NM, 1-Feb-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	sspmlem.y	$⊢ Y = BaseSet (W)$
	sspmlem.h	$⊢ H = SubSp (U)$
	sspmlem.1	$⊢ ((U \in NrmCVec \land W \in H) \land (x \in Y \land y \in Y)) \to x F y = x G y$
	sspmlem.2	$⊢ W \in NrmCVec \to F : Y \times Y ⟶ R$
	sspmlem.3	$⊢ U \in NrmCVec \to G : BaseSet (U) \times BaseSet (U) ⟶ S$
Assertion	sspmlem	$⊢ (U \in NrmCVec \land W \in H) \to F = {G ↾}_{(Y \times Y)}$

Proof

Step	Hyp	Ref	Expression
1		sspmlem.y	$⊢ Y = BaseSet (W)$
2		sspmlem.h	$⊢ H = SubSp (U)$
3		sspmlem.1	$⊢ ((U \in NrmCVec \land W \in H) \land (x \in Y \land y \in Y)) \to x F y = x G y$
4		sspmlem.2	$⊢ W \in NrmCVec \to F : Y \times Y ⟶ R$
5		sspmlem.3	$⊢ U \in NrmCVec \to G : BaseSet (U) \times BaseSet (U) ⟶ S$
6		ovres	$⊢ (x \in Y \land y \in Y) \to x ({G ↾}_{(Y \times Y)}) y = x G y$
7	6	adantl	$⊢ ((U \in NrmCVec \land W \in H) \land (x \in Y \land y \in Y)) \to x ({G ↾}_{(Y \times Y)}) y = x G y$
8	3 7	eqtr4d	$⊢ ((U \in NrmCVec \land W \in H) \land (x \in Y \land y \in Y)) \to x F y = x ({G ↾}_{(Y \times Y)}) y$
9	8	ralrimivva	$⊢ (U \in NrmCVec \land W \in H) \to \forall x \in Y \forall y \in Y x F y = x ({G ↾}_{(Y \times Y)}) y$
10		eqid	$⊢ Y \times Y = Y \times Y$
11	9 10	jctil	$⊢ (U \in NrmCVec \land W \in H) \to (Y \times Y = Y \times Y \land \forall x \in Y \forall y \in Y x F y = x ({G ↾}_{(Y \times Y)}) y)$
12	2	sspnv	$⊢ (U \in NrmCVec \land W \in H) \to W \in NrmCVec$
13		ffn	$⊢ F : Y \times Y ⟶ R \to F Fn (Y \times Y)$
14	12 4 13	3syl	$⊢ (U \in NrmCVec \land W \in H) \to F Fn (Y \times Y)$
15	5	ffnd	$⊢ U \in NrmCVec \to G Fn (BaseSet (U) \times BaseSet (U))$
16	15	adantr	$⊢ (U \in NrmCVec \land W \in H) \to G Fn (BaseSet (U) \times BaseSet (U))$
17		eqid	$⊢ BaseSet (U) = BaseSet (U)$
18	17 1 2	sspba	$⊢ (U \in NrmCVec \land W \in H) \to Y \subseteq BaseSet (U)$
19		xpss12	$⊢ (Y \subseteq BaseSet (U) \land Y \subseteq BaseSet (U)) \to Y \times Y \subseteq BaseSet (U) \times BaseSet (U)$
20	18 18 19	syl2anc	$⊢ (U \in NrmCVec \land W \in H) \to Y \times Y \subseteq BaseSet (U) \times BaseSet (U)$
21		fnssres	$⊢ (G Fn (BaseSet (U) \times BaseSet (U)) \land Y \times Y \subseteq BaseSet (U) \times BaseSet (U)) \to ({G ↾}_{(Y \times Y)}) Fn (Y \times Y)$
22	16 20 21	syl2anc	$⊢ (U \in NrmCVec \land W \in H) \to ({G ↾}_{(Y \times Y)}) Fn (Y \times Y)$
23		eqfnov	$⊢ (F Fn (Y \times Y) \land ({G ↾}_{(Y \times Y)}) Fn (Y \times Y)) \to (F = {G ↾}_{(Y \times Y)} \leftrightarrow (Y \times Y = Y \times Y \land \forall x \in Y \forall y \in Y x F y = x ({G ↾}_{(Y \times Y)}) y))$
24	14 22 23	syl2anc	$⊢ (U \in NrmCVec \land W \in H) \to (F = {G ↾}_{(Y \times Y)} \leftrightarrow (Y \times Y = Y \times Y \land \forall x \in Y \forall y \in Y x F y = x ({G ↾}_{(Y \times Y)}) y))$
25	11 24	mpbird	$⊢ (U \in NrmCVec \land W \in H) \to F = {G ↾}_{(Y \times Y)}$

Metamath Proof Explorer

Theorem sspmlem

Proof