Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dih2dimbALTN Structured version   Unicode version

Theorem dih2dimbALTN 34503
Description: Extend dia2dim 34335 to isomorphism H. (This version combines dib2dim 34501 and dih2dimb 34502 for shorter overall proof, but may be less easy to understand. TODO: decide which to use.) (Contributed by NM, 22-Sep-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
dih2dimb.l  |-  .<_  =  ( le `  K )
dih2dimb.j  |-  .\/  =  ( join `  K )
dih2dimb.a  |-  A  =  ( Atoms `  K )
dih2dimb.h  |-  H  =  ( LHyp `  K
)
dih2dimb.u  |-  U  =  ( ( DVecH `  K
) `  W )
dih2dimb.s  |-  .(+)  =  (
LSSum `  U )
dih2dimb.i  |-  I  =  ( ( DIsoH `  K
) `  W )
dih2dimb.k  |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )
dih2dimb.p  |-  ( ph  ->  ( P  e.  A  /\  P  .<_  W ) )
dih2dimb.q  |-  ( ph  ->  ( Q  e.  A  /\  Q  .<_  W ) )
Assertion
Ref Expression
dih2dimbALTN  |-  ( ph  ->  ( I `  ( P  .\/  Q ) ) 
C_  ( ( I `
 P )  .(+)  ( I `  Q ) ) )

