Metamath Proof Explorer


Theorem elpadd2at2

Description: Membership in a projective subspace sum of two points. (Contributed by NM, 8-Mar-2012)

Ref Expression
Hypotheses paddfval.l ˙=K
paddfval.j ˙=joinK
paddfval.a A=AtomsK
paddfval.p +˙=+𝑃K
Assertion elpadd2at2 KLatQARASASQ+˙RS˙Q˙R

Proof

Step Hyp Ref Expression
1 paddfval.l ˙=K
2 paddfval.j ˙=joinK
3 paddfval.a A=AtomsK
4 paddfval.p +˙=+𝑃K
5 1 2 3 4 elpadd2at KLatQARASQ+˙RSAS˙Q˙R
6 5 3adant3r3 KLatQARASASQ+˙RSAS˙Q˙R
7 simpr3 KLatQARASASA
8 7 biantrurd KLatQARASAS˙Q˙RSAS˙Q˙R
9 6 8 bitr4d KLatQARASASQ+˙RS˙Q˙R