Metamath Proof Explorer

Theorem djhljjN

Description: Lattice join in terms of DVecH vector space closed subspace join. (Contributed by NM, 17-Aug-2014) (New usage is discouraged.)

Ref Expression
Hypotheses djhlj.b ⊢B=BaseK
djhlj.k ⊢∨˙=join⁡K
djhlj.h ⊢H=LHyp⁡K
djhlj.i ⊢I=DIsoH⁡K⁡W
djhlj.j ⊢J=joinH⁡K⁡W
djhljj.w ⊢φ→K∈HL∧W∈H
djhljj.x ⊢φ→X∈B
djhljj.y ⊢φ→Y∈B
Assertion djhljjN ⊢φ→X∨˙Y=I-1⁡I⁡XJI⁡Y

Proof

Step Hyp Ref Expression
1 djhlj.b ⊢B=BaseK
2 djhlj.k ⊢∨˙=join⁡K
3 djhlj.h ⊢H=LHyp⁡K
4 djhlj.i ⊢I=DIsoH⁡K⁡W
5 djhlj.j ⊢J=joinH⁡K⁡W
6 djhljj.w ⊢φ→K∈HL∧W∈H
7 djhljj.x ⊢φ→X∈B
8 djhljj.y ⊢φ→Y∈B
9 1 2 3 4 5 djhlj ⊢K∈HL∧W∈H∧X∈B∧Y∈B→I⁡X∨˙Y=I⁡XJI⁡Y
10 6 7 8 9 syl12anc ⊢φ→I⁡X∨˙Y=I⁡XJI⁡Y
11 1 3 4 dihcl ⊢K∈HL∧W∈H∧X∈B→I⁡X∈ran⁡I
12 6 7 11 syl2anc ⊢φ→I⁡X∈ran⁡I
13 eqid ⊢DVecH⁡K⁡W=DVecH⁡K⁡W
14 eqid ⊢BaseDVecH⁡K⁡W=BaseDVecH⁡K⁡W
15 3 13 4 14 dihrnss ⊢K∈HL∧W∈H∧I⁡X∈ran⁡I→I⁡X⊆BaseDVecH⁡K⁡W
16 6 12 15 syl2anc ⊢φ→I⁡X⊆BaseDVecH⁡K⁡W
17 1 3 4 dihcl ⊢K∈HL∧W∈H∧Y∈B→I⁡Y∈ran⁡I
18 6 8 17 syl2anc ⊢φ→I⁡Y∈ran⁡I
19 3 13 4 14 dihrnss ⊢K∈HL∧W∈H∧I⁡Y∈ran⁡I→I⁡Y⊆BaseDVecH⁡K⁡W
20 6 18 19 syl2anc ⊢φ→I⁡Y⊆BaseDVecH⁡K⁡W
21 3 4 13 14 5 djhcl ⊢K∈HL∧W∈H∧I⁡X⊆BaseDVecH⁡K⁡W∧I⁡Y⊆BaseDVecH⁡K⁡W→I⁡XJI⁡Y∈ran⁡I
22 6 16 20 21 syl12anc ⊢φ→I⁡XJI⁡Y∈ran⁡I
23 3 4 dihcnvid2 ⊢K∈HL∧W∈H∧I⁡XJI⁡Y∈ran⁡I→I⁡I-1⁡I⁡XJI⁡Y=I⁡XJI⁡Y
24 6 22 23 syl2anc ⊢φ→I⁡I-1⁡I⁡XJI⁡Y=I⁡XJI⁡Y
25 10 24 eqtr4d ⊢φ→I⁡X∨˙Y=I⁡I-1⁡I⁡XJI⁡Y
26 6 simpld ⊢φ→K∈HL
27 26 hllatd ⊢φ→K∈Lat
28 1 2 latjcl ⊢K∈Lat∧X∈B∧Y∈B→X∨˙Y∈B
29 27 7 8 28 syl3anc ⊢φ→X∨˙Y∈B
30 1 3 4 dihcnvcl ⊢K∈HL∧W∈H∧I⁡XJI⁡Y∈ran⁡I→I-1⁡I⁡XJI⁡Y∈B
31 6 22 30 syl2anc ⊢φ→I-1⁡I⁡XJI⁡Y∈B
32 1 3 4 dih11 ⊢K∈HL∧W∈H∧X∨˙Y∈B∧I-1⁡I⁡XJI⁡Y∈B→I⁡X∨˙Y=I⁡I-1⁡I⁡XJI⁡Y↔X∨˙Y=I-1⁡I⁡XJI⁡Y
33 6 29 31 32 syl3anc ⊢φ→I⁡X∨˙Y=I⁡I-1⁡I⁡XJI⁡Y↔X∨˙Y=I-1⁡I⁡XJI⁡Y
34 25 33 mpbid ⊢φ→X∨˙Y=I-1⁡I⁡XJI⁡Y