Metamath Proof Explorer

Theorem elpaddn0

Description: Member of projective subspace sum of nonempty sets. (Contributed by NM, 3-Jan-2012)

Ref Expression
Hypotheses paddfval.l 
|- .<_ = ( le ` K )
paddfval.j 
|- .\/ = ( join ` K )
paddfval.a 
|- A = ( Atoms ` K )
paddfval.p 
|- .+ = ( +P ` K )
Assertion 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 ) ) ) )

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 1 2 3 4 elpadd 
 |-  ( ( K e. Lat /\ X C_ A /\ Y C_ A ) -> ( S e. ( X .+ Y ) <-> ( ( S e. X \/ S e. Y ) \/ ( S e. A /\ E. q e. X E. r e. Y S .<_ ( q .\/ r ) ) ) ) )
6 5 adantr 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( X =/= (/) /\ Y =/= (/) ) ) -> ( S e. ( X .+ Y ) <-> ( ( S e. X \/ S e. Y ) \/ ( S e. A /\ E. q e. X E. r e. Y S .<_ ( q .\/ r ) ) ) ) )
7 simpl2 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( X =/= (/) /\ Y =/= (/) ) ) -> X C_ A )
8 7 sseld 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( X =/= (/) /\ Y =/= (/) ) ) -> ( S e. X -> S e. A ) )
9 simpll1 
 |-  ( ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ S e. X ) /\ r e. Y ) -> K e. Lat )
10 ssel2 
 |-  ( ( X C_ A /\ S e. X ) -> S e. A )
11 10 3ad2antl2 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ S e. X ) -> S e. A )
12 11 adantr 
 |-  ( ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ S e. X ) /\ r e. Y ) -> S e. A )
13 eqid 
 |-  ( Base ` K ) = ( Base ` K )
14 13 3 atbase 
 |-  ( S e. A -> S e. ( Base ` K ) )
15 12 14 syl 
 |-  ( ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ S e. X ) /\ r e. Y ) -> S e. ( Base ` K ) )
16 simpl3 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ S e. X ) -> Y C_ A )
17 16 sselda 
 |-  ( ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ S e. X ) /\ r e. Y ) -> r e. A )
18 13 3 atbase 
 |-  ( r e. A -> r e. ( Base ` K ) )
19 17 18 syl 
 |-  ( ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ S e. X ) /\ r e. Y ) -> r e. ( Base ` K ) )
20 13 1 2 latlej1 
 |-  ( ( K e. Lat /\ S e. ( Base ` K ) /\ r e. ( Base ` K ) ) -> S .<_ ( S .\/ r ) )
21 9 15 19 20 syl3anc 
 |-  ( ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ S e. X ) /\ r e. Y ) -> S .<_ ( S .\/ r ) )
22 21 reximdva0 
 |-  ( ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ S e. X ) /\ Y =/= (/) ) -> E. r e. Y S .<_ ( S .\/ r ) )
23 22 exp31 
 |-  ( ( K e. Lat /\ X C_ A /\ Y C_ A ) -> ( S e. X -> ( Y =/= (/) -> E. r e. Y S .<_ ( S .\/ r ) ) ) )
24 23 com23 
 |-  ( ( K e. Lat /\ X C_ A /\ Y C_ A ) -> ( Y =/= (/) -> ( S e. X -> E. r e. Y S .<_ ( S .\/ r ) ) ) )
25 24 imp 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ Y =/= (/) ) -> ( S e. X -> E. r e. Y S .<_ ( S .\/ r ) ) )
26 25 ancld 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ Y =/= (/) ) -> ( S e. X -> ( S e. X /\ E. r e. Y S .<_ ( S .\/ r ) ) ) )
27 oveq1 
 |-  ( q = S -> ( q .\/ r ) = ( S .\/ r ) )
28 27 breq2d 
 |-  ( q = S -> ( S .<_ ( q .\/ r ) <-> S .<_ ( S .\/ r ) ) )
29 28 rexbidv 
 |-  ( q = S -> ( E. r e. Y S .<_ ( q .\/ r ) <-> E. r e. Y S .<_ ( S .\/ r ) ) )
30 29 rspcev 
 |-  ( ( S e. X /\ E. r e. Y S .<_ ( S .\/ r ) ) -> E. q e. X E. r e. Y S .<_ ( q .\/ r ) )
31 26 30 syl6 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ Y =/= (/) ) -> ( S e. X -> E. q e. X E. r e. Y S .<_ ( q .\/ r ) ) )
32 31 adantrl 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( X =/= (/) /\ Y =/= (/) ) ) -> ( S e. X -> E. q e. X E. r e. Y S .<_ ( q .\/ r ) ) )
33 8 32 jcad 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( X =/= (/) /\ Y =/= (/) ) ) -> ( S e. X -> ( S e. A /\ E. q e. X E. r e. Y S .<_ ( q .\/ r ) ) ) )
34 simpl3 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( X =/= (/) /\ Y =/= (/) ) ) -> Y C_ A )
35 34 sseld 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( X =/= (/) /\ Y =/= (/) ) ) -> ( S e. Y -> S e. A ) )
36 simpll1 
 |-  ( ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ q e. X ) /\ S e. Y ) -> K e. Lat )
