Theorem elpaddn0 18504

Description: Member of projective subspace sum of non-empty sets.

Hypotheses

Ref	Expression
paddfval.l	|- ≤ = (le` K)
paddfval.j	|- ∨ = (join` K)
paddfval.a	|- A = (Atoms` K)
paddfval.p	|- P = (+P` K)

Assertion

Ref	Expression
elpaddn0	|- (((K e. Lat /\ X C_ A /\ Y C_ A) /\ (X =/= (/) /\ Y =/= (/))) -> (S e. (XPY) <-> (S e. A /\ E.q e. X E.r e. Y S ≤ (q ∨ r))))

Distinct variable groups:   r,q,K   X,q   Y,q,r   S,q,r   A,q,r   q, ∨ ,r   q, ≤ ,r   X,r

Proof of Theorem elpaddn0

Step	Hyp	Ref	Expression
1		paddfval.l	. . . 4 |- ≤ = (le` K)
2		paddfval.j	. . . 4 |- ∨ = (join` K)
3		paddfval.a	. . . 4 |- A = (Atoms` K)
4		paddfval.p	. . . 4 |- P = (+P` K)
5	1, 2, 3, 4	elpadd 18503	. . 3 |- ((K e. Lat /\ X C_ A /\ Y C_ A) -> (S e. (XPY) <-> ((S e. X \/ S e. Y) \/ (S e. A /\ E.q e. X E.r e. Y S ≤ (q ∨ r)))))
6	5	adantr 543	. 2 |- (((K e. Lat /\ X C_ A /\ Y C_ A) /\ (X =/= (/) /\ Y =/= (/))) -> (S e. (XPY) <-> ((S e. X \/ S e. Y) \/ (S e. A /\ E.q e. X E.r e. Y S ≤ (q ∨ r)))))
7		simpl2 1152	. . . . . 6 |- (((K e. Lat /\ X C_ A /\ Y C_ A) /\ (X =/= (/) /\ Y =/= (/))) -> X C_ A)
8	7	sseld 2882	. . . . 5 |- (((K e. Lat /\ X C_ A /\ Y C_ A) /\ (X =/= (/) /\ Y =/= (/))) -> (S e. X -> S e. A))
9		simpll1 1187	. . . . . . . . . . . . 13 |- ((((K e. Lat /\ X C_ A /\ Y C_ A) /\ S e. X) /\ r e. Y) -> K e. Lat)
10		ssel2 2879	. . . . . . . . . . . . . . . 16 |- ((X C_ A /\ S e. X) -> S e. A)
11	10	3ad2antl2 1317	. . . . . . . . . . . . . . 15 |- (((K e. Lat /\ X C_ A /\ Y C_ A) /\ S e. X) -> S e. A)
12	11	adantr 543	. . . . . . . . . . . . . 14 |- ((((K e. Lat /\ X C_ A /\ Y C_ A) /\ S e. X) /\ r e. Y) -> S e. A)
13		eqid 2170	. . . . . . . . . . . . . . 15 |- (Base` K) = (Base` K)
14	13, 3	atbase 17942	. . . . . . . . . . . . . 14 |- (S e. A -> S e. (Base` K))
15	12, 14	syl 13	. . . . . . . . . . . . 13 |- ((((K e. Lat /\ X C_ A /\ Y C_ A) /\ S e. X) /\ r e. Y) -> S e. (Base` K))
16		simpl3 1153	. . . . . . . . . . . . . . . 16 |- (((K e. Lat /\ X C_ A /\ Y C_ A) /\ S e. X) -> Y C_ A)
17	16	sseld 2882	. . . . . . . . . . . . . . 15 |- (((K e. Lat /\ X C_ A /\ Y C_ A) /\ S e. X) -> (r e. Y -> r e. A))
18	17	imp 489	. . . . . . . . . . . . . 14 |- ((((K e. Lat /\ X C_ A /\ Y C_ A) /\ S e. X) /\ r e. Y) -> r e. A)
19	13, 3	atbase 17942	. . . . . . . . . . . . . 14 |- (r e. A -> r e. (Base` K))
20	18, 19	syl 13	. . . . . . . . . . . . 13 |- ((((K e. Lat /\ X C_ A /\ Y C_ A) /\ S e. X) /\ r e. Y) -> r e. (Base` K))
21	13, 1, 2	latlej1 9772	. . . . . . . . . . . . 13 |- ((K e. Lat /\ S e. (Base` K) /\ r e. (Base` K)) -> S ≤ (S ∨ r))
22	9, 15, 20, 21	syl111anc 1377	. . . . . . . . . . . 12 |- ((((K e. Lat /\ X C_ A /\ Y C_ A) /\ S e. X) /\ r e. Y) -> S ≤ (S ∨ r))
23	22	reximdva0 3125	. . . . . . . . . . 11 |- ((((K e. Lat /\ X C_ A /\ Y C_ A) /\ S e. X) /\ Y =/= (/)) -> E.r e. Y S ≤ (S ∨ r))
24	23	exp31 673	. . . . . . . . . 10 |- ((K e. Lat /\ X C_ A /\ Y C_ A) -> (S e. X -> (Y =/= (/) -> E.r e. Y S ≤ (S ∨ r))))
25	24	com23 68	. . . . . . . . 9 |- ((K e. Lat /\ X C_ A /\ Y C_ A) -> (Y =/= (/) -> (S e. X -> E.r e. Y S ≤ (S ∨ r))))
26	25	imp 489	. . . . . . . 8 |- (((K e. Lat /\ X C_ A /\ Y C_ A) /\ Y =/= (/)) -> (S e. X -> E.r e. Y S ≤ (S ∨ r)))
27	26	ancld 609	. . . . . . 7 |- (((K e. Lat /\ X C_ A /\ Y C_ A) /\ Y =/= (/)) -> (S e. X -> (S e. X /\ E.r e. Y S ≤ (S ∨ r))))
28		opreq1 5025	. . . . . . . . . 10 |- (q = S -> (q ∨ r) = (S ∨ r))
29	28	breq2d 3551	. . . . . . . . 9 |- (q = S -> (S ≤ (q ∨ r) <-> S ≤ (S ∨ r)))
30	29	rexbidv 2404	. . . . . . . 8 |- (q = S -> (E.r e. Y S ≤ (q ∨ r) <-> E.r e. Y S ≤ (S ∨ r)))
31	30	rcla4ev 2651	. . . . . . 7 |- ((S e. X /\ E.r e. Y S ≤ (S ∨ r)) -> E.q e. X E.r e. Y S ≤ (q ∨ r))
32	27, 31	syl6 39	. . . . . 6 |- (((K e. Lat /\ X C_ A /\ Y C_ A) /\ Y =/= (/)) -> (S e. X -> E.q e. X E.r e. Y S ≤ (q ∨ r)))
33	32	adantrl 836	. . . . 5 |- (((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)))
34	8, 33	jcad 592	. . . 4 |- (((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))))
35		simpl3 1153	. . . . . 6 |- (((K e. Lat /\ X C_ A /\ Y C_ A) /\ (X =/= (/) /\ Y =/= (/))) -> Y C_ A)
36	35	sseld 2882	. . . . 5 |- (((K e. Lat /\ X C_ A /\ Y C_ A) /\ (X =/= (/) /\ Y =/= (/))) -> (S e. Y -> S e. A))
37		simpll1 1187	. . . . . . . . . . . . . . . . . . 19 |- ((((K e. Lat /\ X C_ A /\ Y C_ A) /\ q e. X) /\ S e. Y) -> K e. Lat)
38		ssel2 2879	. . . . . . . . . . . . . . . . . . . . . 22 |- ((X C_ A /\ q e. X) -> q e. A)
39	38	3ad2antl2 1317	. . . . . . . . . . . . . . . . . . . . 21 |- (((K e. Lat /\ X C_ A /\ Y C_ A) /\ q e. X) -> q e. A)
40	39	adantr 543	. . . . . . . . . . . . . . . . . . . 20 |- ((((K e. Lat /\ X C_ A /\ Y C_ A) /\ q e. X) /\ S e. Y) -> q e. A)
41	13, 3	atbase 17942	. . . . . . . . . . . . . . . . . . . 20 |- (q e. A -> q e. (Base` K))
42	40, 41	syl 13	. . . . . . . . . . . . . . . . . . 19 |- ((((K e. Lat /\ X C_ A /\ Y C_ A) /\ q e. X) /\ S e. Y) -> q e. (Base` K))
43		simpl3 1153	. . . . . . . . . . . . . . . . . . . . . 22 |- (((K e. Lat /\ X C_ A /\ Y C_ A) /\ q e. X) -> Y C_ A)
44	43	sseld 2882	. . . . . . . . . . . . . . . . . . . . 21 |- (((K e. Lat /\ X C_ A /\ Y C_ A) /\ q e. X) -> (S e. Y -> S e. A))
45	44	imp 489	. . . . . . . . . . . . . . . . . . . 20 |- ((((K e. Lat /\ X C_ A /\ Y C_ A) /\ q e. X) /\ S e. Y) -> S e. A)
46	45, 14	syl 13	. . . . . . . . . . . . . . . . . . 19 |- ((((K e. Lat /\ X C_ A /\ Y C_ A) /\ q e. X) /\ S e. Y) -> S e. (Base` K))
47	13, 1, 2	latlej2 9773	. . . . . . . . . . . . . . . . . . 19 |- ((K e. Lat /\ q e. (Base` K) /\ S e. (Base` K)) -> S ≤ (q ∨ S))
48	37, 42, 46, 47	syl111anc 1377	. . . . . . . . . . . . . . . . . 18 |- ((((K e. Lat /\ X C_ A /\ Y C_ A) /\ q e. X) /\ S e. Y) -> S ≤ (q ∨ S))
49	48	ex 494	. . . . . . . . . . . . . . . . 17 |- (((K e. Lat /\ X C_ A /\ Y C_ A) /\ q e. X) -> (S e. Y -> S ≤ (q ∨ S)))
50	49	ancld 609	. . . . . . . . . . . . . . . 16 |- (((K e. Lat /\ X C_ A /\ Y C_ A) /\ q e. X) -> (S e. Y -> (S e. Y /\ S ≤ (q ∨ S))))
51		opreq2 5026	. . . . . . . . . . . . . . . . . 18 |- (r = S -> (q ∨ r) = (q ∨ S))
52	51	breq2d 3551	. . . . . . . . . . . . . . . . 17 |- (r = S -> (S ≤ (q ∨ r) <-> S ≤ (q ∨ S)))
53	52	rcla4ev 2651	. . . . . . . . . . . . . . . 16 |- ((S e. Y /\ S ≤ (q ∨ S)) -> E.r e. Y S ≤ (q ∨ r))
54	50, 53	syl6 39	. . . . . . . . . . . . . . 15 |- (((K e. Lat /\ X C_ A /\ Y C_ A) /\ q e. X) -> (S e. Y -> E.r e. Y S ≤ (q ∨ r)))
55	54	ex 494	. . . . . . . . . . . . . 14 |- ((K e. Lat /\ X C_ A /\ Y C_ A) -> (q e. X -> (S e. Y -> E.r e. Y S ≤ (q ∨ r))))
56	55	com23 68	. . . . . . . . . . . . 13 |- ((K e. Lat /\ X C_ A /\ Y C_ A) -> (S e. Y -> (q e. X -> E.r e. Y S ≤ (q ∨ r))))
57	56	imp 489	. . . . . . . . . . . 12 |- (((K e. Lat /\ X C_ A /\ Y C_ A) /\ S e. Y) -> (q e. X -> E.r e. Y S ≤ (q ∨ r)))
58	57	ancld 609	. . . . . . . . . . 11 |- (((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))))
59	58	eximdv 1967	. . . . . . . . . 10 |- (((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))))
60		n0 3123	. . . . . . . . . 10 |- (X =/= (/) <-> E.q q e. X)
61		df-rex 2390	. . . . . . . . . 10 |- (E.q e. X E.r e. Y S ≤ (q ∨ r) <-> E.q(q e. X /\ E.r e. Y S ≤ (q ∨ r)))
62	59, 60, 61	3imtr4g 333	. . . . . . . . 9 |- (((K e. Lat /\ X C_ A /\ Y C_ A) /\ S e. Y) -> (X =/= (/) -> E.q e. X E.r e. Y S ≤ (q ∨ r)))
63	62	ex 494	. . . . . . . 8 |- ((K e. Lat /\ X C_ A /\ Y C_ A) -> (S e. Y -> (X =/= (/) -> E.q e. X E.r e. Y S ≤ (q ∨ r))))
64	63	com23 68	. . . . . . 7 |- ((K e. Lat /\ X C_ A /\ Y C_ A) -> (X =/= (/) -> (S e. Y -> E.q e. X E.r e. Y S ≤ (q ∨ r))))
65	64	imp 489	. . . . . 6 |- (((K e. Lat /\ X C_ A /\ Y C_ A) /\ X =/= (/)) -> (S e. Y -> E.q e. X E.r e. Y S ≤ (q ∨ r)))
66	65	adantrr 838	. . . . 5 |- (((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)))
67	36, 66	jcad 592	. . . 4 |- (((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))))
68	34, 67	jaod 550	. . 3 |- (((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))))
69		pm4.72 1010	. . 3 |- (((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)))))
70	68, 69	sylib 263	. 2 |- (((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)))))
71	6, 70	bitr4d 315	1 |- (((K e. Lat /\ X C_ A /\ Y C_ A) /\ (X =/= (/) /\ Y =/= (/))) -> (S e. (XPY) <-> (S e. A /\ E.q e. X E.r e. Y S ≤ (q ∨ r))))

Syntax hints:   -> wi 3   <-> wb 231   \/ wo 432   /\ wa 433   /\ w3a 1130   = wceq 1615   e. wcel 1617  E.wex 1644   =/= wne 2295  E.wrex 2386   C_ wss 2859  (/)c0 3114   class class class wbr 3539  ` cfv 4163  (class class class)co 5020  Basecbs 9579  lecple 9687  joincjn 9692  Latclat 9751  Atomscatm 17916  +Pcpadd 18499

This theorem is referenced by:  paddvaln0 18505  elpaddri 18506  elpaddat 18508  paddasslem15 18538  paddasslem16 18539  pmodlem2 18551  pmapjat1 18557

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-13 1628  ax-14 1629  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152  ax-rep 3628  ax-sep 3638  ax-nul 3645  ax-pow 3681  ax-pr 3719  ax-un 3961

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-3an 1132  df-ex 1645  df-sb 1845  df-eu 2070  df-mo 2071  df-clab 2158  df-cleq 2163  df-clel 2166  df-ne 2297  df-ral 2389  df-rex 2390  df-reu 2391  df-rab 2392  df-v 2571  df-sbc 2731  df-csb 2806  df-dif 2862  df-un 2864  df-in 2866  df-ss 2868  df-nul 3115  df-if 3213  df-pw 3261  df-sn 3274  df-pr 3275  df-op 3278  df-uni 3399  df-br 3540  df-opab 3598  df-id 3779  df-xp 4165  df-rel 4166  df-cnv 4167  df-co 4168  df-dm 4169  df-rn 4170  df-res 4171  df-ima 4172  df-fun 4173  df-fn 4174  df-f 4175  df-f1 4176  df-fo 4177  df-f1o 4178  df-fv 4179  df-opr 5022  df-oprab 5023  df-mpt 5138  df-mpt2 5139  df-iota 5259  df-er 5519  df-en 5631  df-dom 5632  df-sdom 5633  df-undef 5769  df-riota 5773  df-lub 9718  df-join 9720  df-lat 9758  df-ats 17921  df-padd 18500

Copyright terms: Public domain