Theorem lspprel

Description: Member of the span of a pair of vectors. (Contributed by NM, 10-Apr-2015)

	Ref	Expression
Hypotheses	lsppr.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lsppr.a	⊢ + = ( +g ‘ 𝑊 )
	lsppr.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	lsppr.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
	lsppr.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
	lsppr.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	lsppr.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	lsppr.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	lsppr.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
Assertion	lspprel	⊢ ( 𝜑 → ( 𝑍 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ↔ ∃ 𝑘 ∈ 𝐾 ∃ 𝑙 ∈ 𝐾 𝑍 = ( ( 𝑘 · 𝑋 ) + ( 𝑙 · 𝑌 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		lsppr.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lsppr.a	⊢ + = ( +g ‘ 𝑊 )
3		lsppr.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4		lsppr.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
5		lsppr.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
6		lsppr.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
7		lsppr.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
8		lsppr.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
9		lsppr.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
10	1 2 3 4 5 6 7 8 9	lsppr	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 ∃ 𝑙 ∈ 𝐾 𝑣 = ( ( 𝑘 · 𝑋 ) + ( 𝑙 · 𝑌 ) ) } )
11	10	eleq2d	⊢ ( 𝜑 → ( 𝑍 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ↔ 𝑍 ∈ { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 ∃ 𝑙 ∈ 𝐾 𝑣 = ( ( 𝑘 · 𝑋 ) + ( 𝑙 · 𝑌 ) ) } ) )
12		id	⊢ ( 𝑍 = ( ( 𝑘 · 𝑋 ) + ( 𝑙 · 𝑌 ) ) → 𝑍 = ( ( 𝑘 · 𝑋 ) + ( 𝑙 · 𝑌 ) ) )
13		ovex	⊢ ( ( 𝑘 · 𝑋 ) + ( 𝑙 · 𝑌 ) ) ∈ V
14	12 13	eqeltrdi	⊢ ( 𝑍 = ( ( 𝑘 · 𝑋 ) + ( 𝑙 · 𝑌 ) ) → 𝑍 ∈ V )
15	14	rexlimivw	⊢ ( ∃ 𝑙 ∈ 𝐾 𝑍 = ( ( 𝑘 · 𝑋 ) + ( 𝑙 · 𝑌 ) ) → 𝑍 ∈ V )
16	15	rexlimivw	⊢ ( ∃ 𝑘 ∈ 𝐾 ∃ 𝑙 ∈ 𝐾 𝑍 = ( ( 𝑘 · 𝑋 ) + ( 𝑙 · 𝑌 ) ) → 𝑍 ∈ V )
17		eqeq1	⊢ ( 𝑣 = 𝑍 → ( 𝑣 = ( ( 𝑘 · 𝑋 ) + ( 𝑙 · 𝑌 ) ) ↔ 𝑍 = ( ( 𝑘 · 𝑋 ) + ( 𝑙 · 𝑌 ) ) ) )
18	17	2rexbidv	⊢ ( 𝑣 = 𝑍 → ( ∃ 𝑘 ∈ 𝐾 ∃ 𝑙 ∈ 𝐾 𝑣 = ( ( 𝑘 · 𝑋 ) + ( 𝑙 · 𝑌 ) ) ↔ ∃ 𝑘 ∈ 𝐾 ∃ 𝑙 ∈ 𝐾 𝑍 = ( ( 𝑘 · 𝑋 ) + ( 𝑙 · 𝑌 ) ) ) )
19	16 18	elab3	⊢ ( 𝑍 ∈ { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 ∃ 𝑙 ∈ 𝐾 𝑣 = ( ( 𝑘 · 𝑋 ) + ( 𝑙 · 𝑌 ) ) } ↔ ∃ 𝑘 ∈ 𝐾 ∃ 𝑙 ∈ 𝐾 𝑍 = ( ( 𝑘 · 𝑋 ) + ( 𝑙 · 𝑌 ) ) )
20	11 19	bitrdi	⊢ ( 𝜑 → ( 𝑍 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ↔ ∃ 𝑘 ∈ 𝐾 ∃ 𝑙 ∈ 𝐾 𝑍 = ( ( 𝑘 · 𝑋 ) + ( 𝑙 · 𝑌 ) ) ) )