This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lspprel

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

Ref Expression
Hypotheses lsppr.v 
|- V = ( Base ` W )
lsppr.a 
|- .+ = ( +g ` W )
lsppr.f 
|- F = ( Scalar ` W )
lsppr.k 
|- K = ( Base ` F )
lsppr.t 
|- .x. = ( .s ` W )
lsppr.n 
|- N = ( LSpan ` W )
lsppr.w 
|- ( ph -> W e. LMod )
lsppr.x 
|- ( ph -> X e. V )
lsppr.y 
|- ( ph -> Y e. V )
Assertion lspprel 
|- ( ph -> ( Z e. ( N ` { X , Y } ) <-> E. k e. K E. l e. K Z = ( ( k .x. X ) .+ ( l .x. Y ) ) ) )

Proof

Step Hyp Ref Expression
1 lsppr.v 
 |-  V = ( Base ` W )
2 lsppr.a 
 |-  .+ = ( +g ` W )
3 lsppr.f 
 |-  F = ( Scalar ` W )
4 lsppr.k 
 |-  K = ( Base ` F )
5 lsppr.t 
 |-  .x. = ( .s ` W )
6 lsppr.n 
 |-  N = ( LSpan ` W )
7 lsppr.w 
 |-  ( ph -> W e. LMod )
8 lsppr.x 
 |-  ( ph -> X e. V )
9 lsppr.y 
 |-  ( ph -> Y e. V )
10 1 2 3 4 5 6 7 8 9 lsppr 
 |-  ( ph -> ( N ` { X , Y } ) = { v | E. k e. K E. l e. K v = ( ( k .x. X ) .+ ( l .x. Y ) ) } )
11 10 eleq2d 
 |-  ( ph -> ( Z e. ( N ` { X , Y } ) <-> Z e. { v | E. k e. K E. l e. K v = ( ( k .x. X ) .+ ( l .x. Y ) ) } ) )
12 id 
 |-  ( Z = ( ( k .x. X ) .+ ( l .x. Y ) ) -> Z = ( ( k .x. X ) .+ ( l .x. Y ) ) )
13 ovex 
 |-  ( ( k .x. X ) .+ ( l .x. Y ) ) e. _V
14 12 13 eqeltrdi 
 |-  ( Z = ( ( k .x. X ) .+ ( l .x. Y ) ) -> Z e. _V )
15 14 rexlimivw 
 |-  ( E. l e. K Z = ( ( k .x. X ) .+ ( l .x. Y ) ) -> Z e. _V )
16 15 rexlimivw 
 |-  ( E. k e. K E. l e. K Z = ( ( k .x. X ) .+ ( l .x. Y ) ) -> Z e. _V )
17 eqeq1 
 |-  ( v = Z -> ( v = ( ( k .x. X ) .+ ( l .x. Y ) ) <-> Z = ( ( k .x. X ) .+ ( l .x. Y ) ) ) )
18 17 2rexbidv 
 |-  ( v = Z -> ( E. k e. K E. l e. K v = ( ( k .x. X ) .+ ( l .x. Y ) ) <-> E. k e. K E. l e. K Z = ( ( k .x. X ) .+ ( l .x. Y ) ) ) )
19 16 18 elab3 
 |-  ( Z e. { v | E. k e. K E. l e. K v = ( ( k .x. X ) .+ ( l .x. Y ) ) } <-> E. k e. K E. l e. K Z = ( ( k .x. X ) .+ ( l .x. Y ) ) )
20 11 19 bitrdi 
 |-  ( ph -> ( Z e. ( N ` { X , Y } ) <-> E. k e. K E. l e. K Z = ( ( k .x. X ) .+ ( l .x. Y ) ) ) )