Theorem osumcllem7N 38425

Description: Lemma for osumclN 38430. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.)

Hypotheses

Ref	Expression
osumcllem.l	⊢ ≤ = (le‘𝐾)
osumcllem.j	⊢ ∨ = (join‘𝐾)
osumcllem.a	⊢ 𝐴 = (Atoms‘𝐾)
osumcllem.p	⊢ + = (+𝑃‘𝐾)
osumcllem.o	⊢ ⊥ = (⊥𝑃‘𝐾)
osumcllem.c	⊢ 𝐶 = (PSubCl‘𝐾)
osumcllem.m	⊢ 𝑀 = (𝑋 + {𝑝})
osumcllem.u	⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))

Assertion

Ref	Expression
osumcllem7N	⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝐴) ∧ 𝑞 ∈ (𝑌 ∩ 𝑀)) → 𝑝 ∈ (𝑋 + 𝑌))

Distinct variable groups:   𝐴,𝑞   𝐾,𝑞   𝑀,𝑞   ⊥ ,𝑞   + ,𝑞   𝑋,𝑞   𝑌,𝑞   𝑞,𝑝

Allowed substitution hints:   𝐴(𝑝)   𝐶(𝑞,𝑝)   + (𝑝)   𝑈(𝑞,𝑝)   ∨ (𝑞,𝑝)   𝐾(𝑝)   ≤ (𝑞,𝑝)   𝑀(𝑝)   ⊥ (𝑝)   𝑋(𝑝)   𝑌(𝑝)

Proof of Theorem osumcllem7N

