Metamath Proof Explorer


Theorem isdilN

Description: The predicate "is a dilation". (Contributed by NM, 4-Feb-2012) (New usage is discouraged.)

Ref Expression
Hypotheses dilset.a A = Atoms K
dilset.s S = PSubSp K
dilset.w W = WAtoms K
dilset.m M = PAut K
dilset.l L = Dil K
Assertion isdilN K B D A F L D F M x S x W D F x = x

Proof

Step Hyp Ref Expression
1 dilset.a A = Atoms K
2 dilset.s S = PSubSp K
3 dilset.w W = WAtoms K
4 dilset.m M = PAut K
5 dilset.l L = Dil K
6 1 2 3 4 5 dilsetN K B D A L D = f M | x S x W D f x = x
7 6 eleq2d K B D A F L D F f M | x S x W D f x = x
8 fveq1 f = F f x = F x
9 8 eqeq1d f = F f x = x F x = x
10 9 imbi2d f = F x W D f x = x x W D F x = x
11 10 ralbidv f = F x S x W D f x = x x S x W D F x = x
12 11 elrab F f M | x S x W D f x = x F M x S x W D F x = x
13 7 12 bitrdi K B D A F L D F M x S x W D F x = x