Metamath Proof Explorer

Theorem dihjatcclem4

Description: Lemma for isomorphism H of lattice join of two atoms not under the fiducial hyperplane. (Contributed by NM, 29-Sep-2014)

Ref Expression
Hypotheses dihjatcclem.b 
|- B = ( Base ` K )
dihjatcclem.l 
|- .<_ = ( le ` K )
dihjatcclem.h 
|- H = ( LHyp ` K )
dihjatcclem.j 
|- .\/ = ( join ` K )
dihjatcclem.m 
|- ./\ = ( meet ` K )
dihjatcclem.a 
|- A = ( Atoms ` K )
dihjatcclem.u 
|- U = ( ( DVecH ` K ) ` W )
dihjatcclem.s 
|- .(+) = ( LSSum ` U )
dihjatcclem.i 
|- I = ( ( DIsoH ` K ) ` W )
dihjatcclem.v 
|- V = ( ( P .\/ Q ) ./\ W )
dihjatcclem.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
dihjatcclem.p 
|- ( ph -> ( P e. A /\ -. P .<_ W ) )
dihjatcclem.q 
|- ( ph -> ( Q e. A /\ -. Q .<_ W ) )
dihjatcc.w 
|- C = ( ( oc ` K ) ` W )
dihjatcc.t 
|- T = ( ( LTrn ` K ) ` W )
dihjatcc.r 
|- R = ( ( trL ` K ) ` W )
dihjatcc.e 
|- E = ( ( TEndo ` K ) ` W )
dihjatcc.g 
|- G = ( iota_ d e. T ( d ` C ) = P )
dihjatcc.dd 
|- D = ( iota_ d e. T ( d ` C ) = Q )
dihjatcc.n 
|- N = ( a e. E |-> ( d e. T |-> `' ( a ` d ) ) )
dihjatcc.o 
|- .0. = ( d e. T |-> ( _I |` B ) )
dihjatcc.d 
|- J = ( a e. E , b e. E |-> ( d e. T |-> ( ( a ` d ) o. ( b ` d ) ) ) )
Assertion dihjatcclem4 
|- ( ph -> ( I ` V ) C_ ( ( I ` P ) .(+) ( I ` Q ) ) )

Proof

Step Hyp Ref Expression
1 dihjatcclem.b 
 |-  B = ( Base ` K )
2 dihjatcclem.l 
 |-  .<_ = ( le ` K )
3 dihjatcclem.h 
 |-  H = ( LHyp ` K )
4 dihjatcclem.j 
 |-  .\/ = ( join ` K )
5 dihjatcclem.m 
 |-  ./\ = ( meet ` K )
6 dihjatcclem.a 
 |-  A = ( Atoms ` K )
7 dihjatcclem.u 
 |-  U = ( ( DVecH ` K ) ` W )
8 dihjatcclem.s 
 |-  .(+) = ( LSSum ` U )
9 dihjatcclem.i 
 |-  I = ( ( DIsoH ` K ) ` W )
10 dihjatcclem.v 
 |-  V = ( ( P .\/ Q ) ./\ W )
11 dihjatcclem.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
12 dihjatcclem.p 
 |-  ( ph -> ( P e. A /\ -. P .<_ W ) )
13 dihjatcclem.q 
 |-  ( ph -> ( Q e. A /\ -. Q .<_ W ) )
14 dihjatcc.w 
 |-  C = ( ( oc ` K ) ` W )
15 dihjatcc.t 
 |-  T = ( ( LTrn ` K ) ` W )
16 dihjatcc.r 
 |-  R = ( ( trL ` K ) ` W )
17 dihjatcc.e 
 |-  E = ( ( TEndo ` K ) ` W )
18 dihjatcc.g 
 |-  G = ( iota_ d e. T ( d ` C ) = P )