Dummy variable 𝑟 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp11 1203	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝐴) ∧ 𝑞 ∈ (𝑌 ∩ 𝑀)) → 𝐾 ∈ HL)
2	1	hllatd 37826	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝐴) ∧ 𝑞 ∈ (𝑌 ∩ 𝑀)) → 𝐾 ∈ Lat)
3		simp12 1204	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝐴) ∧ 𝑞 ∈ (𝑌 ∩ 𝑀)) → 𝑋 ⊆ 𝐴)
4		simp23 1208	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝐴) ∧ 𝑞 ∈ (𝑌 ∩ 𝑀)) → 𝑝 ∈ 𝐴)
5		simp22 1207	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝐴) ∧ 𝑞 ∈ (𝑌 ∩ 𝑀)) → 𝑋 ≠ ∅)
6		inss2 4189	. . . . . 6 ⊢ (𝑌 ∩ 𝑀) ⊆ 𝑀
7	6	sseli 3940	. . . . 5 ⊢ (𝑞 ∈ (𝑌 ∩ 𝑀) → 𝑞 ∈ 𝑀)
8	7	3ad2ant3 1135	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝐴) ∧ 𝑞 ∈ (𝑌 ∩ 𝑀)) → 𝑞 ∈ 𝑀)
9		osumcllem.m	. . . 4 ⊢ 𝑀 = (𝑋 + {𝑝})
10	8, 9	eleqtrdi 2848	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝐴) ∧ 𝑞 ∈ (𝑌 ∩ 𝑀)) → 𝑞 ∈ (𝑋 + {𝑝}))
11		osumcllem.l	. . . 4 ⊢ ≤ = (le‘𝐾)
12		osumcllem.j	. . . 4 ⊢ ∨ = (join‘𝐾)
13		osumcllem.a	. . . 4 ⊢ 𝐴 = (Atoms‘𝐾)
14		osumcllem.p	. . . 4 ⊢ + = (+𝑃‘𝐾)
15	11, 12, 13, 14	elpaddatiN 38268	. . 3 ⊢ (((𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑞 ∈ (𝑋 + {𝑝}))) → ∃𝑟 ∈ 𝑋 𝑞 ≤ (𝑟 ∨ 𝑝))
16	2, 3, 4, 5, 10, 15	syl32anc 1378	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝐴) ∧ 𝑞 ∈ (𝑌 ∩ 𝑀)) → ∃𝑟 ∈ 𝑋 𝑞 ≤ (𝑟 ∨ 𝑝))
17		simp11 1203	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝐴) ∧ 𝑞 ∈ (𝑌 ∩ 𝑀)) ∧ 𝑟 ∈ 𝑋 ∧ 𝑞 ≤ (𝑟 ∨ 𝑝)) → (𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴))
18		simp121 1305	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝐴) ∧ 𝑞 ∈ (𝑌 ∩ 𝑀)) ∧ 𝑟 ∈ 𝑋 ∧ 𝑞 ≤ (𝑟 ∨ 𝑝)) → 𝑋 ⊆ ( ⊥ ‘𝑌))
19		simp123 1307	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝐴) ∧ 𝑞 ∈ (𝑌 ∩ 𝑀)) ∧ 𝑟 ∈ 𝑋 ∧ 𝑞 ≤ (𝑟 ∨ 𝑝)) → 𝑝 ∈ 𝐴)
20		simp2 1137	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝐴) ∧ 𝑞 ∈ (𝑌 ∩ 𝑀)) ∧ 𝑟 ∈ 𝑋 ∧ 𝑞 ≤ (𝑟 ∨ 𝑝)) → 𝑟 ∈ 𝑋)
21		inss1 4188	. . . . 5 ⊢ (𝑌 ∩ 𝑀) ⊆ 𝑌
22		simp13 1205	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝐴) ∧ 𝑞 ∈ (𝑌 ∩ 𝑀)) ∧ 𝑟 ∈ 𝑋 ∧ 𝑞 ≤ (𝑟 ∨ 𝑝)) → 𝑞 ∈ (𝑌 ∩ 𝑀))
23	21, 22	sselid 3942	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝐴) ∧ 𝑞 ∈ (𝑌 ∩ 𝑀)) ∧ 𝑟 ∈ 𝑋 ∧ 𝑞 ≤ (𝑟 ∨ 𝑝)) → 𝑞 ∈ 𝑌)
24		simp3 1138	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝐴) ∧ 𝑞 ∈ (𝑌 ∩ 𝑀)) ∧ 𝑟 ∈ 𝑋 ∧ 𝑞 ≤ (𝑟 ∨ 𝑝)) → 𝑞 ≤ (𝑟 ∨ 𝑝))
25		osumcllem.o	. . . . 5 ⊢ ⊥ = (⊥𝑃‘𝐾)
26		osumcllem.c	. . . . 5 ⊢ 𝐶 = (PSubCl‘𝐾)
27		osumcllem.u	. . . . 5 ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))
28	11, 12, 13, 14, 25, 26, 9, 27	osumcllem6N 38424	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑝 ∈ 𝐴) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ 𝑌 ∧ 𝑞 ≤ (𝑟 ∨ 𝑝))) → 𝑝 ∈ (𝑋 + 𝑌))
29	17, 18, 19, 20, 23, 24, 28	syl123anc 1387	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝐴) ∧ 𝑞 ∈ (𝑌 ∩ 𝑀)) ∧ 𝑟 ∈ 𝑋 ∧ 𝑞 ≤ (𝑟 ∨ 𝑝)) → 𝑝 ∈ (𝑋 + 𝑌))
30	29	rexlimdv3a 3156	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝐴) ∧ 𝑞 ∈ (𝑌 ∩ 𝑀)) → (∃𝑟 ∈ 𝑋 𝑞 ≤ (𝑟 ∨ 𝑝) → 𝑝 ∈ (𝑋 + 𝑌)))
31	16, 30	mpd 15	1 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝐴) ∧ 𝑞 ∈ (𝑌 ∩ 𝑀)) → 𝑝 ∈ (𝑋 + 𝑌))

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   ≠ wne 2943  ∃wrex 3073   ∩ cin 3909   ⊆ wss 3910  ∅c0 4282  {csn 4586   class class class wbr 5105  ‘cfv 6496  (class class class)co 7357  lecple 17140  joincjn 18200  Latclat 18320  Atomscatm 37725  HLchlt 37812  +_𝑃cpadd 38258  ⊥_𝑃cpolN 38365  PSubClcpscN 38397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-1st 7921  df-2nd 7922  df-proset 18184  df-poset 18202  df-plt 18219  df-lub 18235  df-glb 18236  df-join 18237  df-meet 18238  df-p0 18314  df-p1 18315  df-lat 18321  df-clat 18388  df-oposet 37638  df-ol 37640  df-oml 37641  df-covers 37728  df-ats 37729  df-atl 37760  df-cvlat 37784  df-hlat 37813  df-pmap 37967  df-padd 38259  df-polarityN 38366

This theorem is referenced by:  osumcllem8N  38426