Metamath Proof Explorer


Theorem cdlemg1finvtrlemN

Description: Lemma for ltrniotacnvN . (Contributed by NM, 18-Apr-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdlemg1.b B = Base K
cdlemg1.l ˙ = K
cdlemg1.j ˙ = join K
cdlemg1.m ˙ = meet K
cdlemg1.a A = Atoms K
cdlemg1.h H = LHyp K
cdlemg1.u U = P ˙ Q ˙ W
cdlemg1.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
cdlemg1.e E = P ˙ Q ˙ D ˙ s ˙ t ˙ W
cdlemg1.g G = x B if P Q ¬ x ˙ W ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = if s ˙ P ˙ Q ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E s / t D ˙ x ˙ W x
cdlemg1.t T = LTrn K W
cdlemg1.f F = ι f T | f P = Q
Assertion cdlemg1finvtrlemN K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F -1 T

Proof

Step Hyp Ref Expression
1 cdlemg1.b B = Base K
2 cdlemg1.l ˙ = K
3 cdlemg1.j ˙ = join K
4 cdlemg1.m ˙ = meet K
5 cdlemg1.a A = Atoms K
6 cdlemg1.h H = LHyp K
7 cdlemg1.u U = P ˙ Q ˙ W
8 cdlemg1.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
9 cdlemg1.e E = P ˙ Q ˙ D ˙ s ˙ t ˙ W
10 cdlemg1.g G = x B if P Q ¬ x ˙ W ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = if s ˙ P ˙ Q ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E s / t D ˙ x ˙ W x
11 cdlemg1.t T = LTrn K W
12 cdlemg1.f F = ι f T | f P = Q
13 1 2 3 4 5 6 7 8 9 10 11 12 cdlemg1b2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F = G
14 13 cnveqd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F -1 = G -1
15 1 2 3 4 5 6 7 8 9 10 11 cdleme51finvtrN K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G -1 T
16 14 15 eqeltrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F -1 T