Metamath Proof Explorer

Theorem elpaddri

Description: Condition implying membership in a projective subspace sum. (Contributed by NM, 8-Jan-2012)

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

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 simp3l 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( Q e. X /\ R e. Y ) /\ ( S e. A /\ S .<_ ( Q .\/ R ) ) ) -> S e. A )
6 simp2l 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( Q e. X /\ R e. Y ) /\ ( S e. A /\ S .<_ ( Q .\/ R ) ) ) -> Q e. X )
7 simp2r 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( Q e. X /\ R e. Y ) /\ ( S e. A /\ S .<_ ( Q .\/ R ) ) ) -> R e. Y )
8 simp3r 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( Q e. X /\ R e. Y ) /\ ( S e. A /\ S .<_ ( Q .\/ R ) ) ) -> S .<_ ( Q .\/ R ) )
9 oveq1 
 |-  ( q = Q -> ( q .\/ r ) = ( Q .\/ r ) )
10 9 breq2d 
 |-  ( q = Q -> ( S .<_ ( q .\/ r ) <-> S .<_ ( Q .\/ r ) ) )
11 oveq2 
 |-  ( r = R -> ( Q .\/ r ) = ( Q .\/ R ) )
12 11 breq2d 
 |-  ( r = R -> ( S .<_ ( Q .\/ r ) <-> S .<_ ( Q .\/ R ) ) )
13 10 12 rspc2ev 
 |-  ( ( Q e. X /\ R e. Y /\ S .<_ ( Q .\/ R ) ) -> E. q e. X E. r e. Y S .<_ ( q .\/ r ) )
14 6 7 8 13 syl3anc 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( Q e. X /\ R e. Y ) /\ ( S e. A /\ S .<_ ( Q .\/ R ) ) ) -> E. q e. X E. r e. Y S .<_ ( q .\/ r ) )
15 ne0i 
 |-  ( Q e. X -> X =/= (/) )
16 ne0i 
 |-  ( R e. Y -> Y =/= (/) )
17 15 16 anim12i 
 |-  ( ( Q e. X /\ R e. Y ) -> ( X =/= (/) /\ Y =/= (/) ) )
18 17 anim2i 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( Q e. X /\ R e. Y ) ) -> ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( X =/= (/) /\ Y =/= (/) ) ) )
19 18 3adant3 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( Q e. X /\ R e. Y ) /\ ( S e. A /\ S .<_ ( Q .\/ R ) ) ) -> ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( X =/= (/) /\ Y =/= (/) ) ) )
20 1 2 3 4 elpaddn0 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( X =/= (/) /\ Y =/= (/) ) ) -> ( S e. ( X .+ Y ) <-> ( S e. A /\ E. q e. X E. r e. Y S .<_ ( q .\/ r ) ) ) )
21 19 20 syl 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( Q e. X /\ R e. Y ) /\ ( S e. A /\ S .<_ ( Q .\/ R ) ) ) -> ( S e. ( X .+ Y ) <-> ( S e. A /\ E. q e. X E. r e. Y S .<_ ( q .\/ r ) ) ) )
22 5 14 21 mpbir2and 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( Q e. X /\ R e. Y ) /\ ( S e. A /\ S .<_ ( Q .\/ R ) ) ) -> S e. ( X .+ Y ) )