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