Metamath Proof Explorer

Theorem cdlemg2idN

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

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

Proof

Step Hyp Ref Expression
1 cdlemg2id.l 
 |-  .<_ = ( le ` K )
2 cdlemg2id.a 
 |-  A = ( Atoms ` K )
3 cdlemg2id.h 
 |-  H = ( LHyp ` K )
4 cdlemg2id.t 
 |-  T = ( ( LTrn ` K ) ` W )
5 cdlemg2id.b 
 |-  B = ( Base ` K )
6 simp111 
 |-  ( ( ( ( K e. HL /\ W e. H /\ F e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( F ` P ) = Q /\ X e. B ) /\ P = Q ) -> K e. HL )
7 simp112 
 |-  ( ( ( ( K e. HL /\ W e. H /\ F e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( F ` P ) = Q /\ X e. B ) /\ P = Q ) -> W e. H )
8 simp12 
 |-  ( ( ( ( K e. HL /\ W e. H /\ F e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( F ` P ) = Q /\ X e. B ) /\ P = Q ) -> ( P e. A /\ -. P .<_ W ) )
9 simp13 
 |-  ( ( ( ( K e. HL /\ W e. H /\ F e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( F ` P ) = Q /\ X e. B ) /\ P = Q ) -> ( Q e. A /\ -. Q .<_ W ) )
10 simp113 
 |-  ( ( ( ( K e. HL /\ W e. H /\ F e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( F ` P ) = Q /\ X e. B ) /\ P = Q ) -> F e. T )
11 simp2l 
 |-  ( ( ( ( K e. HL /\ W e. H /\ F e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( F ` P ) = Q /\ X e. B ) /\ P = Q ) -> ( F ` P ) = Q )
12 eqid 
 |-  ( join ` K ) = ( join ` K )
13 eqid 
 |-  ( meet ` K ) = ( meet ` K )
14 eqid 
 |-  ( ( P ( join ` K ) Q ) ( meet ` K ) W ) = ( ( P ( join ` K ) Q ) ( meet ` K ) W )
15 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 ) ) )
16 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 ) ) )
17 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 ) )
18 5 1 12 13 2 3 4 14 15 16 17 cdlemg2dN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ ( F ` P ) = Q ) ) -> F = ( 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 ) ) )
19 6 7 8 9 10 11 18 syl222anc 
 |-  ( ( ( ( K e. HL /\ W e. H /\ F e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( F ` P ) = Q /\ X e. B ) /\ P = Q ) -> F = ( 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 ) ) )
20 19 fveq1d 
 |-  ( ( ( ( K e. HL /\ W e. H /\ F e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( F ` P ) = Q /\ X e. B ) /\ P = Q ) -> ( F ` 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 ) ) ` X ) )
21 simp2r 
 |-  ( ( ( ( K e. HL /\ W e. H /\ F e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( F ` P ) = Q /\ X e. B ) /\ P = Q ) -> X e. B )
22 simp3 
 |-  ( ( ( ( K e. HL /\ W e. H /\ F e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( F ` P ) = Q /\ X e. B ) /\ P = Q ) -> P = Q )
23 17 cdleme31id 
 |-  ( ( X e. B /\ P = Q ) -> ( ( 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 ) = X )
24 21 22 23 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H /\ F e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( F ` P ) = Q /\ X e. B ) /\ P = Q ) -> ( ( 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 ) = X )
25 20 24 eqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H /\ F e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( F ` P ) = Q /\ X e. B ) /\ P = Q ) -> ( F ` X ) = X )