Metamath Proof Explorer

Theorem diblsmopel

Description: Membership in subspace sum for partial isomorphism B. (Contributed by NM, 21-Sep-2014) (Revised by Mario Carneiro, 6-May-2015)

Ref Expression
Hypotheses diblsmopel.b 
|- B = ( Base ` K )
diblsmopel.l 
|- .<_ = ( le ` K )
diblsmopel.h 
|- H = ( LHyp ` K )
diblsmopel.t 
|- T = ( ( LTrn ` K ) ` W )
diblsmopel.o 
|- O = ( f e. T |-> ( _I |` B ) )
diblsmopel.v 
|- V = ( ( DVecA ` K ) ` W )
diblsmopel.u 
|- U = ( ( DVecH ` K ) ` W )
diblsmopel.q 
|- .(+) = ( LSSum ` V )
diblsmopel.p 
|- .+b = ( LSSum ` U )
diblsmopel.j 
|- J = ( ( DIsoA ` K ) ` W )
diblsmopel.i 
|- I = ( ( DIsoB ` K ) ` W )
diblsmopel.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
diblsmopel.x 
|- ( ph -> ( X e. B /\ X .<_ W ) )
diblsmopel.y 
|- ( ph -> ( Y e. B /\ Y .<_ W ) )
Assertion diblsmopel 
|- ( ph -> ( <. F , S >. e. ( ( I ` X ) .+b ( I ` Y ) ) <-> ( F e. ( ( J ` X ) .(+) ( J ` Y ) ) /\ S = O ) ) )

Proof

Step Hyp Ref Expression
1 diblsmopel.b 
 |-  B = ( Base ` K )
2 diblsmopel.l 
 |-  .<_ = ( le ` K )
3 diblsmopel.h 
 |-  H = ( LHyp ` K )
4 diblsmopel.t 
 |-  T = ( ( LTrn ` K ) ` W )
5 diblsmopel.o 
 |-  O = ( f e. T |-> ( _I |` B ) )
6 diblsmopel.v 
 |-  V = ( ( DVecA ` K ) ` W )
7 diblsmopel.u 
 |-  U = ( ( DVecH ` K ) ` W )
8 diblsmopel.q 
 |-  .(+) = ( LSSum ` V )
9 diblsmopel.p 
 |-  .+b = ( LSSum ` U )
10 diblsmopel.j 
 |-  J = ( ( DIsoA ` K ) ` W )
11 diblsmopel.i 
 |-  I = ( ( DIsoB ` K ) ` W )
12 diblsmopel.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
13 diblsmopel.x 
 |-  ( ph -> ( X e. B /\ X .<_ W ) )
14 diblsmopel.y 
 |-  ( ph -> ( Y e. B /\ Y .<_ W ) )
15 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
16 1 2 3 7 11 15 diblss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) e. ( LSubSp ` U ) )
17 12 13 16 syl2anc 
 |-  ( ph -> ( I ` X ) e. ( LSubSp ` U ) )
18 1 2 3 7 11 15 diblss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( I ` Y ) e. ( LSubSp ` U ) )
19 12 14 18 syl2anc 
 |-  ( ph -> ( I ` Y ) e. ( LSubSp ` U ) )
20 eqid 
 |-  ( +g ` U ) = ( +g ` U )
21 3 7 20 15 9 dvhopellsm 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( I ` X ) e. ( LSubSp ` U ) /\ ( I ` Y ) e. ( LSubSp ` U ) ) -> ( <. F , S >. e. ( ( I ` X ) .+b ( I ` Y ) ) <-> E. x E. y E. z E. w ( ( <. x , y >. e. ( I ` X ) /\ <. z , w >. e. ( I ` Y ) ) /\ <. F , S >. = ( <. x , y >. ( +g ` U ) <. z , w >. ) ) ) )
22 12 17 19 21 syl3anc 
 |-  ( ph -> ( <. F , S >. e. ( ( I ` X ) .+b ( I ` Y ) ) <-> E. x E. y E. z E. w ( ( <. x , y >. e. ( I ` X ) /\ <. z , w >. e. ( I ` Y ) ) /\ <. F , S >. = ( <. x , y >. ( +g ` U ) <. z , w >. ) ) ) )
23 excom 
 |-  ( E. y E. z E. w ( ( <. x , y >. e. ( I ` X ) /\ <. z , w >. e. ( I ` Y ) ) /\ <. F , S >. = ( <. x , y >. ( +g ` U ) <. z , w >. ) ) <-> E. z E. y E. w ( ( <. x , y >. e. ( I ` X ) /\ <. z , w >. e. ( I ` Y ) ) /\ <. F , S >. = ( <. x , y >. ( +g ` U ) <. z , w >. ) ) )
24 1 2 3 4 5 10 11 dibopelval2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( <. x , y >. e. ( I ` X ) <-> ( x e. ( J ` X ) /\ y = O ) ) )
25 12 13 24 syl2anc 
 |-  ( ph -> ( <. x , y >. e. ( I ` X ) <-> ( x e. ( J ` X ) /\ y = O ) ) )
26 1 2 3 4 5 10 11 dibopelval2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( <. z , w >. e. ( I ` Y ) <-> ( z e. ( J ` Y ) /\ w = O ) ) )
27 12 14 26 syl2anc 
 |-  ( ph -> ( <. z , w >. e. ( I ` Y ) <-> ( z e. ( J ` Y ) /\ w = O ) ) )
28 25 27 anbi12d 
 |-  ( ph -> ( ( <. x , y >. e. ( I ` X ) /\ <. z , w >. e. ( I ` Y ) ) <-> ( ( x e. ( J ` X ) /\ y = O ) /\ ( z e. ( J ` Y ) /\ w = O ) ) ) )
29 an4 
 |-  ( ( ( x e. ( J ` X ) /\ y = O ) /\ ( z e. ( J ` Y ) /\ w = O ) ) <-> ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ ( y = O /\ w = O ) ) )
30 ancom 
 |-  ( ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ ( y = O /\ w = O ) ) <-> ( ( y = O /\ w = O ) /\ ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) ) )
31 29 30 bitri 
 |-  ( ( ( x e. ( J ` X ) /\ y = O ) /\ ( z e. ( J ` Y ) /\ w = O ) ) <-> ( ( y = O /\ w = O ) /\ ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) ) )
32 28 31 bitrdi 
 |-  ( ph -> ( ( <. x , y >. e. ( I ` X ) /\ <. z , w >. e. ( I ` Y ) ) <-> ( ( y = O /\ w = O ) /\ ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) ) ) )
33 32 anbi1d 
 |-  ( ph -> ( ( ( <. x , y >. e. ( I ` X ) /\ <. z , w >. e. ( I ` Y ) ) /\ <. F , S >. = ( <. x , y >. ( +g ` U ) <. z , w >. ) ) <-> ( ( ( y = O /\ w = O ) /\ ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) ) /\ <. F , S >. = ( <. x , y >. ( +g ` U ) <. z , w >. ) ) ) )
34 anass 
 |-  ( ( ( ( y = O /\ w = O ) /\ ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) ) /\ <. F , S >. = ( <. x , y >. ( +g ` U ) <. z , w >. ) ) <-> ( ( y = O /\ w = O ) /\ ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ <. F , S >. = ( <. x , y >. ( +g ` U ) <. z , w >. ) ) ) )
35 df-3an 
 |-  ( ( y = O /\ w = O /\ ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ <. F , S >. = ( <. x , y >. ( +g ` U ) <. z , w >. ) ) ) <-> ( ( y = O /\ w = O ) /\ ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ <. F , S >. = ( <. x , y >. ( +g ` U ) <. z , w >. ) ) ) )
36 34 35 bitr4i 
 |-  ( ( ( ( y = O /\ w = O ) /\ ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) ) /\ <. F , S >. = ( <. x , y >. ( +g ` U ) <. z , w >. ) ) <-> ( y = O /\ w = O /\ ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ <. F , S >. = ( <. x , y >. ( +g ` U ) <. z , w >. ) ) ) )
37 33 36 bitrdi 
 |-  ( ph -> ( ( ( <. x , y >. e. ( I ` X ) /\ <. z , w >. e. ( I ` Y ) ) /\ <. F , S >. = ( <. x , y >. ( +g ` U ) <. z , w >. ) ) <-> ( y = O /\ w = O /\ ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ <. F , S >. = ( <. x , y >. ( +g ` U ) <. z , w >. ) ) ) ) )
38 37 2exbidv 
 |-  ( ph -> ( E. y E. w ( ( <. x , y >. e. ( I ` X ) /\ <. z , w >. e. ( I ` Y ) ) /\ <. F , S >. = ( <. x , y >. ( +g ` U ) <. z , w >. ) ) <-> E. y E. w ( y = O /\ w = O /\ ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ <. F , S >. = ( <. x , y >. ( +g ` U ) <. z , w >. ) ) ) ) )
39 4 fvexi 
 |-  T e. _V
40 39 mptex 
 |-  ( f e. T |-> ( _I |` B ) ) e. _V
41 5 40 eqeltri 
 |-  O e. _V
42 opeq2 
 |-  ( y = O -> <. x , y >. = <. x , O >. )
43 42 oveq1d 
 |-  ( y = O -> ( <. x , y >. ( +g ` U ) <. z , w >. ) = ( <. x , O >. ( +g ` U ) <. z , w >. ) )
44 43 eqeq2d 
 |-  ( y = O -> ( <. F , S >. = ( <. x , y >. ( +g ` U ) <. z , w >. ) <-> <. F , S >. = ( <. x , O >. ( +g ` U ) <. z , w >. ) ) )
45 44 anbi2d 
 |-  ( y = O -> ( ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ <. F , S >. = ( <. x , y >. ( +g ` U ) <. z , w >. ) ) <-> ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ <. F , S >. = ( <. x , O >. ( +g ` U ) <. z , w >. ) ) ) )
46 opeq2 
 |-  ( w = O -> <. z , w >. = <. z , O >. )
47 46 oveq2d 
 |-  ( w = O -> ( <. x , O >. ( +g ` U ) <. z , w >. ) = ( <. x , O >. ( +g ` U ) <. z , O >. ) )
48 47 eqeq2d 
 |-  ( w = O -> ( <. F , S >. = ( <. x , O >. ( +g ` U ) <. z , w >. ) <-> <. F , S >. = ( <. x , O >. ( +g ` U ) <. z , O >. ) ) )
49 48 anbi2d 
 |-  ( w = O -> ( ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ <. F , S >. = ( <. x , O >. ( +g ` U ) <. z , w >. ) ) <-> ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ <. F , S >. = ( <. x , O >. ( +g ` U ) <. z , O >. ) ) ) )
50 41 41 45 49 ceqsex2v 
 |-  ( E. y E. w ( y = O /\ w = O /\ ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ <. F , S >. = ( <. x , y >. ( +g ` U ) <. z , w >. ) ) ) <-> ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ <. F , S >. = ( <. x , O >. ( +g ` U ) <. z , O >. ) ) )
51 12 adantr 
 |-  ( ( ph /\ ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) ) -> ( K e. HL /\ W e. H ) )
52 13 adantr 
 |-  ( ( ph /\ ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) ) -> ( X e. B /\ X .<_ W ) )
53 simprl 
 |-  ( ( ph /\ ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) ) -> x e. ( J ` X ) )
54 1 2 3 4 10 diael 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ x e. ( J ` X ) ) -> x e. T )
55 51 52 53 54 syl3anc 
 |-  ( ( ph /\ ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) ) -> x e. T )
