Metamath Proof Explorer


Theorem cdlemkuv-2N

Description: Part of proof of Lemma K of Crawley p. 118. Value of the sigma_2 (p) function, given V . (Contributed by NM, 2-Jul-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdlemk2.b B = Base K
cdlemk2.l ˙ = K
cdlemk2.j ˙ = join K
cdlemk2.m ˙ = meet K
cdlemk2.a A = Atoms K
cdlemk2.h H = LHyp K
cdlemk2.t T = LTrn K W
cdlemk2.r R = trL K W
cdlemk2.s S = f T ι i T | i P = P ˙ R f ˙ N P ˙ R f F -1
cdlemk2.q Q = S C
cdlemk2.v V = d T ι k T | k P = P ˙ R d ˙ Q P ˙ R d C -1
Assertion cdlemkuv-2N G T V G = ι k T | k P = P ˙ R G ˙ Q P ˙ R G C -1

Proof

Step Hyp Ref Expression
1 cdlemk2.b B = Base K
2 cdlemk2.l ˙ = K
3 cdlemk2.j ˙ = join K
4 cdlemk2.m ˙ = meet K
5 cdlemk2.a A = Atoms K
6 cdlemk2.h H = LHyp K
7 cdlemk2.t T = LTrn K W
8 cdlemk2.r R = trL K W
9 cdlemk2.s S = f T ι i T | i P = P ˙ R f ˙ N P ˙ R f F -1
10 cdlemk2.q Q = S C
11 cdlemk2.v V = d T ι k T | k P = P ˙ R d ˙ Q P ˙ R d C -1
12 1 2 3 5 6 7 8 4 11 cdlemksv G T V G = ι k T | k P = P ˙ R G ˙ Q P ˙ R G C -1