Metamath Proof Explorer


Theorem ltrnval1

Description: Value of a lattice translation under its co-atom. (Contributed by NM, 20-May-2012)

Ref Expression
Hypotheses ltrnval1.b B = Base K
ltrnval1.l ˙ = K
ltrnval1.h H = LHyp K
ltrnval1.t T = LTrn K W
Assertion ltrnval1 K V W H F T X B X ˙ W F X = X

Proof

Step Hyp Ref Expression
1 ltrnval1.b B = Base K
2 ltrnval1.l ˙ = K
3 ltrnval1.h H = LHyp K
4 ltrnval1.t T = LTrn K W
5 eqid LDil K W = LDil K W
6 3 5 4 ltrnldil K V W H F T F LDil K W
7 6 3adant3 K V W H F T X B X ˙ W F LDil K W
8 1 2 3 5 ldilval K V W H F LDil K W X B X ˙ W F X = X
9 7 8 syld3an2 K V W H F T X B X ˙ W F X = X