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 } ) ) ) ) )