37 ssel2 
 |-  ( ( X C_ A /\ q e. X ) -> q e. A )
38 37 3ad2antl2 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ q e. X ) -> q e. A )
39 38 adantr 
 |-  ( ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ q e. X ) /\ S e. Y ) -> q e. A )
40 13 3 atbase 
 |-  ( q e. A -> q e. ( Base ` K ) )
41 39 40 syl 
 |-  ( ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ q e. X ) /\ S e. Y ) -> q e. ( Base ` K ) )
42 simpl3 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ q e. X ) -> Y C_ A )
43 42 sselda 
 |-  ( ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ q e. X ) /\ S e. Y ) -> S e. A )
44 43 14 syl 
 |-  ( ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ q e. X ) /\ S e. Y ) -> S e. ( Base ` K ) )
45 13 1 2 latlej2 
 |-  ( ( K e. Lat /\ q e. ( Base ` K ) /\ S e. ( Base ` K ) ) -> S .<_ ( q .\/ S ) )
46 36 41 44 45 syl3anc 
 |-  ( ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ q e. X ) /\ S e. Y ) -> S .<_ ( q .\/ S ) )
47 46 ex 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ q e. X ) -> ( S e. Y -> S .<_ ( q .\/ S ) ) )
48 47 ancld 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ q e. X ) -> ( S e. Y -> ( S e. Y /\ S .<_ ( q .\/ S ) ) ) )
49 oveq2 
 |-  ( r = S -> ( q .\/ r ) = ( q .\/ S ) )
50 49 breq2d 
 |-  ( r = S -> ( S .<_ ( q .\/ r ) <-> S .<_ ( q .\/ S ) ) )
51 50 rspcev 
 |-  ( ( S e. Y /\ S .<_ ( q .\/ S ) ) -> E. r e. Y S .<_ ( q .\/ r ) )
52 48 51 syl6 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ q e. X ) -> ( S e. Y -> E. r e. Y S .<_ ( q .\/ r ) ) )
53 52 impancom 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ S e. Y ) -> ( q e. X -> E. r e. Y S .<_ ( q .\/ r ) ) )
54 53 ancld 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ S e. Y ) -> ( q e. X -> ( q e. X /\ E. r e. Y S .<_ ( q .\/ r ) ) ) )
55 54 eximdv 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ S e. Y ) -> ( E. q q e. X -> E. q ( q e. X /\ E. r e. Y S .<_ ( q .\/ r ) ) ) )
56 n0 
 |-  ( X =/= (/) <-> E. q q e. X )
57 df-rex 
 |-  ( E. q e. X E. r e. Y S .<_ ( q .\/ r ) <-> E. q ( q e. X /\ E. r e. Y S .<_ ( q .\/ r ) ) )
58 55 56 57 3imtr4g 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ S e. Y ) -> ( X =/= (/) -> E. q e. X E. r e. Y S .<_ ( q .\/ r ) ) )
59 58 impancom 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ X =/= (/) ) -> ( S e. Y -> E. q e. X E. r e. Y S .<_ ( q .\/ r ) ) )
60 59 adantrr 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( X =/= (/) /\ Y =/= (/) ) ) -> ( S e. Y -> E. q e. X E. r e. Y S .<_ ( q .\/ r ) ) )
61 35 60 jcad 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( X =/= (/) /\ Y =/= (/) ) ) -> ( S e. Y -> ( S e. A /\ E. q e. X E. r e. Y S .<_ ( q .\/ r ) ) ) )
62 33 61 jaod 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( X =/= (/) /\ Y =/= (/) ) ) -> ( ( S e. X \/ S e. Y ) -> ( S e. A /\ E. q e. X E. r e. Y S .<_ ( q .\/ r ) ) ) )
63 pm4.72 
 |-  ( ( ( S e. X \/ S e. Y ) -> ( S e. A /\ E. q e. X E. r e. Y S .<_ ( q .\/ r ) ) ) <-> ( ( S e. A /\ E. q e. X E. r e. Y S .<_ ( q .\/ r ) ) <-> ( ( S e. X \/ S e. Y ) \/ ( S e. A /\ E. q e. X E. r e. Y S .<_ ( q .\/ r ) ) ) ) )
64 62 63 sylib 
 |-  ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( X =/= (/) /\ Y =/= (/) ) ) -> ( ( S e. A /\ E. q e. X E. r e. Y S .<_ ( q .\/ r ) ) <-> ( ( S e. X \/ S e. Y ) \/ ( S e. A /\ E. q e. X E. r e. Y S .<_ ( q .\/ r ) ) ) ) )
65 6 64 bitr4d 
 |-  ( ( ( 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 ) ) ) )