Metamath Proof Explorer


Theorem diaocN

Description: Value of partial isomorphism A at lattice orthocomplement (using a Sasaki projection to get orthocomplement relative to the fiducial co-atom W ). (Contributed by NM, 6-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses diaoc.j ˙=joinK
diaoc.m ˙=meetK
diaoc.o ˙=ocK
diaoc.h H=LHypK
diaoc.t T=LTrnKW
diaoc.i I=DIsoAKW
diaoc.n N=ocAKW
Assertion diaocN KHLWHXdomII˙X˙˙W˙W=NIX

Proof

Step Hyp Ref Expression
1 diaoc.j ˙=joinK
2 diaoc.m ˙=meetK
3 diaoc.o ˙=ocK
4 diaoc.h H=LHypK
5 diaoc.t T=LTrnKW
6 diaoc.i I=DIsoAKW
7 diaoc.n N=ocAKW
8 simpl KHLWHXdomIKHLWH
9 eqid BaseK=BaseK
10 9 4 6 diadmclN KHLWHXdomIXBaseK
11 eqid K=K
12 11 4 6 diadmleN KHLWHXdomIXKW
13 9 11 4 5 6 diass KHLWHXBaseKXKWIXT
14 8 10 12 13 syl12anc KHLWHXdomIIXT
15 1 2 3 4 5 6 7 docavalN KHLWHIXTNIX=I˙I-1zranI|IXz˙˙W˙W
16 14 15 syldan KHLWHXdomINIX=I˙I-1zranI|IXz˙˙W˙W
17 4 6 diaclN KHLWHXdomIIXranI
18 intmin IXranIzranI|IXz=IX
19 17 18 syl KHLWHXdomIzranI|IXz=IX
20 19 fveq2d KHLWHXdomII-1zranI|IXz=I-1IX
21 4 6 diaf11N KHLWHI:domI1-1 ontoranI
22 f1ocnvfv1 I:domI1-1 ontoranIXdomII-1IX=X
23 21 22 sylan KHLWHXdomII-1IX=X
24 20 23 eqtrd KHLWHXdomII-1zranI|IXz=X
25 24 fveq2d KHLWHXdomI˙I-1zranI|IXz=˙X
26 25 oveq1d KHLWHXdomI˙I-1zranI|IXz˙˙W=˙X˙˙W
27 26 fvoveq1d KHLWHXdomII˙I-1zranI|IXz˙˙W˙W=I˙X˙˙W˙W
28 16 27 eqtr2d KHLWHXdomII˙X˙˙W˙W=NIX