Metamath Proof Explorer


Theorem paddvaln0N

Description: Projective subspace sum operation value for nonempty sets. (Contributed by NM, 27-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses paddfval.l ˙ = K
paddfval.j ˙ = join K
paddfval.a A = Atoms K
paddfval.p + ˙ = + 𝑃 K
Assertion paddvaln0N K Lat X A Y A X Y X + ˙ Y = p A | q X r Y p ˙ q ˙ r

Proof

Step Hyp Ref Expression
1 paddfval.l ˙ = K
2 paddfval.j ˙ = join K
3 paddfval.a A = Atoms K
4 paddfval.p + ˙ = + 𝑃 K
5 1 2 3 4 elpaddn0 K Lat X A Y A X Y s X + ˙ Y s A q X r Y s ˙ q ˙ r
6 breq1 p = s p ˙ q ˙ r s ˙ q ˙ r
7 6 2rexbidv p = s q X r Y p ˙ q ˙ r q X r Y s ˙ q ˙ r
8 7 elrab s p A | q X r Y p ˙ q ˙ r s A q X r Y s ˙ q ˙ r
9 5 8 bitr4di K Lat X A Y A X Y s X + ˙ Y s p A | q X r Y p ˙ q ˙ r
10 9 eqrdv K Lat X A Y A X Y X + ˙ Y = p A | q X r Y p ˙ q ˙ r