Metamath Proof Explorer


Theorem pmaplubN

Description: The LUB of a projective map is the projective map's argument. (Contributed by NM, 13-Mar-2012) (New usage is discouraged.)

Ref Expression
Hypotheses pmaplub.b B = Base K
pmaplub.u U = lub K
pmaplub.m M = pmap K
Assertion pmaplubN K HL X B U M X = X

Proof

Step Hyp Ref Expression
1 pmaplub.b B = Base K
2 pmaplub.u U = lub K
3 pmaplub.m M = pmap K
4 eqid K = K
5 eqid Atoms K = Atoms K
6 1 4 5 3 pmapval K HL X B M X = p Atoms K | p K X
7 6 fveq2d K HL X B U M X = U p Atoms K | p K X
8 hlomcmat K HL K OML K CLat K AtLat
9 1 4 2 5 atlatmstc K OML K CLat K AtLat X B U p Atoms K | p K X = X
10 8 9 sylan K HL X B U p Atoms K | p K X = X
11 7 10 eqtrd K HL X B U M X = X