19 dihjatcc.dd 
 |-  D = ( iota_ d e. T ( d ` C ) = Q )
20 dihjatcc.n 
 |-  N = ( a e. E |-> ( d e. T |-> `' ( a ` d ) ) )
21 dihjatcc.o 
 |-  .0. = ( d e. T |-> ( _I |` B ) )
22 dihjatcc.d 
 |-  J = ( a e. E , b e. E |-> ( d e. T |-> ( ( a ` d ) o. ( b ` d ) ) ) )
23 3 9 dihvalrel 
 |-  ( ( K e. HL /\ W e. H ) -> Rel ( I ` V ) )
24 11 23 syl 
 |-  ( ph -> Rel ( I ` V ) )
25 11 adantr 
 |-  ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) -> ( K e. HL /\ W e. H ) )
26 2 6 3 14 lhpocnel2 
 |-  ( ( K e. HL /\ W e. H ) -> ( C e. A /\ -. C .<_ W ) )
27 11 26 syl 
 |-  ( ph -> ( C e. A /\ -. C .<_ W ) )
28 2 6 3 15 18 ltrniotacl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( C e. A /\ -. C .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) -> G e. T )
29 11 27 12 28 syl3anc 
 |-  ( ph -> G e. T )
30 2 6 3 15 19 ltrniotacl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( C e. A /\ -. C .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> D e. T )
31 11 27 13 30 syl3anc 
 |-  ( ph -> D e. T )
32 3 15 ltrncnv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ D e. T ) -> `' D e. T )
33 11 31 32 syl2anc 
 |-  ( ph -> `' D e. T )
34 3 15 ltrnco 
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ `' D e. T ) -> ( G o. `' D ) e. T )
35 11 29 33 34 syl3anc 
 |-  ( ph -> ( G o. `' D ) e. T )
36 35 adantr 
 |-  ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) -> ( G o. `' D ) e. T )
37 simprll 
 |-  ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) -> f e. T )
38 simprlr 
 |-  ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) -> ( R ` f ) .<_ V )
39 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 dihjatcclem3 
 |-  ( ph -> ( R ` ( G o. `' D ) ) = V )
40 39 adantr 
 |-  ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) -> ( R ` ( G o. `' D ) ) = V )
41 38 40 breqtrrd 
 |-  ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) -> ( R ` f ) .<_ ( R ` ( G o. `' D ) ) )
42 2 3 15 16 17 tendoex 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( G o. `' D ) e. T /\ f e. T ) /\ ( R ` f ) .<_ ( R ` ( G o. `' D ) ) ) -> E. t e. E ( t ` ( G o. `' D ) ) = f )
43 25 36 37 41 42 syl121anc 
 |-  ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) -> E. t e. E ( t ` ( G o. `' D ) ) = f )
44 df-rex 
 |-  ( E. t e. E ( t ` ( G o. `' D ) ) = f <-> E. t ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) )
45 43 44 sylib 
 |-  ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) -> E. t ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) )
46 eqidd 
 |-  ( ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) /\ ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) ) -> ( t ` G ) = ( t ` G ) )
47 simprl 
 |-  ( ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) /\ ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) ) -> t e. E )
48 11 ad2antrr 
 |-  ( ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) /\ ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) ) -> ( K e. HL /\ W e. H ) )
49 12 ad2antrr 
 |-  ( ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) /\ ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) ) -> ( P e. A /\ -. P .<_ W ) )
50 fvex 
 |-  ( t ` G ) e. _V
51 vex 
 |-  t e. _V
52 2 6 3 14 15 17 9 18 50 51 dihopelvalcqat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( <. ( t ` G ) , t >. e. ( I ` P ) <-> ( ( t ` G ) = ( t ` G ) /\ t e. E ) ) )
53 48 49 52 syl2anc 
 |-  ( ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) /\ ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) ) -> ( <. ( t ` G ) , t >. e. ( I ` P ) <-> ( ( t ` G ) = ( t ` G ) /\ t e. E ) ) )
54 46 47 53 mpbir2and 
 |-  ( ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) /\ ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) ) -> <. ( t ` G ) , t >. e. ( I ` P ) )
55 eqidd 
 |-  ( ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) /\ ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) ) -> ( ( N ` t ) ` D ) = ( ( N ` t ) ` D ) )
56 3 15 17 20 tendoicl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ t e. E ) -> ( N ` t ) e. E )
57 48 47 56 syl2anc 
 |-  ( ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) /\ ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) ) -> ( N ` t ) e. E )
58 13 ad2antrr 
 |-  ( ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) /\ ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) ) -> ( Q e. A /\ -. Q .<_ W ) )
59 fvex 
 |-  ( ( N ` t ) ` D ) e. _V
60 fvex 
 |-  ( N ` t ) e. _V
