Metamath Proof Explorer

Theorem dih2dimbALTN

Description: Extend dia2dim to isomorphism H. (This version combines dib2dim and dih2dimb 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.)

Ref Expression
Hypotheses 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 dih2dimbALTN 
|- ( ph -> ( I ` ( P .\/ Q ) ) C_ ( ( I ` P ) .(+) ( I ` Q ) ) )

Proof

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