Metamath Proof Explorer

Theorem cdlemg1idN

Description: Version of cdleme31id with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 18-Apr-2013) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	cdlemg1ltrn.l	\|- .<_ = ( le ` K )
		cdlemg1ltrn.a	\|- A = ( Atoms ` K )
		cdlemg1ltrn.h	\|- H = ( LHyp ` K )
		cdlemg1ltrn.f	\|- F = ( iota_ f e. T ( f ` P ) = Q )
		cdlemg1ltrn.t	\|- T = ( ( LTrn ` K ) ` W )
		cdlemg1id.b	\|- B = ( Base ` K )
	Assertion	cdlemg1idN	\|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ X e. B ) /\ P = Q ) -> ( F ` X ) = X )

Proof

Step	Hyp	Ref	Expression
1		cdlemg1ltrn.l	\|- .<_ = ( le ` K )
2		cdlemg1ltrn.a	\|- A = ( Atoms ` K )
3		cdlemg1ltrn.h	\|- H = ( LHyp ` K )
4		cdlemg1ltrn.f	\|- F = ( iota_ f e. T ( f ` P ) = Q )
5		cdlemg1ltrn.t	\|- T = ( ( LTrn ` K ) ` W )
6		cdlemg1id.b	\|- B = ( Base ` K )
7		eqid	\|- ( join ` K ) = ( join ` K )
8		eqid	\|- ( meet ` K ) = ( meet ` K )
9		eqid	\|- ( ( P ( join ` K ) Q ) ( meet ` K ) W ) = ( ( P ( join ` K ) Q ) ( meet ` K ) W )
10		eqid	\|- ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) = ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) )
11		eqid	\|- ( ( P ( join ` K ) Q ) ( meet ` K ) ( ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) ( join ` K ) ( ( s ( join ` K ) t ) ( meet ` K ) W ) ) ) = ( ( P ( join ` K ) Q ) ( meet ` K ) ( ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) ( join ` K ) ( ( s ( join ` K ) t ) ( meet ` K ) W ) ) )
12		eqid	\|- ( x e. B \|-> if ( ( P =/= Q /\ -. x .<_ W ) , ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s ( join ` K ) ( x ( meet ` K ) W ) ) = x ) -> z = ( if ( s .<_ ( P ( join ` K ) Q ) , ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P ( join ` K ) Q ) ) -> y = ( ( P ( join ` K ) Q ) ( meet ` K ) ( ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) ( join ` K ) ( ( s ( join ` K ) t ) ( meet ` K ) W ) ) ) ) ) , [_ s / t ]_ ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) ) ( join ` K ) ( x ( meet ` K ) W ) ) ) ) , x ) ) = ( x e. B \|-> if ( ( P =/= Q /\ -. x .<_ W ) , ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s ( join ` K ) ( x ( meet ` K ) W ) ) = x ) -> z = ( if ( s .<_ ( P ( join ` K ) Q ) , ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P ( join ` K ) Q ) ) -> y = ( ( P ( join ` K ) Q ) ( meet ` K ) ( ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) ( join ` K ) ( ( s ( join ` K ) t ) ( meet ` K ) W ) ) ) ) ) , [_ s / t ]_ ( ( t ( join ` K ) ( ( P ( join ` K ) Q ) ( meet ` K ) W ) ) ( meet ` K ) ( Q ( join ` K ) ( ( P ( join ` K ) t ) ( meet ` K ) W ) ) ) ) ( join ` K ) ( x ( meet ` K ) W ) ) ) ) , x ) )
13	6 1 7 8 2 3 9 10 11 12 5 4	cdlemg1idlemN	\|- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ X e. B ) /\ P = Q ) -> ( F ` X ) = X )