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 ) ) ) ) )