56 eqid 
 |-  ( ( TEndo ` K ) ` W ) = ( ( TEndo ` K ) ` W )
57 1 3 4 56 5 tendo0cl 
 |-  ( ( K e. HL /\ W e. H ) -> O e. ( ( TEndo ` K ) ` W ) )
58 51 57 syl 
 |-  ( ( ph /\ ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) ) -> O e. ( ( TEndo ` K ) ` W ) )
59 14 adantr 
 |-  ( ( ph /\ ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) ) -> ( Y e. B /\ Y .<_ W ) )
60 simprr 
 |-  ( ( ph /\ ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) ) -> z e. ( J ` Y ) )
61 1 2 3 4 10 diael 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Y e. B /\ Y .<_ W ) /\ z e. ( J ` Y ) ) -> z e. T )
62 51 59 60 61 syl3anc 
 |-  ( ( ph /\ ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) ) -> z e. T )
63 eqid 
 |-  ( Scalar ` U ) = ( Scalar ` U )
64 eqid 
 |-  ( +g ` ( Scalar ` U ) ) = ( +g ` ( Scalar ` U ) )
65 3 4 56 7 63 20 64 dvhopvadd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x e. T /\ O e. ( ( TEndo ` K ) ` W ) ) /\ ( z e. T /\ O e. ( ( TEndo ` K ) ` W ) ) ) -> ( <. x , O >. ( +g ` U ) <. z , O >. ) = <. ( x o. z ) , ( O ( +g ` ( Scalar ` U ) ) O ) >. )
66 51 55 58 62 58 65 syl122anc 
 |-  ( ( ph /\ ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) ) -> ( <. x , O >. ( +g ` U ) <. z , O >. ) = <. ( x o. z ) , ( O ( +g ` ( Scalar ` U ) ) O ) >. )
