Metamath Proof Explorer


Theorem elpadd

Description: Member of a projective subspace sum. (Contributed by NM, 29-Dec-2011)

Ref Expression
Hypotheses paddfval.l ˙ = K
paddfval.j ˙ = join K
paddfval.a A = Atoms K
paddfval.p + ˙ = + 𝑃 K
Assertion elpadd K B X A Y A S X + ˙ Y S X S Y S A q X r Y S ˙ 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 paddval K B X A Y A X + ˙ Y = X Y p A | q X r Y p ˙ q ˙ r
6 5 eleq2d K B X A Y A S X + ˙ Y S X Y p A | q X r Y p ˙ q ˙ r
7 elun S X Y p A | q X r Y p ˙ q ˙ r S X Y S p A | q X r Y p ˙ q ˙ r
8 elun S X Y S X S Y
9 breq1 p = S p ˙ q ˙ r S ˙ q ˙ r
10 9 2rexbidv p = S q X r Y p ˙ q ˙ r q X r Y S ˙ q ˙ r
11 10 elrab S p A | q X r Y p ˙ q ˙ r S A q X r Y S ˙ q ˙ r
12 8 11 orbi12i S X Y S p A | q X r Y p ˙ q ˙ r S X S Y S A q X r Y S ˙ q ˙ r
13 7 12 bitri S X Y p A | q X r Y p ˙ q ˙ r S X S Y S A q X r Y S ˙ q ˙ r
14 6 13 bitrdi K B X A Y A S X + ˙ Y S X S Y S A q X r Y S ˙ q ˙ r