61 2 6 3 14 15 17 9 19 59 60 dihopelvalcqat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( <. ( ( N ` t ) ` D ) , ( N ` t ) >. e. ( I ` Q ) <-> ( ( ( N ` t ) ` D ) = ( ( N ` t ) ` D ) /\ ( N ` t ) e. E ) ) )
62 48 58 61 syl2anc 
 |-  ( ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) /\ ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) ) -> ( <. ( ( N ` t ) ` D ) , ( N ` t ) >. e. ( I ` Q ) <-> ( ( ( N ` t ) ` D ) = ( ( N ` t ) ` D ) /\ ( N ` t ) e. E ) ) )
63 55 57 62 mpbir2and 
 |-  ( ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) /\ ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) ) -> <. ( ( N ` t ) ` D ) , ( N ` t ) >. e. ( I ` Q ) )
64 29 ad2antrr 
 |-  ( ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) /\ ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) ) -> G e. T )
65 33 ad2antrr 
 |-  ( ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) /\ ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) ) -> `' D e. T )
66 3 15 17 tendospdi1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( t e. E /\ G e. T /\ `' D e. T ) ) -> ( t ` ( G o. `' D ) ) = ( ( t ` G ) o. ( t ` `' D ) ) )
67 48 47 64 65 66 syl13anc 
 |-  ( ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) /\ ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) ) -> ( t ` ( G o. `' D ) ) = ( ( t ` G ) o. ( t ` `' D ) ) )
68 simprr 
 |-  ( ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) /\ ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) ) -> ( t ` ( G o. `' D ) ) = f )
69 31 ad2antrr 
 |-  ( ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) /\ ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) ) -> D e. T )
70 20 15 tendoi2 
 |-  ( ( t e. E /\ D e. T ) -> ( ( N ` t ) ` D ) = `' ( t ` D ) )
71 47 69 70 syl2anc 
 |-  ( ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) /\ ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) ) -> ( ( N ` t ) ` D ) = `' ( t ` D ) )
72 3 15 17 tendocnv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ t e. E /\ D e. T ) -> `' ( t ` D ) = ( t ` `' D ) )
73 48 47 69 72 syl3anc 
 |-  ( ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) /\ ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) ) -> `' ( t ` D ) = ( t ` `' D ) )
74 71 73 eqtr2d 
 |-  ( ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) /\ ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) ) -> ( t ` `' D ) = ( ( N ` t ) ` D ) )
75 74 coeq2d 
 |-  ( ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) /\ ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) ) -> ( ( t ` G ) o. ( t ` `' D ) ) = ( ( t ` G ) o. ( ( N ` t ) ` D ) ) )
76 67 68 75 3eqtr3d 
 |-  ( ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) /\ ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) ) -> f = ( ( t ` G ) o. ( ( N ` t ) ` D ) ) )
77 simplrr 
 |-  ( ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) /\ ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) ) -> s = .0. )
78 3 15 17 20 1 22 21 tendoipl2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ t e. E ) -> ( t J ( N ` t ) ) = .0. )
79 48 47 78 syl2anc 
 |-  ( ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) /\ ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) ) -> ( t J ( N ` t ) ) = .0. )
80 77 79 eqtr4d 
 |-  ( ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) /\ ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) ) -> s = ( t J ( N ` t ) ) )
81 opeq1 
 |-  ( g = ( t ` G ) -> <. g , t >. = <. ( t ` G ) , t >. )
82 81 eleq1d 
 |-  ( g = ( t ` G ) -> ( <. g , t >. e. ( I ` P ) <-> <. ( t ` G ) , t >. e. ( I ` P ) ) )
83 82 anbi1d 
 |-  ( g = ( t ` G ) -> ( ( <. g , t >. e. ( I ` P ) /\ <. h , u >. e. ( I ` Q ) ) <-> ( <. ( t ` G ) , t >. e. ( I ` P ) /\ <. h , u >. e. ( I ` Q ) ) ) )
84 coeq1 
 |-  ( g = ( t ` G ) -> ( g o. h ) = ( ( t ` G ) o. h ) )
85 84 eqeq2d 
 |-  ( g = ( t ` G ) -> ( f = ( g o. h ) <-> f = ( ( t ` G ) o. h ) ) )
86 85 anbi1d 
 |-  ( g = ( t ` G ) -> ( ( f = ( g o. h ) /\ s = ( t J u ) ) <-> ( f = ( ( t ` G ) o. h ) /\ s = ( t J u ) ) ) )
