This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dihjat

Description: Isomorphism H of lattice join of two atoms. (Contributed by NM, 29-Sep-2014)

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

Proof

Step Hyp Ref Expression
1 dihjat.h 
 |-  H = ( LHyp ` K )
2 dihjat.j 
 |-  .\/ = ( join ` K )
3 dihjat.a 
 |-  A = ( Atoms ` K )
4 dihjat.u 
 |-  U = ( ( DVecH ` K ) ` W )
5 dihjat.s 
 |-  .(+) = ( LSSum ` U )
6 dihjat.i 
 |-  I = ( ( DIsoH ` K ) ` W )
7 dihjat.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
8 dihjat.p 
 |-  ( ph -> P e. A )
9 dihjat.q 
 |-  ( ph -> Q e. A )
10 eqid 
 |-  ( le ` K ) = ( le ` K )
11 7 adantr 
 |-  ( ( ph /\ ( P ( le ` K ) W /\ Q ( le ` K ) W ) ) -> ( K e. HL /\ W e. H ) )
12 8 adantr 
 |-  ( ( ph /\ ( P ( le ` K ) W /\ Q ( le ` K ) W ) ) -> P e. A )
13 simprl 
 |-  ( ( ph /\ ( P ( le ` K ) W /\ Q ( le ` K ) W ) ) -> P ( le ` K ) W )
14 12 13 jca 
 |-  ( ( ph /\ ( P ( le ` K ) W /\ Q ( le ` K ) W ) ) -> ( P e. A /\ P ( le ` K ) W ) )
15 9 adantr 
 |-  ( ( ph /\ ( P ( le ` K ) W /\ Q ( le ` K ) W ) ) -> Q e. A )
16 simprr 
 |-  ( ( ph /\ ( P ( le ` K ) W /\ Q ( le ` K ) W ) ) -> Q ( le ` K ) W )
17 15 16 jca 
 |-  ( ( ph /\ ( P ( le ` K ) W /\ Q ( le ` K ) W ) ) -> ( Q e. A /\ Q ( le ` K ) W ) )
18 10 1 2 3 4 5 6 11 14 17 dihjatb 
 |-  ( ( ph /\ ( P ( le ` K ) W /\ Q ( le ` K ) W ) ) -> ( I ` ( P .\/ Q ) ) = ( ( I ` P ) .(+) ( I ` Q ) ) )
19 eqid 
 |-  ( Base ` K ) = ( Base ` K )
20 7 adantr 
 |-  ( ( ph /\ ( P ( le ` K ) W /\ -. Q ( le ` K ) W ) ) -> ( K e. HL /\ W e. H ) )
21 19 3 atbase 
 |-  ( P e. A -> P e. ( Base ` K ) )
22 8 21 syl 
 |-  ( ph -> P e. ( Base ` K ) )
23 22 adantr 
 |-  ( ( ph /\ ( P ( le ` K ) W /\ -. Q ( le ` K ) W ) ) -> P e. ( Base ` K ) )
24 simprl 
 |-  ( ( ph /\ ( P ( le ` K ) W /\ -. Q ( le ` K ) W ) ) -> P ( le ` K ) W )
25 23 24 jca 
 |-  ( ( ph /\ ( P ( le ` K ) W /\ -. Q ( le ` K ) W ) ) -> ( P e. ( Base ` K ) /\ P ( le ` K ) W ) )
26 9 adantr 
 |-  ( ( ph /\ ( P ( le ` K ) W /\ -. Q ( le ` K ) W ) ) -> Q e. A )
27 simprr 
 |-  ( ( ph /\ ( P ( le ` K ) W /\ -. Q ( le ` K ) W ) ) -> -. Q ( le ` K ) W )
28 26 27 jca 
 |-  ( ( ph /\ ( P ( le ` K ) W /\ -. Q ( le ` K ) W ) ) -> ( Q e. A /\ -. Q ( le ` K ) W ) )
29 19 10 1 2 3 4 5 6 20 25 28 dihjatc 
 |-  ( ( ph /\ ( P ( le ` K ) W /\ -. Q ( le ` K ) W ) ) -> ( I ` ( P .\/ Q ) ) = ( ( I ` P ) .(+) ( I ` Q ) ) )
30 7 adantr 
 |-  ( ( ph /\ ( -. P ( le ` K ) W /\ Q ( le ` K ) W ) ) -> ( K e. HL /\ W e. H ) )
31 19 3 atbase 
 |-  ( Q e. A -> Q e. ( Base ` K ) )
32 9 31 syl 
 |-  ( ph -> Q e. ( Base ` K ) )
33 32 adantr 
 |-  ( ( ph /\ ( -. P ( le ` K ) W /\ Q ( le ` K ) W ) ) -> Q e. ( Base ` K ) )
34 simprr 
 |-  ( ( ph /\ ( -. P ( le ` K ) W /\ Q ( le ` K ) W ) ) -> Q ( le ` K ) W )
35 33 34 jca 
 |-  ( ( ph /\ ( -. P ( le ` K ) W /\ Q ( le ` K ) W ) ) -> ( Q e. ( Base ` K ) /\ Q ( le ` K ) W ) )
36 8 adantr 
 |-  ( ( ph /\ ( -. P ( le ` K ) W /\ Q ( le ` K ) W ) ) -> P e. A )
37 simprl 
 |-  ( ( ph /\ ( -. P ( le ` K ) W /\ Q ( le ` K ) W ) ) -> -. P ( le ` K ) W )
38 36 37 jca 
 |-  ( ( ph /\ ( -. P ( le ` K ) W /\ Q ( le ` K ) W ) ) -> ( P e. A /\ -. P ( le ` K ) W ) )
