Metamath Proof Explorer

Theorem dihopellsm

Description: Ordered pair membership in a subspace sum of isomorphism H values. (Contributed by NM, 26-Sep-2014)

Ref Expression
Hypotheses dihopellsm.b 
|- B = ( Base ` K )
dihopellsm.h 
|- H = ( LHyp ` K )
dihopellsm.t 
|- T = ( ( LTrn ` K ) ` W )
dihopellsm.e 
|- E = ( ( TEndo ` K ) ` W )
dihopellsm.a 
|- A = ( v e. E , w e. E |-> ( i e. T |-> ( ( v ` i ) o. ( w ` i ) ) ) )
dihopellsm.u 
|- U = ( ( DVecH ` K ) ` W )
dihopellsm.l 
|- L = ( LSubSp ` U )
dihopellsm.p 
|- .(+) = ( LSSum ` U )
dihopellsm.i 
|- I = ( ( DIsoH ` K ) ` W )
dihopellsm.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
dihopellsm.x 
|- ( ph -> X e. B )
dihopellsm.y 
|- ( ph -> Y e. B )
Assertion dihopellsm 
|- ( ph -> ( <. F , S >. e. ( ( I ` X ) .(+) ( I ` Y ) ) <-> E. g E. t E. h E. u ( ( <. g , t >. e. ( I ` X ) /\ <. h , u >. e. ( I ` Y ) ) /\ ( F = ( g o. h ) /\ S = ( t A u ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dihopellsm.b 
 |-  B = ( Base ` K )
2 dihopellsm.h 
 |-  H = ( LHyp ` K )
3 dihopellsm.t 
 |-  T = ( ( LTrn ` K ) ` W )
4 dihopellsm.e 
 |-  E = ( ( TEndo ` K ) ` W )
5 dihopellsm.a 
 |-  A = ( v e. E , w e. E |-> ( i e. T |-> ( ( v ` i ) o. ( w ` i ) ) ) )
6 dihopellsm.u 
 |-  U = ( ( DVecH ` K ) ` W )
7 dihopellsm.l 
 |-  L = ( LSubSp ` U )
8 dihopellsm.p 
 |-  .(+) = ( LSSum ` U )
9 dihopellsm.i 
 |-  I = ( ( DIsoH ` K ) ` W )
10 dihopellsm.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
11 dihopellsm.x 
 |-  ( ph -> X e. B )
12 dihopellsm.y 
 |-  ( ph -> Y e. B )
13 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
14 1 2 9 6 13 dihlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. B ) -> ( I ` X ) e. ( LSubSp ` U ) )
15 10 11 14 syl2anc 
 |-  ( ph -> ( I ` X ) e. ( LSubSp ` U ) )
16 1 2 9 6 13 dihlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y e. B ) -> ( I ` Y ) e. ( LSubSp ` U ) )
17 10 12 16 syl2anc 
 |-  ( ph -> ( I ` Y ) e. ( LSubSp ` U ) )
18 eqid 
 |-  ( +g ` U ) = ( +g ` U )
19 2 6 18 13 8 dvhopellsm 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( I ` X ) e. ( LSubSp ` U ) /\ ( I ` Y ) e. ( LSubSp ` U ) ) -> ( <. F , S >. e. ( ( I ` X ) .(+) ( I ` Y ) ) <-> E. g E. t E. h E. u ( ( <. g , t >. e. ( I ` X ) /\ <. h , u >. e. ( I ` Y ) ) /\ <. F , S >. = ( <. g , t >. ( +g ` U ) <. h , u >. ) ) ) )
20 10 15 17 19 syl3anc 
 |-  ( ph -> ( <. F , S >. e. ( ( I ` X ) .(+) ( I ` Y ) ) <-> E. g E. t E. h E. u ( ( <. g , t >. e. ( I ` X ) /\ <. h , u >. e. ( I ` Y ) ) /\ <. F , S >. = ( <. g , t >. ( +g ` U ) <. h , u >. ) ) ) )
21 10 adantr 
 |-  ( ( ph /\ <. g , t >. e. ( I ` X ) ) -> ( K e. HL /\ W e. H ) )
22 11 adantr 
 |-  ( ( ph /\ <. g , t >. e. ( I ` X ) ) -> X e. B )
23 simpr 
 |-  ( ( ph /\ <. g , t >. e. ( I ` X ) ) -> <. g , t >. e. ( I ` X ) )
24 1 2 3 4 9 21 22 23 dihopcl 
 |-  ( ( ph /\ <. g , t >. e. ( I ` X ) ) -> ( g e. T /\ t e. E ) )
25 10 adantr 
 |-  ( ( ph /\ <. h , u >. e. ( I ` Y ) ) -> ( K e. HL /\ W e. H ) )
26 12 adantr 
 |-  ( ( ph /\ <. h , u >. e. ( I ` Y ) ) -> Y e. B )
27 simpr 
 |-  ( ( ph /\ <. h , u >. e. ( I ` Y ) ) -> <. h , u >. e. ( I ` Y ) )
28 1 2 3 4 9 25 26 27 dihopcl 
 |-  ( ( ph /\ <. h , u >. e. ( I ` Y ) ) -> ( h e. T /\ u e. E ) )
29 24 28 anim12dan 
 |-  ( ( ph /\ ( <. g , t >. e. ( I ` X ) /\ <. h , u >. e. ( I ` Y ) ) ) -> ( ( g e. T /\ t e. E ) /\ ( h e. T /\ u e. E ) ) )
30 10 adantr 
 |-  ( ( ph /\ ( ( g e. T /\ t e. E ) /\ ( h e. T /\ u e. E ) ) ) -> ( K e. HL /\ W e. H ) )
31 simprl 
 |-  ( ( ph /\ ( ( g e. T /\ t e. E ) /\ ( h e. T /\ u e. E ) ) ) -> ( g e. T /\ t e. E ) )
32 simprr 
 |-  ( ( ph /\ ( ( g e. T /\ t e. E ) /\ ( h e. T /\ u e. E ) ) ) -> ( h e. T /\ u e. E ) )
33 2 3 4 5 6 18 dvhopvadd2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( g e. T /\ t e. E ) /\ ( h e. T /\ u e. E ) ) -> ( <. g , t >. ( +g ` U ) <. h , u >. ) = <. ( g o. h ) , ( t A u ) >. )
34 30 31 32 33 syl3anc 
 |-  ( ( ph /\ ( ( g e. T /\ t e. E ) /\ ( h e. T /\ u e. E ) ) ) -> ( <. g , t >. ( +g ` U ) <. h , u >. ) = <. ( g o. h ) , ( t A u ) >. )
35 34 eqeq2d 
 |-  ( ( ph /\ ( ( g e. T /\ t e. E ) /\ ( h e. T /\ u e. E ) ) ) -> ( <. F , S >. = ( <. g , t >. ( +g ` U ) <. h , u >. ) <-> <. F , S >. = <. ( g o. h ) , ( t A u ) >. ) )
36 vex 
 |-  g e. _V
37 vex 
 |-  h e. _V
38 36 37 coex 
 |-  ( g o. h ) e. _V
39 ovex 
 |-  ( t A u ) e. _V
40 38 39 opth2 
 |-  ( <. F , S >. = <. ( g o. h ) , ( t A u ) >. <-> ( F = ( g o. h ) /\ S = ( t A u ) ) )
41 35 40 bitrdi 
 |-  ( ( ph /\ ( ( g e. T /\ t e. E ) /\ ( h e. T /\ u e. E ) ) ) -> ( <. F , S >. = ( <. g , t >. ( +g ` U ) <. h , u >. ) <-> ( F = ( g o. h ) /\ S = ( t A u ) ) ) )
42 29 41 syldan 
 |-  ( ( ph /\ ( <. g , t >. e. ( I ` X ) /\ <. h , u >. e. ( I ` Y ) ) ) -> ( <. F , S >. = ( <. g , t >. ( +g ` U ) <. h , u >. ) <-> ( F = ( g o. h ) /\ S = ( t A u ) ) ) )
43 42 pm5.32da 
 |-  ( ph -> ( ( ( <. g , t >. e. ( I ` X ) /\ <. h , u >. e. ( I ` Y ) ) /\ <. F , S >. = ( <. g , t >. ( +g ` U ) <. h , u >. ) ) <-> ( ( <. g , t >. e. ( I ` X ) /\ <. h , u >. e. ( I ` Y ) ) /\ ( F = ( g o. h ) /\ S = ( t A u ) ) ) ) )
44 43 4exbidv 
 |-  ( ph -> ( E. g E. t E. h E. u ( ( <. g , t >. e. ( I ` X ) /\ <. h , u >. e. ( I ` Y ) ) /\ <. F , S >. = ( <. g , t >. ( +g ` U ) <. h , u >. ) ) <-> E. g E. t E. h E. u ( ( <. g , t >. e. ( I ` X ) /\ <. h , u >. e. ( I ` Y ) ) /\ ( F = ( g o. h ) /\ S = ( t A u ) ) ) ) )
45 20 44 bitrd 
 |-  ( ph -> ( <. F , S >. e. ( ( I ` X ) .(+) ( I ` Y ) ) <-> E. g E. t E. h E. u ( ( <. g , t >. e. ( I ` X ) /\ <. h , u >. e. ( I ` Y ) ) /\ ( F = ( g o. h ) /\ S = ( t A u ) ) ) ) )