87 83 86 anbi12d 
 |-  ( g = ( t ` G ) -> ( ( ( <. g , t >. e. ( I ` P ) /\ <. h , u >. e. ( I ` Q ) ) /\ ( f = ( g o. h ) /\ s = ( t J u ) ) ) <-> ( ( <. ( t ` G ) , t >. e. ( I ` P ) /\ <. h , u >. e. ( I ` Q ) ) /\ ( f = ( ( t ` G ) o. h ) /\ s = ( t J u ) ) ) ) )
88 opeq1 
 |-  ( h = ( ( N ` t ) ` D ) -> <. h , u >. = <. ( ( N ` t ) ` D ) , u >. )
89 88 eleq1d 
 |-  ( h = ( ( N ` t ) ` D ) -> ( <. h , u >. e. ( I ` Q ) <-> <. ( ( N ` t ) ` D ) , u >. e. ( I ` Q ) ) )
90 89 anbi2d 
 |-  ( h = ( ( N ` t ) ` D ) -> ( ( <. ( t ` G ) , t >. e. ( I ` P ) /\ <. h , u >. e. ( I ` Q ) ) <-> ( <. ( t ` G ) , t >. e. ( I ` P ) /\ <. ( ( N ` t ) ` D ) , u >. e. ( I ` Q ) ) ) )
91 coeq2 
 |-  ( h = ( ( N ` t ) ` D ) -> ( ( t ` G ) o. h ) = ( ( t ` G ) o. ( ( N ` t ) ` D ) ) )
92 91 eqeq2d 
 |-  ( h = ( ( N ` t ) ` D ) -> ( f = ( ( t ` G ) o. h ) <-> f = ( ( t ` G ) o. ( ( N ` t ) ` D ) ) ) )
93 92 anbi1d 
 |-  ( h = ( ( N ` t ) ` D ) -> ( ( f = ( ( t ` G ) o. h ) /\ s = ( t J u ) ) <-> ( f = ( ( t ` G ) o. ( ( N ` t ) ` D ) ) /\ s = ( t J u ) ) ) )
94 90 93 anbi12d 
 |-  ( h = ( ( N ` t ) ` D ) -> ( ( ( <. ( t ` G ) , t >. e. ( I ` P ) /\ <. h , u >. e. ( I ` Q ) ) /\ ( f = ( ( t ` G ) o. h ) /\ s = ( t J u ) ) ) <-> ( ( <. ( t ` G ) , t >. e. ( I ` P ) /\ <. ( ( N ` t ) ` D ) , u >. e. ( I ` Q ) ) /\ ( f = ( ( t ` G ) o. ( ( N ` t ) ` D ) ) /\ s = ( t J u ) ) ) ) )
95 opeq2 
 |-  ( u = ( N ` t ) -> <. ( ( N ` t ) ` D ) , u >. = <. ( ( N ` t ) ` D ) , ( N ` t ) >. )
96 95 eleq1d 
 |-  ( u = ( N ` t ) -> ( <. ( ( N ` t ) ` D ) , u >. e. ( I ` Q ) <-> <. ( ( N ` t ) ` D ) , ( N ` t ) >. e. ( I ` Q ) ) )
97 96 anbi2d 
 |-  ( u = ( N ` t ) -> ( ( <. ( t ` G ) , t >. e. ( I ` P ) /\ <. ( ( N ` t ) ` D ) , u >. e. ( I ` Q ) ) <-> ( <. ( t ` G ) , t >. e. ( I ` P ) /\ <. ( ( N ` t ) ` D ) , ( N ` t ) >. e. ( I ` Q ) ) ) )
98 oveq2 
 |-  ( u = ( N ` t ) -> ( t J u ) = ( t J ( N ` t ) ) )
99 98 eqeq2d 
 |-  ( u = ( N ` t ) -> ( s = ( t J u ) <-> s = ( t J ( N ` t ) ) ) )
100 99 anbi2d 
 |-  ( u = ( N ` t ) -> ( ( f = ( ( t ` G ) o. ( ( N ` t ) ` D ) ) /\ s = ( t J u ) ) <-> ( f = ( ( t ` G ) o. ( ( N ` t ) ` D ) ) /\ s = ( t J ( N ` t ) ) ) ) )
101 97 100 anbi12d 
 |-  ( u = ( N ` t ) -> ( ( ( <. ( t ` G ) , t >. e. ( I ` P ) /\ <. ( ( N ` t ) ` D ) , u >. e. ( I ` Q ) ) /\ ( f = ( ( t ` G ) o. ( ( N ` t ) ` D ) ) /\ s = ( t J u ) ) ) <-> ( ( <. ( t ` G ) , t >. e. ( I ` P ) /\ <. ( ( N ` t ) ` D ) , ( N ` t ) >. e. ( I ` Q ) ) /\ ( f = ( ( t ` G ) o. ( ( N ` t ) ` D ) ) /\ s = ( t J ( N ` t ) ) ) ) ) )
102 87 94 101 syl3an9b 
 |-  ( ( g = ( t ` G ) /\ h = ( ( N ` t ) ` D ) /\ u = ( N ` t ) ) -> ( ( ( <. g , t >. e. ( I ` P ) /\ <. h , u >. e. ( I ` Q ) ) /\ ( f = ( g o. h ) /\ s = ( t J u ) ) ) <-> ( ( <. ( t ` G ) , t >. e. ( I ` P ) /\ <. ( ( N ` t ) ` D ) , ( N ` t ) >. e. ( I ` Q ) ) /\ ( f = ( ( t ` G ) o. ( ( N ` t ) ` D ) ) /\ s = ( t J ( N ` t ) ) ) ) ) )
103 102 spc3egv 
 |-  ( ( ( t ` G ) e. _V /\ ( ( N ` t ) ` D ) e. _V /\ ( N ` t ) e. _V ) -> ( ( ( <. ( t ` G ) , t >. e. ( I ` P ) /\ <. ( ( N ` t ) ` D ) , ( N ` t ) >. e. ( I ` Q ) ) /\ ( f = ( ( t ` G ) o. ( ( N ` t ) ` D ) ) /\ s = ( t J ( N ` t ) ) ) ) -> E. g E. h E. u ( ( <. g , t >. e. ( I ` P ) /\ <. h , u >. e. ( I ` Q ) ) /\ ( f = ( g o. h ) /\ s = ( t J u ) ) ) ) )
104 50 59 60 103 mp3an 
 |-  ( ( ( <. ( t ` G ) , t >. e. ( I ` P ) /\ <. ( ( N ` t ) ` D ) , ( N ` t ) >. e. ( I ` Q ) ) /\ ( f = ( ( t ` G ) o. ( ( N ` t ) ` D ) ) /\ s = ( t J ( N ` t ) ) ) ) -> E. g E. h E. u ( ( <. g , t >. e. ( I ` P ) /\ <. h , u >. e. ( I ` Q ) ) /\ ( f = ( g o. h ) /\ s = ( t J u ) ) ) )
105 54 63 76 80 104 syl22anc 
 |-  ( ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) /\ ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) ) -> E. g E. h E. u ( ( <. g , t >. e. ( I ` P ) /\ <. h , u >. e. ( I ` Q ) ) /\ ( f = ( g o. h ) /\ s = ( t J u ) ) ) )
106 105 ex 
 |-  ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) -> ( ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) -> E. g E. h E. u ( ( <. g , t >. e. ( I ` P ) /\ <. h , u >. e. ( I ` Q ) ) /\ ( f = ( g o. h ) /\ s = ( t J u ) ) ) ) )
107 106 eximdv 
 |-  ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) -> ( E. t ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) -> E. t E. g E. h E. u ( ( <. g , t >. e. ( I ` P ) /\ <. h , u >. e. ( I ` Q ) ) /\ ( f = ( g o. h ) /\ s = ( t J u ) ) ) ) )
108 excom 
 |-  ( E. t E. g E. h E. u ( ( <. g , t >. e. ( I ` P ) /\ <. h , u >. e. ( I ` Q ) ) /\ ( f = ( g o. h ) /\ s = ( t J u ) ) ) <-> E. g E. t E. h E. u ( ( <. g , t >. e. ( I ` P ) /\ <. h , u >. e. ( I ` Q ) ) /\ ( f = ( g o. h ) /\ s = ( t J u ) ) ) )
109 107 108 syl6ib 
 |-  ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) -> ( E. t ( t e. E /\ ( t ` ( G o. `' D ) ) = f ) -> E. g E. t E. h E. u ( ( <. g , t >. e. ( I ` P ) /\ <. h , u >. e. ( I ` Q ) ) /\ ( f = ( g o. h ) /\ s = ( t J u ) ) ) ) )
110 45 109 mpd 
 |-  ( ( ph /\ ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) -> E. g E. t E. h E. u ( ( <. g , t >. e. ( I ` P ) /\ <. h , u >. e. ( I ` Q ) ) /\ ( f = ( g o. h ) /\ s = ( t J u ) ) ) )
111 110 ex 
 |-  ( ph -> ( ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) -> E. g E. t E. h E. u ( ( <. g , t >. e. ( I ` P ) /\ <. h , u >. e. ( I ` Q ) ) /\ ( f = ( g o. h ) /\ s = ( t J u ) ) ) ) )
112 11 simpld 
 |-  ( ph -> K e. HL )
113 112 hllatd 
 |-  ( ph -> K e. Lat )
114 12 simpld 
 |-  ( ph -> P e. A )
115 13 simpld 
 |-  ( ph -> Q e. A )
116 1 4 6 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) e. B )
117 112 114 115 116 syl3anc 
 |-  ( ph -> ( P .\/ Q ) e. B )
