Metamath Proof Explorer

Theorem dib2dim

Description: Extend dia2dim to partial isomorphism B. (Contributed by NM, 22-Sep-2014)

Ref Expression
Hypotheses dib2dim.l 
|- .<_ = ( le ` K )
dib2dim.j 
|- .\/ = ( join ` K )
dib2dim.a 
|- A = ( Atoms ` K )
dib2dim.h 
|- H = ( LHyp ` K )
dib2dim.u 
|- U = ( ( DVecH ` K ) ` W )
dib2dim.s 
|- .(+) = ( LSSum ` U )
dib2dim.i 
|- I = ( ( DIsoB ` K ) ` W )
dib2dim.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
dib2dim.p 
|- ( ph -> ( P e. A /\ P .<_ W ) )
dib2dim.q 
|- ( ph -> ( Q e. A /\ Q .<_ W ) )
Assertion dib2dim 
|- ( ph -> ( I ` ( P .\/ Q ) ) C_ ( ( I ` P ) .(+) ( I ` Q ) ) )

Proof

Step Hyp Ref Expression
1 dib2dim.l 
 |-  .<_ = ( le ` K )
2 dib2dim.j 
 |-  .\/ = ( join ` K )
3 dib2dim.a 
 |-  A = ( Atoms ` K )
4 dib2dim.h 
 |-  H = ( LHyp ` K )
5 dib2dim.u 
 |-  U = ( ( DVecH ` K ) ` W )
6 dib2dim.s 
 |-  .(+) = ( LSSum ` U )
7 dib2dim.i 
 |-  I = ( ( DIsoB ` K ) ` W )
8 dib2dim.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
9 dib2dim.p 
 |-  ( ph -> ( P e. A /\ P .<_ W ) )
10 dib2dim.q 
 |-  ( ph -> ( Q e. A /\ Q .<_ W ) )
11 4 7 dibvalrel 
 |-  ( ( K e. HL /\ W e. H ) -> Rel ( I ` ( P .\/ Q ) ) )
12 8 11 syl 
 |-  ( ph -> Rel ( I ` ( P .\/ Q ) ) )
13 eqid 
 |-  ( ( DVecA ` K ) ` W ) = ( ( DVecA ` K ) ` W )
14 eqid 
 |-  ( LSSum ` ( ( DVecA ` K ) ` W ) ) = ( LSSum ` ( ( DVecA ` K ) ` W ) )
15 eqid 
 |-  ( ( DIsoA ` K ) ` W ) = ( ( DIsoA ` K ) ` W )
16 1 2 3 4 13 14 15 8 9 10 dia2dim 
 |-  ( ph -> ( ( ( DIsoA ` K ) ` W ) ` ( P .\/ Q ) ) C_ ( ( ( ( DIsoA ` K ) ` W ) ` P ) ( LSSum ` ( ( DVecA ` K ) ` W ) ) ( ( ( DIsoA ` K ) ` W ) ` Q ) ) )
17 16 sseld 
 |-  ( ph -> ( f e. ( ( ( DIsoA ` K ) ` W ) ` ( P .\/ Q ) ) -> f e. ( ( ( ( DIsoA ` K ) ` W ) ` P ) ( LSSum ` ( ( DVecA ` K ) ` W ) ) ( ( ( DIsoA ` K ) ` W ) ` Q ) ) ) )
18 17 anim1d 
 |-  ( 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 ) ) ) ) ) )
19 8 simpld 
 |-  ( ph -> K e. HL )
20 9 simpld 
 |-  ( ph -> P e. A )
21 10 simpld 
 |-  ( ph -> Q e. A )
22 eqid 
 |-  ( Base ` K ) = ( Base ` K )
23 22 2 3 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) e. ( Base ` K ) )
24 19 20 21 23 syl3anc 
 |-  ( ph -> ( P .\/ Q ) e. ( Base ` K ) )
25 9 simprd 
 |-  ( ph -> P .<_ W )
26 10 simprd 
 |-  ( ph -> Q .<_ W )
27 19 hllatd 
 |-  ( ph -> K e. Lat )
28 22 3 atbase 
 |-  ( P e. A -> P e. ( Base ` K ) )
29 20 28 syl 
 |-  ( ph -> P e. ( Base ` K ) )
30 22 3 atbase 
 |-  ( Q e. A -> Q e. ( Base ` K ) )
31 21 30 syl 
 |-  ( ph -> Q e. ( Base ` K ) )
32 8 simprd 
 |-  ( ph -> W e. H )
33 22 4 lhpbase 
 |-  ( W e. H -> W e. ( Base ` K ) )
34 32 33 syl 
 |-  ( ph -> W e. ( Base ` K ) )
35 22 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( P e. ( Base ` K ) /\ Q e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( P .<_ W /\ Q .<_ W ) <-> ( P .\/ Q ) .<_ W ) )
36 27 29 31 34 35 syl13anc 
 |-  ( ph -> ( ( P .<_ W /\ Q .<_ W ) <-> ( P .\/ Q ) .<_ W ) )
37 25 26 36 mpbi2and 
 |-  ( ph -> ( P .\/ Q ) .<_ W )
38 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
39 eqid 
 |-  ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) = ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) )
40 22 1 4 38 39 15 7 dibopelval2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P .\/ Q ) e. ( Base ` K ) /\ ( P .\/ Q ) .<_ W ) ) -> ( <. f , s >. e. ( I ` ( P .\/ Q ) ) <-> ( f e. ( ( ( DIsoA ` K ) ` W ) ` ( P .\/ Q ) ) /\ s = ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) ) ) )
41 8 24 37 40 syl12anc 
 |-  ( ph -> ( <. f , s >. e. ( I ` ( P .\/ Q ) ) <-> ( f e. ( ( ( DIsoA ` K ) ` W ) ` ( P .\/ Q ) ) /\ s = ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) ) ) )
42 29 25 jca 
 |-  ( ph -> ( P e. ( Base ` K ) /\ P .<_ W ) )
43 31 26 jca 
 |-  ( ph -> ( Q e. ( Base ` K ) /\ Q .<_ W ) )
44 22 1 4 38 39 13 5 14 6 15 7 8 42 43 diblsmopel 
 |-  ( ph -> ( <. f , s >. e. ( ( I ` P ) .(+) ( I ` Q ) ) <-> ( f e. ( ( ( ( DIsoA ` K ) ` W ) ` P ) ( LSSum ` ( ( DVecA ` K ) ` W ) ) ( ( ( DIsoA ` K ) ` W ) ` Q ) ) /\ s = ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) ) ) )
45 18 41 44 3imtr4d 
 |-  ( ph -> ( <. f , s >. e. ( I ` ( P .\/ Q ) ) -> <. f , s >. e. ( ( I ` P ) .(+) ( I ` Q ) ) ) )
46 12 45 relssdv 
 |-  ( ph -> ( I ` ( P .\/ Q ) ) C_ ( ( I ` P ) .(+) ( I ` Q ) ) )