Metamath Proof Explorer


Theorem diaelval

Description: Member of the partial isomorphism A for a lattice K . (Contributed by NM, 3-Dec-2013)

Ref Expression
Hypotheses diaval.b B = Base K
diaval.l ˙ = K
diaval.h H = LHyp K
diaval.t T = LTrn K W
diaval.r R = trL K W
diaval.i I = DIsoA K W
Assertion diaelval K V W H X B X ˙ W F I X F T R F ˙ X

Proof

Step Hyp Ref Expression
1 diaval.b B = Base K
2 diaval.l ˙ = K
3 diaval.h H = LHyp K
4 diaval.t T = LTrn K W
5 diaval.r R = trL K W
6 diaval.i I = DIsoA K W
7 1 2 3 4 5 6 diaval K V W H X B X ˙ W I X = f T | R f ˙ X
8 7 eleq2d K V W H X B X ˙ W F I X F f T | R f ˙ X
9 fveq2 f = F R f = R F
10 9 breq1d f = F R f ˙ X R F ˙ X
11 10 elrab F f T | R f ˙ X F T R F ˙ X
12 8 11 bitrdi K V W H X B X ˙ W F I X F T R F ˙ X