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 ) ) )