Theorem osumcllem5N

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

	Ref	Expression
Hypotheses	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	osumcllem5N	|- ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ p e. A /\ ( r e. X /\ q e. Y /\ p .<_ ( r .\/ q ) ) ) -> p e. ( X .+ Y ) )

Proof

Step	Hyp	Ref	Expression
1		osumcllem.l	|- .<_ = ( le ` K )
2		osumcllem.j	|- .\/ = ( join ` K )
3		osumcllem.a	|- A = ( Atoms ` K )
4		osumcllem.p	|- .+ = ( +P ` K )
5		osumcllem.o	|- ._|_ = ( _|_P ` K )
6		osumcllem.c	|- C = ( PSubCl ` K )
7		osumcllem.m	|- M = ( X .+ { p } )
8		osumcllem.u	|- U = ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) )
9		simp11	|- ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ p e. A /\ ( r e. X /\ q e. Y /\ p .<_ ( r .\/ q ) ) ) -> K e. HL )
10	9	hllatd	|- ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ p e. A /\ ( r e. X /\ q e. Y /\ p .<_ ( r .\/ q ) ) ) -> K e. Lat )
11		simp12	|- ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ p e. A /\ ( r e. X /\ q e. Y /\ p .<_ ( r .\/ q ) ) ) -> X C_ A )
12		simp13	|- ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ p e. A /\ ( r e. X /\ q e. Y /\ p .<_ ( r .\/ q ) ) ) -> Y C_ A )
13		simp31	|- ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ p e. A /\ ( r e. X /\ q e. Y /\ p .<_ ( r .\/ q ) ) ) -> r e. X )
14		simp32	|- ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ p e. A /\ ( r e. X /\ q e. Y /\ p .<_ ( r .\/ q ) ) ) -> q e. Y )
15		simp2	|- ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ p e. A /\ ( r e. X /\ q e. Y /\ p .<_ ( r .\/ q ) ) ) -> p e. A )
16		simp33	|- ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ p e. A /\ ( r e. X /\ q e. Y /\ p .<_ ( r .\/ q ) ) ) -> p .<_ ( r .\/ q ) )
17	1 2 3 4	elpaddri	|- ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( r e. X /\ q e. Y ) /\ ( p e. A /\ p .<_ ( r .\/ q ) ) ) -> p e. ( X .+ Y ) )
18	10 11 12 13 14 15 16 17	syl322anc	|- ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ p e. A /\ ( r e. X /\ q e. Y /\ p .<_ ( r .\/ q ) ) ) -> p e. ( X .+ Y ) )