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 )