118 11 simprd 
 |-  ( ph -> W e. H )
119 1 3 lhpbase 
 |-  ( W e. H -> W e. B )
120 118 119 syl 
 |-  ( ph -> W e. B )
121 1 5 latmcl 
 |-  ( ( K e. Lat /\ ( P .\/ Q ) e. B /\ W e. B ) -> ( ( P .\/ Q ) ./\ W ) e. B )
122 113 117 120 121 syl3anc 
 |-  ( ph -> ( ( P .\/ Q ) ./\ W ) e. B )
123 10 122 eqeltrid 
 |-  ( ph -> V e. B )
124 1 2 5 latmle2 
 |-  ( ( K e. Lat /\ ( P .\/ Q ) e. B /\ W e. B ) -> ( ( P .\/ Q ) ./\ W ) .<_ W )
125 113 117 120 124 syl3anc 
 |-  ( ph -> ( ( P .\/ Q ) ./\ W ) .<_ W )
126 10 125 eqbrtrid 
 |-  ( ph -> V .<_ W )
127 eqid 
 |-  ( ( DIsoB ` K ) ` W ) = ( ( DIsoB ` K ) ` W )
128 1 2 3 9 127 dihvalb 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( V e. B /\ V .<_ W ) ) -> ( I ` V ) = ( ( ( DIsoB ` K ) ` W ) ` V ) )
129 11 123 126 128 syl12anc 
 |-  ( ph -> ( I ` V ) = ( ( ( DIsoB ` K ) ` W ) ` V ) )
