Metamath Proof Explorer


Theorem pmapfval

Description: The projective map of a Hilbert lattice. (Contributed by NM, 2-Oct-2011)

Ref Expression
Hypotheses pmapfval.b B=BaseK
pmapfval.l ˙=K
pmapfval.a A=AtomsK
pmapfval.m M=pmapK
Assertion pmapfval KCM=xBaA|a˙x

Proof

Step Hyp Ref Expression
1 pmapfval.b B=BaseK
2 pmapfval.l ˙=K
3 pmapfval.a A=AtomsK
4 pmapfval.m M=pmapK
5 elex KCKV
6 fveq2 k=KBasek=BaseK
7 6 1 eqtr4di k=KBasek=B
8 fveq2 k=KAtomsk=AtomsK
9 8 3 eqtr4di k=KAtomsk=A
10 fveq2 k=Kk=K
11 10 2 eqtr4di k=Kk=˙
12 11 breqd k=Kakxa˙x
13 9 12 rabeqbidv k=KaAtomsk|akx=aA|a˙x
14 7 13 mpteq12dv k=KxBasekaAtomsk|akx=xBaA|a˙x
15 df-pmap pmap=kVxBasekaAtomsk|akx
16 14 15 1 mptfvmpt KVpmapK=xBaA|a˙x
17 4 16 eqtrid KVM=xBaA|a˙x
18 5 17 syl KCM=xBaA|a˙x