Metamath Proof Explorer


Theorem istrnN

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

Ref Expression
Hypotheses trnset.a A = Atoms K
trnset.s S = PSubSp K
trnset.p + ˙ = + 𝑃 K
trnset.o ˙ = 𝑃 K
trnset.w W = WAtoms K
trnset.m M = PAut K
trnset.l L = Dil K
trnset.t T = Trn K
Assertion istrnN K B D A F T D F L D q W D r W D q + ˙ F q ˙ D = r + ˙ F r ˙ D

Proof

Step Hyp Ref Expression
1 trnset.a A = Atoms K
2 trnset.s S = PSubSp K
3 trnset.p + ˙ = + 𝑃 K
4 trnset.o ˙ = 𝑃 K
5 trnset.w W = WAtoms K
6 trnset.m M = PAut K
7 trnset.l L = Dil K
8 trnset.t T = Trn K
9 1 2 3 4 5 6 7 8 trnsetN K B D A T D = f L D | q W D r W D q + ˙ f q ˙ D = r + ˙ f r ˙ D
10 9 eleq2d K B D A F T D F f L D | q W D r W D q + ˙ f q ˙ D = r + ˙ f r ˙ D
11 fveq1 f = F f q = F q
12 11 oveq2d f = F q + ˙ f q = q + ˙ F q
13 12 ineq1d f = F q + ˙ f q ˙ D = q + ˙ F q ˙ D
14 fveq1 f = F f r = F r
15 14 oveq2d f = F r + ˙ f r = r + ˙ F r
16 15 ineq1d f = F r + ˙ f r ˙ D = r + ˙ F r ˙ D
17 13 16 eqeq12d f = F q + ˙ f q ˙ D = r + ˙ f r ˙ D q + ˙ F q ˙ D = r + ˙ F r ˙ D
18 17 2ralbidv f = F q W D r W D q + ˙ f q ˙ D = r + ˙ f r ˙ D q W D r W D q + ˙ F q ˙ D = r + ˙ F r ˙ D
19 18 elrab F f L D | q W D r W D q + ˙ f q ˙ D = r + ˙ f r ˙ D F L D q W D r W D q + ˙ F q ˙ D = r + ˙ F r ˙ D
20 10 19 bitrdi K B D A F T D F L D q W D r W D q + ˙ F q ˙ D = r + ˙ F r ˙ D