130 129 eleq2d 
 |-  ( ph -> ( <. f , s >. e. ( I ` V ) <-> <. f , s >. e. ( ( ( DIsoB ` K ) ` W ) ` V ) ) )
131 1 2 3 15 16 21 127 dibopelval3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( V e. B /\ V .<_ W ) ) -> ( <. f , s >. e. ( ( ( DIsoB ` K ) ` W ) ` V ) <-> ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) )
132 11 123 126 131 syl12anc 
 |-  ( ph -> ( <. f , s >. e. ( ( ( DIsoB ` K ) ` W ) ` V ) <-> ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) )
133 130 132 bitrd 
 |-  ( ph -> ( <. f , s >. e. ( I ` V ) <-> ( ( f e. T /\ ( R ` f ) .<_ V ) /\ s = .0. ) ) )
134 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
135 1 6 atbase 
 |-  ( P e. A -> P e. B )
136 114 135 syl 
 |-  ( ph -> P e. B )
137 1 6 atbase 
 |-  ( Q e. A -> Q e. B )
138 115 137 syl 
 |-  ( ph -> Q e. B )
139 1 3 15 17 22 7 134 8 9 11 136 138 dihopellsm 
 |-  ( ph -> ( <. f , s >. e. ( ( I ` P ) .(+) ( I ` Q ) ) <-> E. g E. t E. h E. u ( ( <. g , t >. e. ( I ` P ) /\ <. h , u >. e. ( I ` Q ) ) /\ ( f = ( g o. h ) /\ s = ( t J u ) ) ) ) )
140 111 133 139 3imtr4d 
 |-  ( ph -> ( <. f , s >. e. ( I ` V ) -> <. f , s >. e. ( ( I ` P ) .(+) ( I ` Q ) ) ) )
141 24 140 relssdv 
 |-  ( ph -> ( I ` V ) C_ ( ( I ` P ) .(+) ( I ` Q ) ) )