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 = Base K
pmapfval.l ˙ = K
pmapfval.a A = Atoms K
pmapfval.m M = pmap K
Assertion pmapfval K C M = x B a A | a ˙ x

Proof

Step Hyp Ref Expression
1 pmapfval.b B = Base K
2 pmapfval.l ˙ = K
3 pmapfval.a A = Atoms K
4 pmapfval.m M = pmap K
5 elex K C K V
6 fveq2 k = K Base k = Base K
7 6 1 eqtr4di k = K Base k = B
8 fveq2 k = K Atoms k = Atoms K
9 8 3 eqtr4di k = K Atoms k = A
10 fveq2 k = K k = K
11 10 2 eqtr4di k = K k = ˙
12 11 breqd k = K a k x a ˙ x
13 9 12 rabeqbidv k = K a Atoms k | a k x = a A | a ˙ x
14 7 13 mpteq12dv k = K x Base k a Atoms k | a k x = x B a A | a ˙ x
15 df-pmap pmap = k V x Base k a Atoms k | a k x
16 14 15 1 mptfvmpt K V pmap K = x B a A | a ˙ x
17 4 16 syl5eq K V M = x B a A | a ˙ x
18 5 17 syl K C M = x B a A | a ˙ x