Theorem sspmlem

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

	Ref	Expression
Hypotheses	sspmlem.y	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
	sspmlem.h	⊢ 𝐻 = ( SubSp ‘ 𝑈 )
	sspmlem.1	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
	sspmlem.2	⊢ ( 𝑊 ∈ NrmCVec → 𝐹 : ( 𝑌 × 𝑌 ) ⟶ 𝑅 )
	sspmlem.3	⊢ ( 𝑈 ∈ NrmCVec → 𝐺 : ( ( BaseSet ‘ 𝑈 ) × ( BaseSet ‘ 𝑈 ) ) ⟶ 𝑆 )
Assertion	sspmlem	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝐹 = ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sspmlem.y	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
2		sspmlem.h	⊢ 𝐻 = ( SubSp ‘ 𝑈 )
3		sspmlem.1	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
4		sspmlem.2	⊢ ( 𝑊 ∈ NrmCVec → 𝐹 : ( 𝑌 × 𝑌 ) ⟶ 𝑅 )
5		sspmlem.3	⊢ ( 𝑈 ∈ NrmCVec → 𝐺 : ( ( BaseSet ‘ 𝑈 ) × ( BaseSet ‘ 𝑈 ) ) ⟶ 𝑆 )
6		ovres	⊢ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑥 ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
7	6	adantl	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝑥 ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
8	3 7	eqtr4d	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝑥 𝐹 𝑦 ) = ( 𝑥 ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) 𝑦 ) )
9	8	ralrimivva	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ∀ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) 𝑦 ) )
10		eqid	⊢ ( 𝑌 × 𝑌 ) = ( 𝑌 × 𝑌 )
11	9 10	jctil	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( ( 𝑌 × 𝑌 ) = ( 𝑌 × 𝑌 ) ∧ ∀ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) 𝑦 ) ) )
12	2	sspnv	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝑊 ∈ NrmCVec )
13		ffn	⊢ ( 𝐹 : ( 𝑌 × 𝑌 ) ⟶ 𝑅 → 𝐹 Fn ( 𝑌 × 𝑌 ) )
14	12 4 13	3syl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝐹 Fn ( 𝑌 × 𝑌 ) )
15	5	ffnd	⊢ ( 𝑈 ∈ NrmCVec → 𝐺 Fn ( ( BaseSet ‘ 𝑈 ) × ( BaseSet ‘ 𝑈 ) ) )
16	15	adantr	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝐺 Fn ( ( BaseSet ‘ 𝑈 ) × ( BaseSet ‘ 𝑈 ) ) )
17		eqid	⊢ ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ 𝑈 )
18	17 1 2	sspba	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝑌 ⊆ ( BaseSet ‘ 𝑈 ) )
19		xpss12	⊢ ( ( 𝑌 ⊆ ( BaseSet ‘ 𝑈 ) ∧ 𝑌 ⊆ ( BaseSet ‘ 𝑈 ) ) → ( 𝑌 × 𝑌 ) ⊆ ( ( BaseSet ‘ 𝑈 ) × ( BaseSet ‘ 𝑈 ) ) )
20	18 18 19	syl2anc	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( 𝑌 × 𝑌 ) ⊆ ( ( BaseSet ‘ 𝑈 ) × ( BaseSet ‘ 𝑈 ) ) )
21		fnssres	⊢ ( ( 𝐺 Fn ( ( BaseSet ‘ 𝑈 ) × ( BaseSet ‘ 𝑈 ) ) ∧ ( 𝑌 × 𝑌 ) ⊆ ( ( BaseSet ‘ 𝑈 ) × ( BaseSet ‘ 𝑈 ) ) ) → ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) Fn ( 𝑌 × 𝑌 ) )
22	16 20 21	syl2anc	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) Fn ( 𝑌 × 𝑌 ) )
23		eqfnov	⊢ ( ( 𝐹 Fn ( 𝑌 × 𝑌 ) ∧ ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) Fn ( 𝑌 × 𝑌 ) ) → ( 𝐹 = ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) ↔ ( ( 𝑌 × 𝑌 ) = ( 𝑌 × 𝑌 ) ∧ ∀ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) 𝑦 ) ) ) )
24	14 22 23	syl2anc	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( 𝐹 = ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) ↔ ( ( 𝑌 × 𝑌 ) = ( 𝑌 × 𝑌 ) ∧ ∀ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) 𝑦 ) ) ) )
25	11 24	mpbird	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝐹 = ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) )