# 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}={\mathrm{Base}}_{{K}}$
dihjatc1.l
dihjatc1.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dihjatc1.j
dihjatc1.m
dihjatc1.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
dihjatc1.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dihjatc1.s
dihjatc1.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
Assertion dihjatc3

### Proof

Step Hyp Ref Expression
1 dihjatc1.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 dihjatc1.l
3 dihjatc1.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
4 dihjatc1.j
5 dihjatc1.m
6 dihjatc1.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
7 dihjatc1.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
8 dihjatc1.s
9 dihjatc1.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
10 1 2 3 4 5 6 7 8 9 dihjatc1
11 simp11
12 3 7 11 dvhlmod
13 lmodabl ${⊢}{U}\in \mathrm{LMod}\to {U}\in \mathrm{Abel}$
14 12 13 syl
15 eqid ${⊢}\mathrm{LSubSp}\left({U}\right)=\mathrm{LSubSp}\left({U}\right)$
16 15 lsssssubg ${⊢}{U}\in \mathrm{LMod}\to \mathrm{LSubSp}\left({U}\right)\subseteq \mathrm{SubGrp}\left({U}\right)$
17 12 16 syl
18 simp11l
19 18 hllatd
20 simp12
21 simp13
22 1 5 latmcl
23 19 20 21 22 syl3anc
24 1 3 9 7 15 dihlss
25 11 23 24 syl2anc
26 17 25 sseldd
27 simp2l
28 1 6 atbase ${⊢}{Q}\in {A}\to {Q}\in {B}$
29 27 28 syl
30 1 3 9 7 15 dihlss ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {Q}\in {B}\right)\to {I}\left({Q}\right)\in \mathrm{LSubSp}\left({U}\right)$
31 11 29 30 syl2anc
32 17 31 sseldd
33 8 lsmcom
34 14 26 32 33 syl3anc
35 10 34 eqtr4d