Proof of Theorem dih2dimbALTN
Dummy variables  f 
s are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dih2dimb.k . . . 4  |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )
2 dih2dimb.h . . . . 5  |-  H  =  ( LHyp `  K
)
3 eqid 2435 . . . . 5  |-  ( (
DIsoB `  K ) `  W )  =  ( ( DIsoB `  K ) `  W )
42, 3dibvalrel 34421 . . . 4  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  Rel  ( ( (
DIsoB `  K ) `  W ) `  ( P  .\/  Q ) ) )
51, 4syl 16 . . 3  |-  ( ph  ->  Rel  ( ( (
DIsoB `  K ) `  W ) `  ( P  .\/  Q ) ) )
6 dih2dimb.l . . . . . . 7  |-  .<_  =  ( le `  K )
7 dih2dimb.j . . . . . . 7  |-  .\/  =  ( join `  K )
8 dih2dimb.a . . . . . . 7  |-  A  =  ( Atoms `  K )
9 eqid 2435 . . . . . . 7  |-  ( (
DVecA `  K ) `  W )  =  ( ( DVecA `  K ) `  W )
10 eqid 2435 . . . . . . 7  |-  ( LSSum `  ( ( DVecA `  K
) `  W )
)  =  ( LSSum `  ( ( DVecA `  K
) `  W )
)
11 eqid 2435 . . . . . . 7  |-  ( (
DIsoA `  K ) `  W )  =  ( ( DIsoA `  K ) `  W )
12 dih2dimb.p . . . . . . 7  |-  ( ph  ->  ( P  e.  A  /\  P  .<_  W ) )
13 dih2dimb.q . . . . . . 7  |-  ( ph  ->  ( Q  e.  A  /\  Q  .<_  W ) )
146, 7, 8, 2, 9, 10, 11, 1, 12, 13dia2dim 34335 . . . . . 6  |-  ( ph  ->  ( ( ( DIsoA `  K ) `  W
) `  ( P  .\/  Q ) )  C_  ( ( ( (
DIsoA `  K ) `  W ) `  P
) ( LSSum `  (
( DVecA `  K ) `  W ) ) ( ( ( DIsoA `  K
) `  W ) `  Q ) ) )
1514sseld 3345 . . . . 5  |-  ( ph  ->  ( f  e.  ( ( ( DIsoA `  K
) `  W ) `  ( P  .\/  Q
) )  ->  f  e.  ( ( ( (
DIsoA `  K ) `  W ) `  P
) ( LSSum `  (
( DVecA `  K ) `  W ) ) ( ( ( DIsoA `  K
) `  W ) `  Q ) ) ) )
1615anim1d 561 . . . 4  |-  ( ph  ->  ( ( f  e.  ( ( ( DIsoA `  K ) `  W
) `  ( P  .\/  Q ) )  /\  s  =  ( f  e.  ( ( LTrn `  K
) `  W )  |->  (  _I  |`  ( Base `  K ) ) ) )  ->  (
f  e.  ( ( ( ( DIsoA `  K
) `  W ) `  P ) ( LSSum `  ( ( DVecA `  K
) `  W )
) ( ( (
DIsoA `  K ) `  W ) `  Q
) )  /\  s  =  ( f  e.  ( ( LTrn `  K
) `  W )  |->  (  _I  |`  ( Base `  K ) ) ) ) ) )
171simpld 456 . . . . . 6  |-  ( ph  ->  K  e.  HL )
1812simpld 456 . . . . . 6  |-  ( ph  ->  P  e.  A )
1913simpld 456 . . . . . 6  |-  ( ph  ->  Q  e.  A )
20 eqid 2435 . . . . . . 7  |-  ( Base `  K )  =  (
Base `  K )
2120, 7, 8hlatjcl 32624 . . . . . 6  |-  ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  ->  ( P  .\/  Q
)  e.  ( Base `  K ) )
2217, 18, 19, 21syl3anc 1213 . . . . 5  |-  ( ph  ->  ( P  .\/  Q
)  e.  ( Base `  K ) )
2312simprd 460 . . . . . 6  |-  ( ph  ->  P  .<_  W )
2413simprd 460 . . . . . 6  |-  ( ph  ->  Q  .<_  W )
25 hllat 32621 . . . . . . . 8  |-  ( K  e.  HL  ->  K  e.  Lat )
2617, 25syl 16 . . . . . . 7  |-  ( ph  ->  K  e.  Lat )
2720, 8atbase 32547 . . . . . . . 8  |-  ( P  e.  A  ->  P  e.  ( Base `  K
) )
2818, 27syl 16 . . . . . . 7  |-  ( ph  ->  P  e.  ( Base `  K ) )
2920, 8atbase 32547 . . . . . . . 8  |-  ( Q  e.  A  ->  Q  e.  ( Base `  K
) )
3019, 29syl 16 . . . . . . 7  |-  ( ph  ->  Q  e.  ( Base `  K ) )
311simprd 460 . . . . . . . 8  |-  ( ph  ->  W  e.  H )
3220, 2lhpbase 33255 . . . . . . . 8  |-  ( W  e.  H  ->  W  e.  ( Base `  K
) )
3331, 32syl 16 . . . . . . 7  |-  ( ph  ->  W  e.  ( Base `  K ) )
3420, 6, 7latjle12 15217 . . . . . . 7  |-  ( ( K  e.  Lat  /\  ( P  e.  ( Base `  K )  /\  Q  e.  ( Base `  K )  /\  W  e.  ( Base `  K
) ) )  -> 
( ( P  .<_  W  /\  Q  .<_  W )  <-> 
( P  .\/  Q
)  .<_  W ) )
3526, 28, 30, 33, 34syl13anc 1215 . . . . . 6  |-  ( ph  ->  ( ( P  .<_  W  /\  Q  .<_  W )  <-> 
( P  .\/  Q
)  .<_  W ) )
3623, 24, 35mpbi2and 907 . . . . 5  |-  ( ph  ->  ( P  .\/  Q
)  .<_  W )
37 eqid 2435 . . . . . 6  |-  ( (
LTrn `  K ) `  W )  =  ( ( LTrn `  K
) `  W )
38 eqid 2435 . . . . . 6  |-  ( f  e.  ( ( LTrn `  K ) `  W
)  |->  (  _I  |`  ( Base `  K ) ) )  =  ( f  e.  ( ( LTrn `  K ) `  W
)  |->  (  _I  |`  ( Base `  K ) ) )
3920, 6, 2, 37, 38, 11, 3dibopelval2 34403 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P 
.\/  Q )  e.  ( Base `  K
)  /\  ( P  .\/  Q )  .<_  W ) )  ->  ( <. f ,  s >.  e.  ( ( ( DIsoB `  K
) `  W ) `  ( P  .\/  Q
) )  <->  ( f  e.  ( ( ( DIsoA `  K ) `  W
) `  ( P  .\/  Q ) )  /\  s  =  ( f  e.  ( ( LTrn `  K
) `  W )  |->  (  _I  |`  ( Base `  K ) ) ) ) ) )
401, 22, 36, 39syl12anc 1211 . . . 4  |-  ( ph  ->  ( <. f ,  s
>.  e.  ( ( (
DIsoB `  K ) `  W ) `  ( P  .\/  Q ) )  <-> 
( f  e.  ( ( ( DIsoA `  K
) `  W ) `  ( P  .\/  Q
) )  /\  s  =  ( f  e.  ( ( LTrn `  K
) `  W )  |->  (  _I  |`  ( Base `  K ) ) ) ) ) )
41 dih2dimb.u . . . . 5  |-  U  =  ( ( DVecH `  K
) `  W )
42 dih2dimb.s . . . . 5  |-  .(+)  =  (
LSSum `  U )
4328, 23jca 529 . . . . 5  |-  ( ph  ->  ( P  e.  (
Base `  K )  /\  P  .<_  W ) )
4430, 24jca 529 . . . . 5  |-  ( ph  ->  ( Q  e.  (
Base `  K )  /\  Q  .<_  W ) )
4520, 6, 2, 37, 38, 9, 41, 10, 42, 11, 3, 1, 43, 44diblsmopel 34429 . . . 4  |-  ( ph  ->  ( <. f ,  s
>.  e.  ( ( ( ( DIsoB `  K ) `  W ) `  P
)  .(+)  ( ( (
DIsoB `  K ) `  W ) `  Q
) )  <->  ( f  e.  ( ( ( (
DIsoA `  K ) `  W ) `  P
) ( LSSum `  (
( DVecA `  K ) `  W ) ) ( ( ( DIsoA `  K
) `  W ) `  Q ) )  /\  s  =  ( f  e.  ( ( LTrn `  K
) `  W )  |->  (  _I  |`  ( Base `  K ) ) ) ) ) )
4616, 40, 453imtr4d 268 . . 3  |-  ( ph  ->  ( <. f ,  s
>.  e.  ( ( (
DIsoB `  K ) `  W ) `  ( P  .\/  Q ) )  ->  <. f ,  s
>.  e.  ( ( ( ( DIsoB `  K ) `  W ) `  P
)  .(+)  ( ( (
DIsoB `  K ) `  W ) `  Q
) ) ) )
475, 46relssdv 4921 . 2  |-  ( ph  ->  ( ( ( DIsoB `  K ) `  W
) `  ( P  .\/  Q ) )  C_  ( ( ( (
DIsoB `  K ) `  W ) `  P
)  .(+)  ( ( (
DIsoB `  K ) `  W ) `  Q
) ) )
48 dih2dimb.i . . . 4  |-  I  =  ( ( DIsoH `  K
) `  W )
4920, 6, 2, 48, 3dihvalb 34495 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P 
.\/  Q )  e.  ( Base `  K
)  /\  ( P  .\/  Q )  .<_  W ) )  ->  ( I `  ( P  .\/  Q
) )  =  ( ( ( DIsoB `  K
) `  W ) `  ( P  .\/  Q
) ) )
501, 22, 36, 49syl12anc 1211 . 2  |-  ( ph  ->  ( I `  ( P  .\/  Q ) )  =  ( ( (
DIsoB `  K ) `  W ) `  ( P  .\/  Q ) ) )
5120, 6, 2, 48, 3dihvalb 34495 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  ( Base `  K
)  /\  P  .<_  W ) )  ->  (
I `  P )  =  ( ( (
DIsoB `  K ) `  W ) `  P
) )
521, 28, 23, 51syl12anc 1211 . . 3  |-  ( ph  ->  ( I `  P
)  =  ( ( ( DIsoB `  K ) `  W ) `  P
) )
5320, 6, 2, 48, 3dihvalb 34495 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( Q  e.  ( Base `  K
)  /\  Q  .<_  W ) )  ->  (
I `  Q )  =  ( ( (
DIsoB `  K ) `  W ) `  Q
) )
541, 30, 24, 53syl12anc 1211 . . 3  |-  ( ph  ->  ( I `  Q
)  =  ( ( ( DIsoB `  K ) `  W ) `  Q
) )
5552, 54oveq12d 6100 . 2  |-  ( ph  ->  ( ( I `  P )  .(+)  ( I `
 Q ) )  =  ( ( ( ( DIsoB `  K ) `  W ) `  P
)  .(+)  ( ( (
DIsoB `  K ) `  W ) `  Q
) ) )
5647, 50, 553sstr4d 3389 1  |-  ( ph  ->  ( I `  ( P  .\/  Q ) ) 
C_  ( ( I `
 P )  .(+)  ( I `  Q ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1364    e. wcel 1757    C_ wss 3318   <.cop 3873   class class class wbr 4282    e. cmpt 4340    _I cid 4620    |` cres 4831   Rel wrel 4834   ` cfv 5408  (class class class)co 6082   Basecbs 14159   lecple 14230   joincjn 15099   Latclat 15200   LSSumclsm 16115   Atomscatm 32521   HLchlt 32608   LHypclh 33241   LTrncltrn 33358   DVecAcdveca 34259   DIsoAcdia 34286   DVecHcdvh 34336   DIsoBcdib 34396   DIsoHcdih 34486
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416  ax-rep 4393  ax-sep 4403  ax-nul 4411  ax-pow 4460  ax-pr 4521  ax-un 6363  ax-cnex 9328  ax-resscn 9329  ax-1cn 9330  ax-icn 9331  ax-addcl 9332  ax-addrcl 9333  ax-mulcl 9334  ax-mulrcl 9335  ax-mulcom 9336  ax-addass 9337  ax-mulass 9338  ax-distr 9339  ax-i2m1 9340  ax-1ne0 9341  ax-1rid 9342  ax-rnegex 9343  ax-rrecex 9344  ax-cnre 9345  ax-pre-lttri 9346  ax-pre-lttrn 9347  ax-pre-ltadd 9348  ax-pre-mulgt0 9349  ax-riotaBAD 32217
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-fal 1370  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2966  df-sbc 3178  df-csb 3279  df-dif 3321  df-un 3323  df-in 3325  df-ss 3332  df-pss 3334  df-nul 3628  df-if 3782  df-pw 3852  df-sn 3868  df-pr 3870  df-tp 3872  df-op 3874  df-uni 4082  df-int 4119  df-iun 4163  df-iin 4164  df-br 4283  df-opab 4341  df-mpt 4342  df-tr 4376  df-eprel 4621  df-id 4625  df-po 4630  df-so 4631  df-fr 4668  df-we 4670  df-ord 4711  df-on 4712  df-lim 4713  df-suc 4714  df-xp 4835  df-rel 4836  df-cnv 4837  df-co 4838  df-dm 4839  df-rn 4840  df-res 4841  df-ima 4842  df-iota 5371  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-riota 6041  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-om 6468  df-1st 6568  df-2nd 6569  df-tpos 6736  df-undef 6780  df-recs 6820  df-rdg 6854  df-1o 6910  df-oadd 6914  df-er 7091  df-map 7206  df-en 7301  df-dom 7302  df-sdom 7303  df-fin 7304  df-pnf 9410  df-mnf 9411  df-xr 9412  df-ltxr 9413  df-le 9414  df-sub 9587  df-neg 9588  df-nn 10313  df-2 10370  df-3 10371  df-4 10372  df-5 10373  df-6 10374  df-n0 10570  df-z 10637  df-uz 10852  df-fz 11427  df-struct 14161  df-ndx 14162  df-slot 14163  df-base 14164  df-sets 14165  df-ress 14166  df-plusg 14236  df-mulr 14237  df-sca 14239  df-vsca 14240  df-0g 14365  df-poset 15101  df-plt 15113  df-lub 15129  df-glb 15130  df-join 15131  df-meet 15132  df-p0 15194  df-p1 15195  df-lat 15201  df-clat 15263  df-mnd 15400  df-submnd 15450  df-grp 15527  df-minusg 15528  df-sbg 15529  df-subg 15660  df-cntz 15817  df-lsm 16117  df-cmn 16261  df-abl 16262  df-mgp 16568  df-rng 16582  df-ur 16584  df-oppr 16651  df-dvdsr 16669  df-unit 16670  df-invr 16700  df-dvr 16711  df-drng 16760  df-lmod 16876  df-lss 16938  df-lsp 16977  df-lvec 17108  df-oposet 32434  df-ol 32436  df-oml 32437  df-covers 32524  df-ats 32525  df-atl 32556  df-cvlat 32580  df-hlat 32609  df-llines 32755  df-lplanes 32756  df-lvols 32757  df-lines 32758  df-psubsp 32760  df-pmap 32761  df-padd 33053  df-lhyp 33245  df-laut 33246  df-ldil 33361  df-ltrn 33362  df-trl 33416  df-tgrp 34000  df-tendo 34012  df-edring 34014  df-dveca 34260  df-disoa 34287  df-dvech 34337  df-dib 34397  df-dih 34487
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator