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

Metamath Proof Explorer

Theorem dvhopellsm

Description: Ordered pair membership in a subspace sum. (Contributed by NM, 12-Mar-2014)

Ref Expression
Hypotheses dvhopellsm.h 
|- H = ( LHyp ` K )
dvhopellsm.u 
|- U = ( ( DVecH ` K ) ` W )
dvhopellsm.a 
|- .+ = ( +g ` U )
dvhopellsm.s 
|- S = ( LSubSp ` U )
dvhopellsm.p 
|- .(+) = ( LSSum ` U )
Assertion dvhopellsm 
|- ( ( ( K e. HL /\ W e. H ) /\ X e. S /\ Y e. S ) -> ( <. F , T >. e. ( X .(+) Y ) <-> E. x E. y E. z E. w ( ( <. x , y >. e. X /\ <. z , w >. e. Y ) /\ <. F , T >. = ( <. x , y >. .+ <. z , w >. ) ) ) )

Proof

Step Hyp Ref Expression
1 dvhopellsm.h 
 |-  H = ( LHyp ` K )
2 dvhopellsm.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 dvhopellsm.a 
 |-  .+ = ( +g ` U )
4 dvhopellsm.s 
 |-  S = ( LSubSp ` U )
5 dvhopellsm.p 
 |-  .(+) = ( LSSum ` U )
6 id 
 |-  ( ( K e. HL /\ W e. H ) -> ( K e. HL /\ W e. H ) )
7 1 2 6 dvhlmod 
 |-  ( ( K e. HL /\ W e. H ) -> U e. LMod )
8 7 3ad2ant1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S /\ Y e. S ) -> U e. LMod )
9 4 lsssssubg 
 |-  ( U e. LMod -> S C_ ( SubGrp ` U ) )
10 8 9 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S /\ Y e. S ) -> S C_ ( SubGrp ` U ) )
11 simp2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S /\ Y e. S ) -> X e. S )
12 10 11 sseldd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S /\ Y e. S ) -> X e. ( SubGrp ` U ) )
13 simp3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S /\ Y e. S ) -> Y e. S )
14 10 13 sseldd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S /\ Y e. S ) -> Y e. ( SubGrp ` U ) )
15 3 5 lsmelval 
 |-  ( ( X e. ( SubGrp ` U ) /\ Y e. ( SubGrp ` U ) ) -> ( <. F , T >. e. ( X .(+) Y ) <-> E. u e. X E. v e. Y <. F , T >. = ( u .+ v ) ) )
16 12 14 15 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S /\ Y e. S ) -> ( <. F , T >. e. ( X .(+) Y ) <-> E. u e. X E. v e. Y <. F , T >. = ( u .+ v ) ) )
17 eqid 
 |-  ( Base ` U ) = ( Base ` U )
18 17 4 lssss 
 |-  ( Y e. S -> Y C_ ( Base ` U ) )
19 18 3ad2ant3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S /\ Y e. S ) -> Y C_ ( Base ` U ) )
20 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
21 eqid 
 |-  ( ( TEndo ` K ) ` W ) = ( ( TEndo ` K ) ` W )
22 1 20 21 2 17 dvhvbase 
 |-  ( ( K e. HL /\ W e. H ) -> ( Base ` U ) = ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) )
23 22 3ad2ant1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S /\ Y e. S ) -> ( Base ` U ) = ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) )
24 19 23 sseqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S /\ Y e. S ) -> Y C_ ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) )
25 relxp 
 |-  Rel ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) )
26 relss 
 |-  ( Y C_ ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) -> ( Rel ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) -> Rel Y ) )
27 24 25 26 mpisyl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S /\ Y e. S ) -> Rel Y )
28 oveq2 
 |-  ( v = <. z , w >. -> ( u .+ v ) = ( u .+ <. z , w >. ) )
29 28 eqeq2d 
 |-  ( v = <. z , w >. -> ( <. F , T >. = ( u .+ v ) <-> <. F , T >. = ( u .+ <. z , w >. ) ) )
30 29 exopxfr2 
 |-  ( Rel Y -> ( E. v e. Y <. F , T >. = ( u .+ v ) <-> E. z E. w ( <. z , w >. e. Y /\ <. F , T >. = ( u .+ <. z , w >. ) ) ) )
31 27 30 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S /\ Y e. S ) -> ( E. v e. Y <. F , T >. = ( u .+ v ) <-> E. z E. w ( <. z , w >. e. Y /\ <. F , T >. = ( u .+ <. z , w >. ) ) ) )
32 31 rexbidv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S /\ Y e. S ) -> ( E. u e. X E. v e. Y <. F , T >. = ( u .+ v ) <-> E. u e. X E. z E. w ( <. z , w >. e. Y /\ <. F , T >. = ( u .+ <. z , w >. ) ) ) )
33 17 4 lssss 
 |-  ( X e. S -> X C_ ( Base ` U ) )
34 33 3ad2ant2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S /\ Y e. S ) -> X C_ ( Base ` U ) )
35 34 23 sseqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S /\ Y e. S ) -> X C_ ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) )
36 relss 
 |-  ( X C_ ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) -> ( Rel ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) -> Rel X ) )
37 35 25 36 mpisyl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S /\ Y e. S ) -> Rel X )
38 oveq1 
 |-  ( u = <. x , y >. -> ( u .+ <. z , w >. ) = ( <. x , y >. .+ <. z , w >. ) )
39 38 eqeq2d 
 |-  ( u = <. x , y >. -> ( <. F , T >. = ( u .+ <. z , w >. ) <-> <. F , T >. = ( <. x , y >. .+ <. z , w >. ) ) )
40 39 anbi2d 
 |-  ( u = <. x , y >. -> ( ( <. z , w >. e. Y /\ <. F , T >. = ( u .+ <. z , w >. ) ) <-> ( <. z , w >. e. Y /\ <. F , T >. = ( <. x , y >. .+ <. z , w >. ) ) ) )
41 40 2exbidv 
 |-  ( u = <. x , y >. -> ( E. z E. w ( <. z , w >. e. Y /\ <. F , T >. = ( u .+ <. z , w >. ) ) <-> E. z E. w ( <. z , w >. e. Y /\ <. F , T >. = ( <. x , y >. .+ <. z , w >. ) ) ) )
42 41 exopxfr2 
 |-  ( Rel X -> ( E. u e. X E. z E. w ( <. z , w >. e. Y /\ <. F , T >. = ( u .+ <. z , w >. ) ) <-> E. x E. y ( <. x , y >. e. X /\ E. z E. w ( <. z , w >. e. Y /\ <. F , T >. = ( <. x , y >. .+ <. z , w >. ) ) ) ) )
43 37 42 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S /\ Y e. S ) -> ( E. u e. X E. z E. w ( <. z , w >. e. Y /\ <. F , T >. = ( u .+ <. z , w >. ) ) <-> E. x E. y ( <. x , y >. e. X /\ E. z E. w ( <. z , w >. e. Y /\ <. F , T >. = ( <. x , y >. .+ <. z , w >. ) ) ) ) )
44 19.42vv 
 |-  ( E. z E. w ( <. x , y >. e. X /\ ( <. z , w >. e. Y /\ <. F , T >. = ( <. x , y >. .+ <. z , w >. ) ) ) <-> ( <. x , y >. e. X /\ E. z E. w ( <. z , w >. e. Y /\ <. F , T >. = ( <. x , y >. .+ <. z , w >. ) ) ) )
45 anass 
 |-  ( ( ( <. x , y >. e. X /\ <. z , w >. e. Y ) /\ <. F , T >. = ( <. x , y >. .+ <. z , w >. ) ) <-> ( <. x , y >. e. X /\ ( <. z , w >. e. Y /\ <. F , T >. = ( <. x , y >. .+ <. z , w >. ) ) ) )
46 45 2exbii 
 |-  ( E. z E. w ( ( <. x , y >. e. X /\ <. z , w >. e. Y ) /\ <. F , T >. = ( <. x , y >. .+ <. z , w >. ) ) <-> E. z E. w ( <. x , y >. e. X /\ ( <. z , w >. e. Y /\ <. F , T >. = ( <. x , y >. .+ <. z , w >. ) ) ) )
47 46 bicomi 
 |-  ( E. z E. w ( <. x , y >. e. X /\ ( <. z , w >. e. Y /\ <. F , T >. = ( <. x , y >. .+ <. z , w >. ) ) ) <-> E. z E. w ( ( <. x , y >. e. X /\ <. z , w >. e. Y ) /\ <. F , T >. = ( <. x , y >. .+ <. z , w >. ) ) )
48 47 a1i 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S /\ Y e. S ) -> ( E. z E. w ( <. x , y >. e. X /\ ( <. z , w >. e. Y /\ <. F , T >. = ( <. x , y >. .+ <. z , w >. ) ) ) <-> E. z E. w ( ( <. x , y >. e. X /\ <. z , w >. e. Y ) /\ <. F , T >. = ( <. x , y >. .+ <. z , w >. ) ) ) )
49 44 48 bitr3id 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S /\ Y e. S ) -> ( ( <. x , y >. e. X /\ E. z E. w ( <. z , w >. e. Y /\ <. F , T >. = ( <. x , y >. .+ <. z , w >. ) ) ) <-> E. z E. w ( ( <. x , y >. e. X /\ <. z , w >. e. Y ) /\ <. F , T >. = ( <. x , y >. .+ <. z , w >. ) ) ) )
50 49 2exbidv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S /\ Y e. S ) -> ( E. x E. y ( <. x , y >. e. X /\ E. z E. w ( <. z , w >. e. Y /\ <. F , T >. = ( <. x , y >. .+ <. z , w >. ) ) ) <-> E. x E. y E. z E. w ( ( <. x , y >. e. X /\ <. z , w >. e. Y ) /\ <. F , T >. = ( <. x , y >. .+ <. z , w >. ) ) ) )
51 43 50 bitrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S /\ Y e. S ) -> ( E. u e. X E. z E. w ( <. z , w >. e. Y /\ <. F , T >. = ( u .+ <. z , w >. ) ) <-> E. x E. y E. z E. w ( ( <. x , y >. e. X /\ <. z , w >. e. Y ) /\ <. F , T >. = ( <. x , y >. .+ <. z , w >. ) ) ) )
52 16 32 51 3bitrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. S /\ Y e. S ) -> ( <. F , T >. e. ( X .(+) Y ) <-> E. x E. y E. z E. w ( ( <. x , y >. e. X /\ <. z , w >. e. Y ) /\ <. F , T >. = ( <. x , y >. .+ <. z , w >. ) ) ) )