Theorem osumcllem9N 33574

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

Hypotheses

Ref	Expression
osumcllem.l	|- .<_ = ( le ` K )
osumcllem.j	|- .\/ = ( join ` K )
osumcllem.a	|- A = ( Atoms ` K )
osumcllem.p	|- .+ = ( +P ` K )
osumcllem.o	|- ._|_ = ( _|_P ` K )
osumcllem.c	|- C = ( PSubCl ` K )
osumcllem.m	|- M = ( X .+ { p } )
osumcllem.u	|- U = ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) )

Assertion

Ref	Expression
osumcllem9N	|- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> M = X )

Proof of Theorem osumcllem9N

Step	Hyp	Ref	Expression
1		inass 3654	. . . . . . 7 |- ( ( ( ._|_ ` X ) i^i U ) i^i M ) = ( ( ._|_ ` X ) i^i ( U i^i M ) )
2		simp11 1044	. . . . . . . . 9 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> K e. HL )
3		simp13 1046	. . . . . . . . 9 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> Y e. C )
4		simp21 1047	. . . . . . . . 9 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> X C_ ( ._|_ ` Y ) )
5		osumcllem.l	. . . . . . . . . 10 |- .<_ = ( le ` K )
6		osumcllem.j	. . . . . . . . . 10 |- .\/ = ( join ` K )
7		osumcllem.a	. . . . . . . . . 10 |- A = ( Atoms ` K )
8		osumcllem.p	. . . . . . . . . 10 |- .+ = ( +P ` K )
9		osumcllem.o	. . . . . . . . . 10 |- ._|_ = ( _|_P ` K )
10		osumcllem.c	. . . . . . . . . 10 |- C = ( PSubCl ` K )
11		osumcllem.m	. . . . . . . . . 10 |- M = ( X .+ { p } )
12		osumcllem.u	. . . . . . . . . 10 |- U = ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) )
13	5, 6, 7, 8, 9, 10, 11, 12	osumcllem3N 33568	. . . . . . . . 9 |- ( ( K e. HL /\ Y e. C /\ X C_ ( ._|_ ` Y ) ) -> ( ( ._|_ ` X ) i^i U ) = Y )
14	2, 3, 4, 13	syl3anc 1276	. . . . . . . 8 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> ( ( ._|_ ` X ) i^i U ) = Y )
15	14	ineq1d 3645	. . . . . . 7 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> ( ( ( ._|_ ` X ) i^i U ) i^i M ) = ( Y i^i M ) )
16	1, 15	syl5eqr 2510	. . . . . 6 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> ( ( ._|_ ` X ) i^i ( U i^i M ) ) = ( Y i^i M ) )
17		simp12 1045	. . . . . . . 8 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> X e. C )
18	7, 10	psubclssatN 33551	. . . . . . . 8 |- ( ( K e. HL /\ X e. C ) -> X C_ A )
19	2, 17, 18	syl2anc 671	. . . . . . 7 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> X C_ A )
20	7, 10	psubclssatN 33551	. . . . . . . 8 |- ( ( K e. HL /\ Y e. C ) -> Y C_ A )
21	2, 3, 20	syl2anc 671	. . . . . . 7 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> Y C_ A )
22		simp22 1048	. . . . . . 7 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> X =/= (/) )
23	7, 8	paddssat 33424	. . . . . . . . . . . 12 |- ( ( K e. HL /\ X C_ A /\ Y C_ A ) -> ( X .+ Y ) C_ A )
24	2, 19, 21, 23	syl3anc 1276	. . . . . . . . . . 11 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> ( X .+ Y ) C_ A )
25	7, 9	polssatN 33518	. . . . . . . . . . 11 |- ( ( K e. HL /\ ( X .+ Y ) C_ A ) -> ( ._|_ ` ( X .+ Y ) ) C_ A )
26	2, 24, 25	syl2anc 671	. . . . . . . . . 10 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> ( ._|_ ` ( X .+ Y ) ) C_ A )
27	7, 9	polssatN 33518	. . . . . . . . . 10 |- ( ( K e. HL /\ ( ._|_ ` ( X .+ Y ) ) C_ A ) -> ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) C_ A )
28	2, 26, 27	syl2anc 671	. . . . . . . . 9 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) C_ A )
29	12, 28	syl5eqss 3488	. . . . . . . 8 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> U C_ A )
30		simp23 1049	. . . . . . . 8 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> p e. U )
31	29, 30	sseldd 3445	. . . . . . 7 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> p e. A )
32		simp3 1016	. . . . . . 7 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> -. p e. ( X .+ Y ) )
33	5, 6, 7, 8, 9, 10, 11, 12	osumcllem8N 33573	. . . . . . 7 |- ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. A ) /\ -. p e. ( X .+ Y ) ) -> ( Y i^i M ) = (/) )
34	2, 19, 21, 4, 22, 31, 32, 33	syl331anc 1301	. . . . . 6 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> ( Y i^i M ) = (/) )
35	16, 34	eqtrd 2496	. . . . 5 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> ( ( ._|_ ` X ) i^i ( U i^i M ) ) = (/) )
36	35	fveq2d 5892	. . . 4 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> ( ._|_ ` ( ( ._|_ ` X ) i^i ( U i^i M ) ) ) = ( ._|_ ` (/) ) )
37	7, 9	pol0N 33519	. . . . 5 |- ( K e. HL -> ( ._|_ ` (/) ) = A )
38	2, 37	syl 17	. . . 4 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> ( ._|_ ` (/) ) = A )
39	36, 38	eqtrd 2496	. . 3 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> ( ._|_ ` ( ( ._|_ ` X ) i^i ( U i^i M ) ) ) = A )
40	5, 6, 7, 8, 9, 10, 11, 12	osumcllem1N 33566	. . . 4 |- ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ p e. U ) -> ( U i^i M ) = M )
41	2, 19, 21, 30, 40	syl31anc 1279	. . 3 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> ( U i^i M ) = M )
42	39, 41	ineq12d 3647	. 2 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> ( ( ._|_ ` ( ( ._|_ ` X ) i^i ( U i^i M ) ) ) i^i ( U i^i M ) ) = ( A i^i M ) )
43	7, 9, 10	polsubclN 33562	. . . . . 6 |- ( ( K e. HL /\ ( ._|_ ` ( X .+ Y ) ) C_ A ) -> ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) e. C )
44	2, 26, 43	syl2anc 671	. . . . 5 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) e. C )
45	12, 44	syl5eqel 2544	. . . 4 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> U e. C )
46	7, 8, 10	paddatclN 33559	. . . . . 6 |- ( ( K e. HL /\ X e. C /\ p e. A ) -> ( X .+ { p } ) e. C )
47	2, 17, 31, 46	syl3anc 1276	. . . . 5 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> ( X .+ { p } ) e. C )
48	11, 47	syl5eqel 2544	. . . 4 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> M e. C )
49	10	psubclinN 33558	. . . 4 |- ( ( K e. HL /\ U e. C /\ M e. C ) -> ( U i^i M ) e. C )
50	2, 45, 48, 49	syl3anc 1276	. . 3 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> ( U i^i M ) e. C )
51	5, 6, 7, 8, 9, 10, 11, 12	osumcllem2N 33567	. . . 4 |- ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ p e. U ) -> X C_ ( U i^i M ) )
52	2, 19, 21, 30, 51	syl31anc 1279	. . 3 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> X C_ ( U i^i M ) )
53	10, 9	poml6N 33565	. . 3 |- ( ( ( K e. HL /\ X e. C /\ ( U i^i M ) e. C ) /\ X C_ ( U i^i M ) ) -> ( ( ._|_ ` ( ( ._|_ ` X ) i^i ( U i^i M ) ) ) i^i ( U i^i M ) ) = X )
54	2, 17, 50, 52, 53	syl31anc 1279	. 2 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> ( ( ._|_ ` ( ( ._|_ ` X ) i^i ( U i^i M ) ) ) i^i ( U i^i M ) ) = X )
55	31	snssd 4130	. . . . 5 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> { p } C_ A )
56	7, 8	paddssat 33424	. . . . 5 |- ( ( K e. HL /\ X C_ A /\ { p } C_ A ) -> ( X .+ { p } ) C_ A )
57	2, 19, 55, 56	syl3anc 1276	. . . 4 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> ( X .+ { p } ) C_ A )
58	11, 57	syl5eqss 3488	. . 3 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> M C_ A )
59		sseqin2 3663	. . 3 |- ( M C_ A <-> ( A i^i M ) = M )
60	58, 59	sylib 201	. 2 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> ( A i^i M ) = M )
61	42, 54, 60	3eqtr3rd 2505	1 |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> M = X )

Syntax hints:   -. wn 3   -> wi 4   /\ w3a 991   = wceq 1455   e. wcel 1898   =/= wne 2633   i^i cin 3415   C_ wss 3416   (/)c0 3743   {csn 3980   ` cfv 5601  (class class class)co 6315   lecple 15246   joincjn 16238   Atomscatm 32874   HLchlt 32961   +Pcpadd 33405   _|_PcpolN 33512   PSubClcpscN 33544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4529  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-riotaBAD 32570

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-iun 4294  df-iin 4295  df-br 4417  df-opab 4476  df-mpt 4477  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-1st 6820  df-2nd 6821  df-undef 7046  df-preset 16222  df-poset 16240  df-plt 16253  df-lub 16269  df-glb 16270  df-join 16271  df-meet 16272  df-p0 16334  df-p1 16335  df-lat 16341  df-clat 16403  df-oposet 32787  df-ol 32789  df-oml 32790  df-covers 32877  df-ats 32878  df-atl 32909  df-cvlat 32933  df-hlat 32962  df-psubsp 33113  df-pmap 33114  df-padd 33406  df-polarityN 33513  df-psubclN 33545

This theorem is referenced by:  osumcllem11N  33576