Metamath Proof Explorer


Theorem cdlemfnid

Description: cdlemf with additional constraint of non-identity. (Contributed by NM, 20-Jun-2013)

Ref Expression
Hypotheses cdlemfnid.b B = Base K
cdlemfnid.l ˙ = K
cdlemfnid.a A = Atoms K
cdlemfnid.h H = LHyp K
cdlemfnid.t T = LTrn K W
cdlemfnid.r R = trL K W
Assertion cdlemfnid K HL W H U A U ˙ W f T R f = U f I B

Proof

Step Hyp Ref Expression
1 cdlemfnid.b B = Base K
2 cdlemfnid.l ˙ = K
3 cdlemfnid.a A = Atoms K
4 cdlemfnid.h H = LHyp K
5 cdlemfnid.t T = LTrn K W
6 cdlemfnid.r R = trL K W
7 2 3 4 5 6 cdlemf K HL W H U A U ˙ W f T R f = U
8 simp3 K HL W H U A U ˙ W f T R f = U R f = U
9 simp1rl K HL W H U A U ˙ W f T R f = U U A
10 8 9 eqeltrd K HL W H U A U ˙ W f T R f = U R f A
11 simp1l K HL W H U A U ˙ W f T R f = U K HL W H
12 simp2 K HL W H U A U ˙ W f T R f = U f T
13 1 3 4 5 6 trlnidatb K HL W H f T f I B R f A
14 11 12 13 syl2anc K HL W H U A U ˙ W f T R f = U f I B R f A
15 10 14 mpbird K HL W H U A U ˙ W f T R f = U f I B
16 8 15 jca K HL W H U A U ˙ W f T R f = U R f = U f I B
17 16 3expia K HL W H U A U ˙ W f T R f = U R f = U f I B
18 17 reximdva K HL W H U A U ˙ W f T R f = U f T R f = U f I B
19 7 18 mpd K HL W H U A U ˙ W f T R f = U f I B