39 19 10 1 2 3 4 5 6 30 35 38 dihjatc 
 |-  ( ( ph /\ ( -. P ( le ` K ) W /\ Q ( le ` K ) W ) ) -> ( I ` ( Q .\/ P ) ) = ( ( I ` Q ) .(+) ( I ` P ) ) )
40 7 simpld 
 |-  ( ph -> K e. HL )
41 2 3 hlatjcom 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) = ( Q .\/ P ) )
42 40 8 9 41 syl3anc 
 |-  ( ph -> ( P .\/ Q ) = ( Q .\/ P ) )
43 42 fveq2d 
 |-  ( ph -> ( I ` ( P .\/ Q ) ) = ( I ` ( Q .\/ P ) ) )
44 43 adantr 
 |-  ( ( ph /\ ( -. P ( le ` K ) W /\ Q ( le ` K ) W ) ) -> ( I ` ( P .\/ Q ) ) = ( I ` ( Q .\/ P ) ) )
45 1 4 7 dvhlmod 
 |-  ( ph -> U e. LMod )
46 lmodabl 
 |-  ( U e. LMod -> U e. Abel )
47 45 46 syl 
 |-  ( ph -> U e. Abel )
48 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
49 48 lsssssubg 
 |-  ( U e. LMod -> ( LSubSp ` U ) C_ ( SubGrp ` U ) )
50 45 49 syl 
 |-  ( ph -> ( LSubSp ` U ) C_ ( SubGrp ` U ) )
51 19 1 6 4 48 dihlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ P e. ( Base ` K ) ) -> ( I ` P ) e. ( LSubSp ` U ) )
52 7 22 51 syl2anc 
 |-  ( ph -> ( I ` P ) e. ( LSubSp ` U ) )
53 50 52 sseldd 
 |-  ( ph -> ( I ` P ) e. ( SubGrp ` U ) )
54 19 1 6 4 48 dihlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Q e. ( Base ` K ) ) -> ( I ` Q ) e. ( LSubSp ` U ) )
55 7 32 54 syl2anc 
 |-  ( ph -> ( I ` Q ) e. ( LSubSp ` U ) )
56 50 55 sseldd 
 |-  ( ph -> ( I ` Q ) e. ( SubGrp ` U ) )
57 5 lsmcom 
 |-  ( ( U e. Abel /\ ( I ` P ) e. ( SubGrp ` U ) /\ ( I ` Q ) e. ( SubGrp ` U ) ) -> ( ( I ` P ) .(+) ( I ` Q ) ) = ( ( I ` Q ) .(+) ( I ` P ) ) )
58 47 53 56 57 syl3anc 
 |-  ( ph -> ( ( I ` P ) .(+) ( I ` Q ) ) = ( ( I ` Q ) .(+) ( I ` P ) ) )
59 58 adantr 
 |-  ( ( ph /\ ( -. P ( le ` K ) W /\ Q ( le ` K ) W ) ) -> ( ( I ` P ) .(+) ( I ` Q ) ) = ( ( I ` Q ) .(+) ( I ` P ) ) )
60 39 44 59 3eqtr4d 
 |-  ( ( ph /\ ( -. P ( le ` K ) W /\ Q ( le ` K ) W ) ) -> ( I ` ( P .\/ Q ) ) = ( ( I ` P ) .(+) ( I ` Q ) ) )
61 7 adantr 
 |-  ( ( ph /\ ( -. P ( le ` K ) W /\ -. Q ( le ` K ) W ) ) -> ( K e. HL /\ W e. H ) )
62 8 adantr 
 |-  ( ( ph /\ ( -. P ( le ` K ) W /\ -. Q ( le ` K ) W ) ) -> P e. A )
63 simprl 
 |-  ( ( ph /\ ( -. P ( le ` K ) W /\ -. Q ( le ` K ) W ) ) -> -. P ( le ` K ) W )
64 62 63 jca 
 |-  ( ( ph /\ ( -. P ( le ` K ) W /\ -. Q ( le ` K ) W ) ) -> ( P e. A /\ -. P ( le ` K ) W ) )
65 9 adantr 
 |-  ( ( ph /\ ( -. P ( le ` K ) W /\ -. Q ( le ` K ) W ) ) -> Q e. A )
66 simprr 
 |-  ( ( ph /\ ( -. P ( le ` K ) W /\ -. Q ( le ` K ) W ) ) -> -. Q ( le ` K ) W )
67 65 66 jca 
 |-  ( ( ph /\ ( -. P ( le ` K ) W /\ -. Q ( le ` K ) W ) ) -> ( Q e. A /\ -. Q ( le ` K ) W ) )
68 10 1 2 3 4 5 6 61 64 67 dihjatcc 
 |-  ( ( ph /\ ( -. P ( le ` K ) W /\ -. Q ( le ` K ) W ) ) -> ( I ` ( P .\/ Q ) ) = ( ( I ` P ) .(+) ( I ` Q ) ) )
69 18 29 60 68 4casesdan 
 |-  ( ph -> ( I ` ( P .\/ Q ) ) = ( ( I ` P ) .(+) ( I ` Q ) ) )