Theorem elpadd2at

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

	Ref	Expression
Hypotheses	paddfval.l	|- .<_ = ( le ` K )
	paddfval.j	|- .\/ = ( join ` K )
	paddfval.a	|- A = ( Atoms ` K )
	paddfval.p	|- .+ = ( +P ` K )
Assertion	elpadd2at	|- ( ( K e. Lat /\ Q e. A /\ R e. A ) -> ( S e. ( { Q } .+ { R } ) <-> ( S e. A /\ S .<_ ( Q .\/ R ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		paddfval.l	|- .<_ = ( le ` K )
2		paddfval.j	|- .\/ = ( join ` K )
3		paddfval.a	|- A = ( Atoms ` K )
4		paddfval.p	|- .+ = ( +P ` K )
5		simp1	|- ( ( K e. Lat /\ Q e. A /\ R e. A ) -> K e. Lat )
6		simp2	|- ( ( K e. Lat /\ Q e. A /\ R e. A ) -> Q e. A )
7	6	snssd	|- ( ( K e. Lat /\ Q e. A /\ R e. A ) -> { Q } C_ A )
8		simp3	|- ( ( K e. Lat /\ Q e. A /\ R e. A ) -> R e. A )
9		snnzg	|- ( Q e. A -> { Q } =/= (/) )
10	9	3ad2ant2	|- ( ( K e. Lat /\ Q e. A /\ R e. A ) -> { Q } =/= (/) )
11	1 2 3 4	elpaddat	|- ( ( ( K e. Lat /\ { Q } C_ A /\ R e. A ) /\ { Q } =/= (/) ) -> ( S e. ( { Q } .+ { R } ) <-> ( S e. A /\ E. r e. { Q } S .<_ ( r .\/ R ) ) ) )
12	5 7 8 10 11	syl31anc	|- ( ( K e. Lat /\ Q e. A /\ R e. A ) -> ( S e. ( { Q } .+ { R } ) <-> ( S e. A /\ E. r e. { Q } S .<_ ( r .\/ R ) ) ) )
13		oveq1	|- ( r = Q -> ( r .\/ R ) = ( Q .\/ R ) )
14	13	breq2d	|- ( r = Q -> ( S .<_ ( r .\/ R ) <-> S .<_ ( Q .\/ R ) ) )
15	14	rexsng	|- ( Q e. A -> ( E. r e. { Q } S .<_ ( r .\/ R ) <-> S .<_ ( Q .\/ R ) ) )
16	15	3ad2ant2	|- ( ( K e. Lat /\ Q e. A /\ R e. A ) -> ( E. r e. { Q } S .<_ ( r .\/ R ) <-> S .<_ ( Q .\/ R ) ) )
17	16	anbi2d	|- ( ( K e. Lat /\ Q e. A /\ R e. A ) -> ( ( S e. A /\ E. r e. { Q } S .<_ ( r .\/ R ) ) <-> ( S e. A /\ S .<_ ( Q .\/ R ) ) ) )
18	12 17	bitrd	|- ( ( K e. Lat /\ Q e. A /\ R e. A ) -> ( S e. ( { Q } .+ { R } ) <-> ( S e. A /\ S .<_ ( Q .\/ R ) ) ) )