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
|- .+ = ( +P ` K )
trnset.o
|- ._|_ = ( _|_P ` K )
trnset.w
|- W = ( WAtoms ` K )
trnset.m
|- M = ( PAut ` K )
trnset.l
|- L = ( Dil ` K )
trnset.t
|- T = ( Trn ` K )
Assertion istrnN
|- ( ( K e. B /\ D e. A ) -> ( F e. ( T ` D ) <-> ( F e. ( L ` D ) /\ A. q e. ( W ` D ) A. r e. ( W ` D ) ( ( q .+ ( F ` q ) ) i^i ( ._|_ ` { D } ) ) = ( ( r .+ ( F ` r ) ) i^i ( ._|_ ` { D } ) ) ) ) )

Proof

Step Hyp Ref Expression
1 trnset.a
 |-  A = ( Atoms ` K )
2 trnset.s
 |-  S = ( PSubSp ` K )
3 trnset.p
 |-  .+ = ( +P ` K )
4 trnset.o
 |-  ._|_ = ( _|_P ` 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 e. B /\ D e. A ) -> ( T ` D ) = { f e. ( L ` D ) | A. q e. ( W ` D ) A. r e. ( W ` D ) ( ( q .+ ( f ` q ) ) i^i ( ._|_ ` { D } ) ) = ( ( r .+ ( f ` r ) ) i^i ( ._|_ ` { D } ) ) } )
10 9 eleq2d
 |-  ( ( K e. B /\ D e. A ) -> ( F e. ( T ` D ) <-> F e. { f e. ( L ` D ) | A. q e. ( W ` D ) A. r e. ( W ` D ) ( ( q .+ ( f ` q ) ) i^i ( ._|_ ` { D } ) ) = ( ( r .+ ( f ` r ) ) i^i ( ._|_ ` { 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 ) ) i^i ( ._|_ ` { D } ) ) = ( ( q .+ ( F ` q ) ) i^i ( ._|_ ` { 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 ) ) i^i ( ._|_ ` { D } ) ) = ( ( r .+ ( F ` r ) ) i^i ( ._|_ ` { D } ) ) )
17 13 16 eqeq12d
 |-  ( f = F -> ( ( ( q .+ ( f ` q ) ) i^i ( ._|_ ` { D } ) ) = ( ( r .+ ( f ` r ) ) i^i ( ._|_ ` { D } ) ) <-> ( ( q .+ ( F ` q ) ) i^i ( ._|_ ` { D } ) ) = ( ( r .+ ( F ` r ) ) i^i ( ._|_ ` { D } ) ) ) )
18 17 2ralbidv
 |-  ( f = F -> ( A. q e. ( W ` D ) A. r e. ( W ` D ) ( ( q .+ ( f ` q ) ) i^i ( ._|_ ` { D } ) ) = ( ( r .+ ( f ` r ) ) i^i ( ._|_ ` { D } ) ) <-> A. q e. ( W ` D ) A. r e. ( W ` D ) ( ( q .+ ( F ` q ) ) i^i ( ._|_ ` { D } ) ) = ( ( r .+ ( F ` r ) ) i^i ( ._|_ ` { D } ) ) ) )
19 18 elrab
 |-  ( F e. { f e. ( L ` D ) | A. q e. ( W ` D ) A. r e. ( W ` D ) ( ( q .+ ( f ` q ) ) i^i ( ._|_ ` { D } ) ) = ( ( r .+ ( f ` r ) ) i^i ( ._|_ ` { D } ) ) } <-> ( F e. ( L ` D ) /\ A. q e. ( W ` D ) A. r e. ( W ` D ) ( ( q .+ ( F ` q ) ) i^i ( ._|_ ` { D } ) ) = ( ( r .+ ( F ` r ) ) i^i ( ._|_ ` { D } ) ) ) )
20 10 19 bitrdi
 |-  ( ( K e. B /\ D e. A ) -> ( F e. ( T ` D ) <-> ( F e. ( L ` D ) /\ A. q e. ( W ` D ) A. r e. ( W ` D ) ( ( q .+ ( F ` q ) ) i^i ( ._|_ ` { D } ) ) = ( ( r .+ ( F ` r ) ) i^i ( ._|_ ` { D } ) ) ) ) )