Metamath Proof Explorer

Theorem dihjat5N

Description: Transfer lattice join with atom to subspace sum. (Contributed by NM, 25-Apr-2015) (New usage is discouraged.)

Ref Expression
Hypotheses dihjat5.b ⊢B=BaseK
dihjat5.h ⊢H=LHyp⁡K
dihjat5.j ⊢∨˙=join⁡K
dihjat5.a ⊢A=Atoms⁡K
dihjat5.u ⊢U=DVecH⁡K⁡W
dihjat5.s ⊢⊕˙=LSSum⁡U
dihjat5.i ⊢I=DIsoH⁡K⁡W
dihjat5.k ⊢φ→K∈HL∧W∈H
dihjat5.x ⊢φ→X∈B
dihjat5.p ⊢φ→P∈A
Assertion dihjat5N ⊢φ→X∨˙P=I-1⁡I⁡X⊕˙I⁡P

Proof

Step Hyp Ref Expression
1 dihjat5.b ⊢B=BaseK
2 dihjat5.h ⊢H=LHyp⁡K
3 dihjat5.j ⊢∨˙=join⁡K
4 dihjat5.a ⊢A=Atoms⁡K
5 dihjat5.u ⊢U=DVecH⁡K⁡W
6 dihjat5.s ⊢⊕˙=LSSum⁡U
7 dihjat5.i ⊢I=DIsoH⁡K⁡W
8 dihjat5.k ⊢φ→K∈HL∧W∈H
9 dihjat5.x ⊢φ→X∈B
10 dihjat5.p ⊢φ→P∈A
11 1 2 3 4 5 6 7 8 9 10 dihjat3 ⊢φ→I⁡X∨˙P=I⁡X⊕˙I⁡P
12 eqid ⊢LSAtoms⁡U=LSAtoms⁡U
13 1 2 7 dihcl ⊢K∈HL∧W∈H∧X∈B→I⁡X∈ran⁡I
14 8 9 13 syl2anc ⊢φ→I⁡X∈ran⁡I
15 4 2 5 7 12 dihatlat ⊢K∈HL∧W∈H∧P∈A→I⁡P∈LSAtoms⁡U
16 8 10 15 syl2anc ⊢φ→I⁡P∈LSAtoms⁡U
17 2 7 5 6 12 8 14 16 dihsmatrn ⊢φ→I⁡X⊕˙I⁡P∈ran⁡I
18 2 7 dihcnvid2 ⊢K∈HL∧W∈H∧I⁡X⊕˙I⁡P∈ran⁡I→I⁡I-1⁡I⁡X⊕˙I⁡P=I⁡X⊕˙I⁡P
19 8 17 18 syl2anc ⊢φ→I⁡I-1⁡I⁡X⊕˙I⁡P=I⁡X⊕˙I⁡P
20 11 19 eqtr4d ⊢φ→I⁡X∨˙P=I⁡I-1⁡I⁡X⊕˙I⁡P
21 8 simpld ⊢φ→K∈HL
22 21 hllatd ⊢φ→K∈Lat
23 1 4 atbase ⊢P∈A→P∈B
24 10 23 syl ⊢φ→P∈B
25 1 3 latjcl ⊢K∈Lat∧X∈B∧P∈B→X∨˙P∈B
26 22 9 24 25 syl3anc ⊢φ→X∨˙P∈B
27 1 2 7 dihcnvcl ⊢K∈HL∧W∈H∧I⁡X⊕˙I⁡P∈ran⁡I→I-1⁡I⁡X⊕˙I⁡P∈B
28 8 17 27 syl2anc ⊢φ→I-1⁡I⁡X⊕˙I⁡P∈B
29 1 2 7 dih11 ⊢K∈HL∧W∈H∧X∨˙P∈B∧I-1⁡I⁡X⊕˙I⁡P∈B→I⁡X∨˙P=I⁡I-1⁡I⁡X⊕˙I⁡P↔X∨˙P=I-1⁡I⁡X⊕˙I⁡P
30 8 26 28 29 syl3anc ⊢φ→I⁡X∨˙P=I⁡I-1⁡I⁡X⊕˙I⁡P↔X∨˙P=I-1⁡I⁡X⊕˙I⁡P
31 20 30 mpbid ⊢φ→X∨˙P=I-1⁡I⁡X⊕˙I⁡P