67 66 eqeq2d 
 |-  ( ( ph /\ ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) ) -> ( <. F , S >. = ( <. x , O >. ( +g ` U ) <. z , O >. ) <-> <. F , S >. = <. ( x o. z ) , ( O ( +g ` ( Scalar ` U ) ) O ) >. ) )
68 vex 
 |-  x e. _V
69 vex 
 |-  z e. _V
70 68 69 coex 
 |-  ( x o. z ) e. _V
71 ovex 
 |-  ( O ( +g ` ( Scalar ` U ) ) O ) e. _V
72 70 71 opth2 
 |-  ( <. F , S >. = <. ( x o. z ) , ( O ( +g ` ( Scalar ` U ) ) O ) >. <-> ( F = ( x o. z ) /\ S = ( O ( +g ` ( Scalar ` U ) ) O ) ) )
73 eqid 
 |-  ( +g ` V ) = ( +g ` V )
74 3 4 6 73 dvavadd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x e. T /\ z e. T ) ) -> ( x ( +g ` V ) z ) = ( x o. z ) )
75 51 55 62 74 syl12anc 
 |-  ( ( ph /\ ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) ) -> ( x ( +g ` V ) z ) = ( x o. z ) )
76 75 eqeq2d 
 |-  ( ( ph /\ ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) ) -> ( F = ( x ( +g ` V ) z ) <-> F = ( x o. z ) ) )
77 76 bicomd 
 |-  ( ( ph /\ ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) ) -> ( F = ( x o. z ) <-> F = ( x ( +g ` V ) z ) ) )
78 eqid 
 |-  ( s e. ( ( TEndo ` K ) ` W ) , t e. ( ( TEndo ` K ) ` W ) |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) ) = ( s e. ( ( TEndo ` K ) ` W ) , t e. ( ( TEndo ` K ) ` W ) |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) )
79 3 4 56 7 63 78 64 dvhfplusr 
 |-  ( ( K e. HL /\ W e. H ) -> ( +g ` ( Scalar ` U ) ) = ( s e. ( ( TEndo ` K ) ` W ) , t e. ( ( TEndo ` K ) ` W ) |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) ) )
80 51 79 syl 
 |-  ( ( ph /\ ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) ) -> ( +g ` ( Scalar ` U ) ) = ( s e. ( ( TEndo ` K ) ` W ) , t e. ( ( TEndo ` K ) ` W ) |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) ) )
81 80 oveqd 
 |-  ( ( ph /\ ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) ) -> ( O ( +g ` ( Scalar ` U ) ) O ) = ( O ( s e. ( ( TEndo ` K ) ` W ) , t e. ( ( TEndo ` K ) ` W ) |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) ) O ) )
82 1 3 4 56 5 78 tendo0pl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ O e. ( ( TEndo ` K ) ` W ) ) -> ( O ( s e. ( ( TEndo ` K ) ` W ) , t e. ( ( TEndo ` K ) ` W ) |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) ) O ) = O )
83 51 58 82 syl2anc 
 |-  ( ( ph /\ ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) ) -> ( O ( s e. ( ( TEndo ` K ) ` W ) , t e. ( ( TEndo ` K ) ` W ) |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) ) O ) = O )
84 81 83 eqtrd 
 |-  ( ( ph /\ ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) ) -> ( O ( +g ` ( Scalar ` U ) ) O ) = O )
85 84 eqeq2d 
 |-  ( ( ph /\ ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) ) -> ( S = ( O ( +g ` ( Scalar ` U ) ) O ) <-> S = O ) )
86 77 85 anbi12d 
 |-  ( ( ph /\ ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) ) -> ( ( F = ( x o. z ) /\ S = ( O ( +g ` ( Scalar ` U ) ) O ) ) <-> ( F = ( x ( +g ` V ) z ) /\ S = O ) ) )
