Metamath Proof Explorer

Theorem dihjatcclem1

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=LHyp⁡K
dihjatcclem.j ⊢∨˙=join⁡K
dihjatcclem.m ⊢∧˙=meet⁡K
dihjatcclem.a ⊢A=Atoms⁡K
dihjatcclem.u ⊢U=DVecH⁡K⁡W
dihjatcclem.s ⊢⊕˙=LSSum⁡U
dihjatcclem.i ⊢I=DIsoH⁡K⁡W
dihjatcclem.v ⊢V=P∨˙Q∧˙W
dihjatcclem.k ⊢φ→K∈HL∧W∈H
dihjatcclem.p ⊢φ→P∈A∧¬P≤˙W
dihjatcclem.q ⊢φ→Q∈A∧¬Q≤˙W
Assertion dihjatcclem1 ⊢φ→I⁡P∨˙Q=I⁡P⊕˙I⁡Q⊕˙I⁡V

Proof

Step Hyp Ref Expression
1 dihjatcclem.b ⊢B=BaseK
2 dihjatcclem.l ⊢≤˙=≤K
3 dihjatcclem.h ⊢H=LHyp⁡K
4 dihjatcclem.j ⊢∨˙=join⁡K
5 dihjatcclem.m ⊢∧˙=meet⁡K
6 dihjatcclem.a ⊢A=Atoms⁡K
7 dihjatcclem.u ⊢U=DVecH⁡K⁡W
8 dihjatcclem.s ⊢⊕˙=LSSum⁡U
9 dihjatcclem.i ⊢I=DIsoH⁡K⁡W
10 dihjatcclem.v ⊢V=P∨˙Q∧˙W
11 dihjatcclem.k ⊢φ→K∈HL∧W∈H
12 dihjatcclem.p ⊢φ→P∈A∧¬P≤˙W
13 dihjatcclem.q ⊢φ→Q∈A∧¬Q≤˙W
14 3 7 11 dvhlmod ⊢φ→U∈LMod
15 lmodabl ⊢U∈LMod→U∈Abel
16 14 15 syl ⊢φ→U∈Abel
17 eqid ⊢LSubSp⁡U=LSubSp⁡U
18 17 lsssssubg ⊢U∈LMod→LSubSp⁡U⊆SubGrp⁡U
19 14 18 syl ⊢φ→LSubSp⁡U⊆SubGrp⁡U
20 12 simpld ⊢φ→P∈A
21 1 6 atbase ⊢P∈A→P∈B
22 20 21 syl ⊢φ→P∈B
23 1 3 9 7 17 dihlss ⊢K∈HL∧W∈H∧P∈B→I⁡P∈LSubSp⁡U
24 11 22 23 syl2anc ⊢φ→I⁡P∈LSubSp⁡U
25 19 24 sseldd ⊢φ→I⁡P∈SubGrp⁡U
26 11 simpld ⊢φ→K∈HL
27 26 hllatd ⊢φ→K∈Lat
28 13 simpld ⊢φ→Q∈A
29 1 4 6 hlatjcl ⊢K∈HL∧P∈A∧Q∈A→P∨˙Q∈B
30 26 20 28 29 syl3anc ⊢φ→P∨˙Q∈B
31 11 simprd ⊢φ→W∈H
32 1 3 lhpbase ⊢W∈H→W∈B
33 31 32 syl ⊢φ→W∈B
34 1 5 latmcl ⊢K∈Lat∧P∨˙Q∈B∧W∈B→P∨˙Q∧˙W∈B
35 27 30 33 34 syl3anc ⊢φ→P∨˙Q∧˙W∈B
36 10 35 eqeltrid ⊢φ→V∈B
37 1 3 9 7 17 dihlss ⊢K∈HL∧W∈H∧V∈B→I⁡V∈LSubSp⁡U
38 11 36 37 syl2anc ⊢φ→I⁡V∈LSubSp⁡U
39 19 38 sseldd ⊢φ→I⁡V∈SubGrp⁡U
40 1 6 atbase ⊢Q∈A→Q∈B
41 28 40 syl ⊢φ→Q∈B
42 1 3 9 7 17 dihlss ⊢K∈HL∧W∈H∧Q∈B→I⁡Q∈LSubSp⁡U
43 11 41 42 syl2anc ⊢φ→I⁡Q∈LSubSp⁡U
44 19 43 sseldd ⊢φ→I⁡Q∈SubGrp⁡U
45 8 lsm4 ⊢U∈Abel∧I⁡P∈SubGrp⁡U∧I⁡V∈SubGrp⁡U∧I⁡Q∈SubGrp⁡U∧I⁡V∈SubGrp⁡U→I⁡P⊕˙I⁡V⊕˙I⁡Q⊕˙I⁡V=I⁡P⊕˙I⁡Q⊕˙I⁡V⊕˙I⁡V
46 16 25 39 44 39 45 syl122anc ⊢φ→I⁡P⊕˙I⁡V⊕˙I⁡Q⊕˙I⁡V=I⁡P⊕˙I⁡Q⊕˙I⁡V⊕˙I⁡V
47 13 simprd ⊢φ→¬Q≤˙W
48 47 intnand ⊢φ→¬P≤˙W∧Q≤˙W
49 1 2 4 latjle12 ⊢K∈Lat∧P∈B∧Q∈B∧W∈B→P≤˙W∧Q≤˙W↔P∨˙Q≤˙W
50 27 22 41 33 49 syl13anc ⊢φ→P≤˙W∧Q≤˙W↔P∨˙Q≤˙W
51 48 50 mtbid ⊢φ→¬P∨˙Q≤˙W
52 2 4 6 hlatlej1 ⊢K∈HL∧P∈A∧Q∈A→P≤˙P∨˙Q
53 26 20 28 52 syl3anc ⊢φ→P≤˙P∨˙Q
54 1 2 4 5 6 3 9 7 8 dihvalcq2 ⊢K∈HL∧W∈H∧P∨˙Q∈B∧¬P∨˙Q≤˙W∧P∈A∧¬P≤˙W∧P≤˙P∨˙Q→I⁡P∨˙Q=I⁡P⊕˙I⁡P∨˙Q∧˙W
55 11 30 51 12 53 54 syl122anc ⊢φ→I⁡P∨˙Q=I⁡P⊕˙I⁡P∨˙Q∧˙W
56 10 fveq2i ⊢I⁡V=I⁡P∨˙Q∧˙W
57 56 oveq2i ⊢I⁡P⊕˙I⁡V=I⁡P⊕˙I⁡P∨˙Q∧˙W
58 55 57 eqtr4di ⊢φ→I⁡P∨˙Q=I⁡P⊕˙I⁡V
59 2 4 6 hlatlej2 ⊢K∈HL∧P∈A∧Q∈A→Q≤˙P∨˙Q
60 26 20 28 59 syl3anc ⊢φ→Q≤˙P∨˙Q
61 1 2 4 5 6 3 9 7 8 dihvalcq2 ⊢K∈HL∧W∈H∧P∨˙Q∈B∧¬P∨˙Q≤˙W∧Q∈A∧¬Q≤˙W∧Q≤˙P∨˙Q→I⁡P∨˙Q=I⁡Q⊕˙I⁡P∨˙Q∧˙W
62 11 30 51 13 60 61 syl122anc ⊢φ→I⁡P∨˙Q=I⁡Q⊕˙I⁡P∨˙Q∧˙W
63 56 oveq2i ⊢I⁡Q⊕˙I⁡V=I⁡Q⊕˙I⁡P∨˙Q∧˙W
64 62 63 eqtr4di ⊢φ→I⁡P∨˙Q=I⁡Q⊕˙I⁡V
65 58 64 oveq12d ⊢φ→I⁡P∨˙Q⊕˙I⁡P∨˙Q=I⁡P⊕˙I⁡V⊕˙I⁡Q⊕˙I⁡V
66 1 3 9 7 17 dihlss ⊢K∈HL∧W∈H∧P∨˙Q∈B→I⁡P∨˙Q∈LSubSp⁡U
67 11 30 66 syl2anc ⊢φ→I⁡P∨˙Q∈LSubSp⁡U
68 19 67 sseldd ⊢φ→I⁡P∨˙Q∈SubGrp⁡U
69 8 lsmidm ⊢I⁡P∨˙Q∈SubGrp⁡U→I⁡P∨˙Q⊕˙I⁡P∨˙Q=I⁡P∨˙Q
70 68 69 syl ⊢φ→I⁡P∨˙Q⊕˙I⁡P∨˙Q=I⁡P∨˙Q
71 65 70 eqtr3d ⊢φ→I⁡P⊕˙I⁡V⊕˙I⁡Q⊕˙I⁡V=I⁡P∨˙Q
72 8 lsmidm ⊢I⁡V∈SubGrp⁡U→I⁡V⊕˙I⁡V=I⁡V
73 39 72 syl ⊢φ→I⁡V⊕˙I⁡V=I⁡V
74 73 oveq2d ⊢φ→I⁡P⊕˙I⁡Q⊕˙I⁡V⊕˙I⁡V=I⁡P⊕˙I⁡Q⊕˙I⁡V
75 46 71 74 3eqtr3d ⊢φ→I⁡P∨˙Q=I⁡P⊕˙I⁡Q⊕˙I⁡V