This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )