Metamath Proof Explorer


Theorem dihjatcclem2

Description: Lemma for isomorphism H of lattice join of two atoms not under the fiducial hyperplane. (Contributed by NM, 26-Sep-2014)

Ref Expression
Hypotheses dihjatcclem.b B=BaseK
dihjatcclem.l ˙=K
dihjatcclem.h H=LHypK
dihjatcclem.j ˙=joinK
dihjatcclem.m ˙=meetK
dihjatcclem.a A=AtomsK
dihjatcclem.u U=DVecHKW
dihjatcclem.s ˙=LSSumU
dihjatcclem.i I=DIsoHKW
dihjatcclem.v V=P˙Q˙W
dihjatcclem.k φKHLWH
dihjatcclem.p φPA¬P˙W
dihjatcclem.q φQA¬Q˙W
dihjatcclem2.c φIVIP˙IQ
Assertion dihjatcclem2 φIP˙Q=IP˙IQ

Proof

Step Hyp Ref Expression
1 dihjatcclem.b B=BaseK
2 dihjatcclem.l ˙=K
3 dihjatcclem.h H=LHypK
4 dihjatcclem.j ˙=joinK
5 dihjatcclem.m ˙=meetK
6 dihjatcclem.a A=AtomsK
7 dihjatcclem.u U=DVecHKW
8 dihjatcclem.s ˙=LSSumU
9 dihjatcclem.i I=DIsoHKW
10 dihjatcclem.v V=P˙Q˙W
11 dihjatcclem.k φKHLWH
12 dihjatcclem.p φPA¬P˙W
13 dihjatcclem.q φQA¬Q˙W
14 dihjatcclem2.c φIVIP˙IQ
15 1 2 3 4 5 6 7 8 9 10 11 12 13 dihjatcclem1 φIP˙Q=IP˙IQ˙IV
16 3 7 11 dvhlmod φULMod
17 eqid LSubSpU=LSubSpU
18 17 lsssssubg ULModLSubSpUSubGrpU
19 16 18 syl φLSubSpUSubGrpU
20 12 simpld φPA
21 1 6 atbase PAPB
22 20 21 syl φPB
23 1 3 9 7 17 dihlss KHLWHPBIPLSubSpU
24 11 22 23 syl2anc φIPLSubSpU
25 13 simpld φQA
26 1 6 atbase QAQB
27 25 26 syl φQB
28 1 3 9 7 17 dihlss KHLWHQBIQLSubSpU
29 11 27 28 syl2anc φIQLSubSpU
30 17 8 lsmcl ULModIPLSubSpUIQLSubSpUIP˙IQLSubSpU
31 16 24 29 30 syl3anc φIP˙IQLSubSpU
32 19 31 sseldd φIP˙IQSubGrpU
33 10 fveq2i IV=IP˙Q˙W
34 11 simpld φKHL
35 34 hllatd φKLat
36 1 4 6 hlatjcl KHLPAQAP˙QB
37 34 20 25 36 syl3anc φP˙QB
38 11 simprd φWH
39 1 3 lhpbase WHWB
40 38 39 syl φWB
41 1 5 latmcl KLatP˙QBWBP˙Q˙WB
42 35 37 40 41 syl3anc φP˙Q˙WB
43 1 3 9 7 17 dihlss KHLWHP˙Q˙WBIP˙Q˙WLSubSpU
44 11 42 43 syl2anc φIP˙Q˙WLSubSpU
45 33 44 eqeltrid φIVLSubSpU
46 19 45 sseldd φIVSubGrpU
47 8 lsmss2 IP˙IQSubGrpUIVSubGrpUIVIP˙IQIP˙IQ˙IV=IP˙IQ
48 32 46 14 47 syl3anc φIP˙IQ˙IV=IP˙IQ
49 15 48 eqtrd φIP˙Q=IP˙IQ