87 72 86 bitrid 
 |-  ( ( ph /\ ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) ) -> ( <. F , S >. = <. ( x o. z ) , ( O ( +g ` ( Scalar ` U ) ) O ) >. <-> ( F = ( x ( +g ` V ) z ) /\ S = O ) ) )
88 67 87 bitrd 
 |-  ( ( ph /\ ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) ) -> ( <. F , S >. = ( <. x , O >. ( +g ` U ) <. z , O >. ) <-> ( F = ( x ( +g ` V ) z ) /\ S = O ) ) )
89 88 pm5.32da 
 |-  ( ph -> ( ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ <. F , S >. = ( <. x , O >. ( +g ` U ) <. z , O >. ) ) <-> ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ ( F = ( x ( +g ` V ) z ) /\ S = O ) ) ) )
90 50 89 bitrid 
 |-  ( ph -> ( E. y E. w ( y = O /\ w = O /\ ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ <. F , S >. = ( <. x , y >. ( +g ` U ) <. z , w >. ) ) ) <-> ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ ( F = ( x ( +g ` V ) z ) /\ S = O ) ) ) )
91 38 90 bitrd 
 |-  ( ph -> ( E. y E. w ( ( <. x , y >. e. ( I ` X ) /\ <. z , w >. e. ( I ` Y ) ) /\ <. F , S >. = ( <. x , y >. ( +g ` U ) <. z , w >. ) ) <-> ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ ( F = ( x ( +g ` V ) z ) /\ S = O ) ) ) )
92 91 exbidv 
 |-  ( ph -> ( E. z E. y E. w ( ( <. x , y >. e. ( I ` X ) /\ <. z , w >. e. ( I ` Y ) ) /\ <. F , S >. = ( <. x , y >. ( +g ` U ) <. z , w >. ) ) <-> E. z ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ ( F = ( x ( +g ` V ) z ) /\ S = O ) ) ) )
93 23 92 bitrid 
 |-  ( ph -> ( E. y E. z E. w ( ( <. x , y >. e. ( I ` X ) /\ <. z , w >. e. ( I ` Y ) ) /\ <. F , S >. = ( <. x , y >. ( +g ` U ) <. z , w >. ) ) <-> E. z ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ ( F = ( x ( +g ` V ) z ) /\ S = O ) ) ) )
94 93 exbidv 
 |-  ( ph -> ( E. x E. y E. z E. w ( ( <. x , y >. e. ( I ` X ) /\ <. z , w >. e. ( I ` Y ) ) /\ <. F , S >. = ( <. x , y >. ( +g ` U ) <. z , w >. ) ) <-> E. x E. z ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ ( F = ( x ( +g ` V ) z ) /\ S = O ) ) ) )
95 anass 
 |-  ( ( ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ F = ( x ( +g ` V ) z ) ) /\ S = O ) <-> ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ ( F = ( x ( +g ` V ) z ) /\ S = O ) ) )
96 95 bicomi 
 |-  ( ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ ( F = ( x ( +g ` V ) z ) /\ S = O ) ) <-> ( ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ F = ( x ( +g ` V ) z ) ) /\ S = O ) )
97 96 2exbii 
 |-  ( E. x E. z ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ ( F = ( x ( +g ` V ) z ) /\ S = O ) ) <-> E. x E. z ( ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ F = ( x ( +g ` V ) z ) ) /\ S = O ) )
98 19.41vv 
 |-  ( E. x E. z ( ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ F = ( x ( +g ` V ) z ) ) /\ S = O ) <-> ( E. x E. z ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ F = ( x ( +g ` V ) z ) ) /\ S = O ) )
99 97 98 bitri 
 |-  ( E. x E. z ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ ( F = ( x ( +g ` V ) z ) /\ S = O ) ) <-> ( E. x E. z ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ F = ( x ( +g ` V ) z ) ) /\ S = O ) )
100 3 6 dvalvec 
 |-  ( ( K e. HL /\ W e. H ) -> V e. LVec )
101 lveclmod 
 |-  ( V e. LVec -> V e. LMod )
102 eqid 
 |-  ( LSubSp ` V ) = ( LSubSp ` V )
103 102 lsssssubg 
 |-  ( V e. LMod -> ( LSubSp ` V ) C_ ( SubGrp ` V ) )
104 12 100 101 103 4syl 
 |-  ( ph -> ( LSubSp ` V ) C_ ( SubGrp ` V ) )
105 1 2 3 6 10 102 dialss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( J ` X ) e. ( LSubSp ` V ) )
106 12 13 105 syl2anc 
 |-  ( ph -> ( J ` X ) e. ( LSubSp ` V ) )
107 104 106 sseldd 
 |-  ( ph -> ( J ` X ) e. ( SubGrp ` V ) )
108 1 2 3 6 10 102 dialss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( J ` Y ) e. ( LSubSp ` V ) )
109 12 14 108 syl2anc 
 |-  ( ph -> ( J ` Y ) e. ( LSubSp ` V ) )
110 104 109 sseldd 
 |-  ( ph -> ( J ` Y ) e. ( SubGrp ` V ) )
111 73 8 lsmelval 
 |-  ( ( ( J ` X ) e. ( SubGrp ` V ) /\ ( J ` Y ) e. ( SubGrp ` V ) ) -> ( F e. ( ( J ` X ) .(+) ( J ` Y ) ) <-> E. x e. ( J ` X ) E. z e. ( J ` Y ) F = ( x ( +g ` V ) z ) ) )
