This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prdsinvgd2

Description: Negation of a single coordinate in a structure product. (Contributed by Stefan O'Rear, 11-Jan-2015)

Ref Expression
Hypotheses prdsinvgd2.y 
|- Y = ( S Xs_ R )
prdsinvgd2.i 
|- ( ph -> I e. W )
prdsinvgd2.s 
|- ( ph -> S e. V )
prdsinvgd2.r 
|- ( ph -> R : I --> Grp )
prdsinvgd2.b 
|- B = ( Base ` Y )
prdsinvgd2.n 
|- N = ( invg ` Y )
prdsinvgd2.x 
|- ( ph -> X e. B )
prdsinvgd2.j 
|- ( ph -> J e. I )
Assertion prdsinvgd2 
|- ( ph -> ( ( N ` X ) ` J ) = ( ( invg ` ( R ` J ) ) ` ( X ` J ) ) )

Proof

Step Hyp Ref Expression
1 prdsinvgd2.y 
 |-  Y = ( S Xs_ R )
2 prdsinvgd2.i 
 |-  ( ph -> I e. W )
3 prdsinvgd2.s 
 |-  ( ph -> S e. V )
4 prdsinvgd2.r 
 |-  ( ph -> R : I --> Grp )
5 prdsinvgd2.b 
 |-  B = ( Base ` Y )
6 prdsinvgd2.n 
 |-  N = ( invg ` Y )
7 prdsinvgd2.x 
 |-  ( ph -> X e. B )
8 prdsinvgd2.j 
 |-  ( ph -> J e. I )
9 1 2 3 4 5 6 7 prdsinvgd 
 |-  ( ph -> ( N ` X ) = ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) ) )
10 9 fveq1d 
 |-  ( ph -> ( ( N ` X ) ` J ) = ( ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) ) ` J ) )
11 2fveq3 
 |-  ( x = J -> ( invg ` ( R ` x ) ) = ( invg ` ( R ` J ) ) )
12 fveq2 
 |-  ( x = J -> ( X ` x ) = ( X ` J ) )
13 11 12 fveq12d 
 |-  ( x = J -> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) = ( ( invg ` ( R ` J ) ) ` ( X ` J ) ) )
14 eqid 
 |-  ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) ) = ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) )
15 fvex 
 |-  ( ( invg ` ( R ` J ) ) ` ( X ` J ) ) e. _V
16 13 14 15 fvmpt 
 |-  ( J e. I -> ( ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) ) ` J ) = ( ( invg ` ( R ` J ) ) ` ( X ` J ) ) )
17 8 16 syl 
 |-  ( ph -> ( ( x e. I |-> ( ( invg ` ( R ` x ) ) ` ( X ` x ) ) ) ` J ) = ( ( invg ` ( R ` J ) ) ` ( X ` J ) ) )
18 10 17 eqtrd 
 |-  ( ph -> ( ( N ` X ) ` J ) = ( ( invg ` ( R ` J ) ) ` ( X ` J ) ) )