# Metamath Proof Explorer

## Theorem dihjatc3

Description: Isomorphism H of join with an atom. (Contributed by NM, 26-Aug-2014)

Ref Expression
Hypotheses dihjatc1.b
`|- B = ( Base ` K )`
dihjatc1.l
`|- .<_ = ( le ` K )`
dihjatc1.h
`|- H = ( LHyp ` K )`
dihjatc1.j
`|- .\/ = ( join ` K )`
dihjatc1.m
`|- ./\ = ( meet ` K )`
dihjatc1.a
`|- A = ( Atoms ` K )`
dihjatc1.u
`|- U = ( ( DVecH ` K ) ` W )`
dihjatc1.s
`|- .(+) = ( LSSum ` U )`
dihjatc1.i
`|- I = ( ( DIsoH ` K ) ` W )`
Assertion dihjatc3
`|- ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> ( I ` ( ( X ./\ Y ) .\/ Q ) ) = ( ( I ` ( X ./\ Y ) ) .(+) ( I ` Q ) ) )`

### Proof

Step Hyp Ref Expression
1 dihjatc1.b
` |-  B = ( Base ` K )`
2 dihjatc1.l
` |-  .<_ = ( le ` K )`
3 dihjatc1.h
` |-  H = ( LHyp ` K )`
4 dihjatc1.j
` |-  .\/ = ( join ` K )`
5 dihjatc1.m
` |-  ./\ = ( meet ` K )`
6 dihjatc1.a
` |-  A = ( Atoms ` K )`
7 dihjatc1.u
` |-  U = ( ( DVecH ` K ) ` W )`
8 dihjatc1.s
` |-  .(+) = ( LSSum ` U )`
9 dihjatc1.i
` |-  I = ( ( DIsoH ` K ) ` W )`
10 1 2 3 4 5 6 7 8 9 dihjatc1
` |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> ( I ` ( ( X ./\ Y ) .\/ Q ) ) = ( ( I ` Q ) .(+) ( I ` ( X ./\ Y ) ) ) )`
11 simp11
` |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> ( K e. HL /\ W e. H ) )`
12 3 7 11 dvhlmod
` |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> U e. LMod )`
13 lmodabl
` |-  ( U e. LMod -> U e. Abel )`
14 12 13 syl
` |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> U e. Abel )`
15 eqid
` |-  ( LSubSp ` U ) = ( LSubSp ` U )`
16 15 lsssssubg
` |-  ( U e. LMod -> ( LSubSp ` U ) C_ ( SubGrp ` U ) )`
17 12 16 syl
` |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> ( LSubSp ` U ) C_ ( SubGrp ` U ) )`
18 simp11l
` |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> K e. HL )`
19 18 hllatd
` |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> K e. Lat )`
20 simp12
` |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> X e. B )`
21 simp13
` |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> Y e. B )`
22 1 5 latmcl
` |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) e. B )`
23 19 20 21 22 syl3anc
` |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> ( X ./\ Y ) e. B )`
24 1 3 9 7 15 dihlss
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( X ./\ Y ) e. B ) -> ( I ` ( X ./\ Y ) ) e. ( LSubSp ` U ) )`
25 11 23 24 syl2anc
` |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> ( I ` ( X ./\ Y ) ) e. ( LSubSp ` U ) )`
26 17 25 sseldd
` |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> ( I ` ( X ./\ Y ) ) e. ( SubGrp ` U ) )`
27 simp2l
` |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> Q e. A )`
28 1 6 atbase
` |-  ( Q e. A -> Q e. B )`
29 27 28 syl
` |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> Q e. B )`
30 1 3 9 7 15 dihlss
` |-  ( ( ( K e. HL /\ W e. H ) /\ Q e. B ) -> ( I ` Q ) e. ( LSubSp ` U ) )`
31 11 29 30 syl2anc
` |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> ( I ` Q ) e. ( LSubSp ` U ) )`
32 17 31 sseldd
` |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> ( I ` Q ) e. ( SubGrp ` U ) )`
33 8 lsmcom
` |-  ( ( U e. Abel /\ ( I ` ( X ./\ Y ) ) e. ( SubGrp ` U ) /\ ( I ` Q ) e. ( SubGrp ` U ) ) -> ( ( I ` ( X ./\ Y ) ) .(+) ( I ` Q ) ) = ( ( I ` Q ) .(+) ( I ` ( X ./\ Y ) ) ) )`
34 14 26 32 33 syl3anc
` |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> ( ( I ` ( X ./\ Y ) ) .(+) ( I ` Q ) ) = ( ( I ` Q ) .(+) ( I ` ( X ./\ Y ) ) ) )`
35 10 34 eqtr4d
` |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( Q .<_ X /\ ( X ./\ Y ) .<_ W ) ) -> ( I ` ( ( X ./\ Y ) .\/ Q ) ) = ( ( I ` ( X ./\ Y ) ) .(+) ( I ` Q ) ) )`