112 107 110 111 syl2anc 
 |-  ( ph -> ( F e. ( ( J ` X ) .(+) ( J ` Y ) ) <-> E. x e. ( J ` X ) E. z e. ( J ` Y ) F = ( x ( +g ` V ) z ) ) )
113 r2ex 
 |-  ( E. x e. ( J ` X ) E. z e. ( J ` Y ) F = ( x ( +g ` V ) z ) <-> E. x E. z ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ F = ( x ( +g ` V ) z ) ) )
114 112 113 bitrdi 
 |-  ( ph -> ( F e. ( ( J ` X ) .(+) ( J ` Y ) ) <-> E. x E. z ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ F = ( x ( +g ` V ) z ) ) ) )
115 114 anbi1d 
 |-  ( ph -> ( ( F e. ( ( J ` X ) .(+) ( J ` Y ) ) /\ S = O ) <-> ( E. x E. z ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ F = ( x ( +g ` V ) z ) ) /\ S = O ) ) )
116 115 bicomd 
 |-  ( ph -> ( ( E. x E. z ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ F = ( x ( +g ` V ) z ) ) /\ S = O ) <-> ( F e. ( ( J ` X ) .(+) ( J ` Y ) ) /\ S = O ) ) )
117 99 116 bitrid 
 |-  ( ph -> ( E. x E. z ( ( x e. ( J ` X ) /\ z e. ( J ` Y ) ) /\ ( F = ( x ( +g ` V ) z ) /\ S = O ) ) <-> ( F e. ( ( J ` X ) .(+) ( J ` Y ) ) /\ S = O ) ) )
118 22 94 117 3bitrd 
 |-  ( ph -> ( <. F , S >. e. ( ( I ` X ) .+b ( I ` Y ) ) <-> ( F e. ( ( J ` X ) .(+) ( J ` Y ) ) /\ S = O ) ) )