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	⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
	prdsinvgd2.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	prdsinvgd2.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
	prdsinvgd2.r	⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Grp )
	prdsinvgd2.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
	prdsinvgd2.n	⊢ 𝑁 = ( invg ‘ 𝑌 )
	prdsinvgd2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	prdsinvgd2.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐼 )
Assertion	prdsinvgd2	⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑋 ) ‘ 𝐽 ) = ( ( invg ‘ ( 𝑅 ‘ 𝐽 ) ) ‘ ( 𝑋 ‘ 𝐽 ) ) )

Proof

Step	Hyp	Ref	Expression
1		prdsinvgd2.y	⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
2		prdsinvgd2.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
3		prdsinvgd2.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
4		prdsinvgd2.r	⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Grp )
5		prdsinvgd2.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
6		prdsinvgd2.n	⊢ 𝑁 = ( invg ‘ 𝑌 )
7		prdsinvgd2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8		prdsinvgd2.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐼 )
9	1 2 3 4 5 6 7	prdsinvgd	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑋 ) = ( 𝑥 ∈ 𝐼 ↦ ( ( invg ‘ ( 𝑅 ‘ 𝑥 ) ) ‘ ( 𝑋 ‘ 𝑥 ) ) ) )
10	9	fveq1d	⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑋 ) ‘ 𝐽 ) = ( ( 𝑥 ∈ 𝐼 ↦ ( ( invg ‘ ( 𝑅 ‘ 𝑥 ) ) ‘ ( 𝑋 ‘ 𝑥 ) ) ) ‘ 𝐽 ) )
11		2fveq3	⊢ ( 𝑥 = 𝐽 → ( invg ‘ ( 𝑅 ‘ 𝑥 ) ) = ( invg ‘ ( 𝑅 ‘ 𝐽 ) ) )
12		fveq2	⊢ ( 𝑥 = 𝐽 → ( 𝑋 ‘ 𝑥 ) = ( 𝑋 ‘ 𝐽 ) )
13	11 12	fveq12d	⊢ ( 𝑥 = 𝐽 → ( ( invg ‘ ( 𝑅 ‘ 𝑥 ) ) ‘ ( 𝑋 ‘ 𝑥 ) ) = ( ( invg ‘ ( 𝑅 ‘ 𝐽 ) ) ‘ ( 𝑋 ‘ 𝐽 ) ) )
14		eqid	⊢ ( 𝑥 ∈ 𝐼 ↦ ( ( invg ‘ ( 𝑅 ‘ 𝑥 ) ) ‘ ( 𝑋 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( invg ‘ ( 𝑅 ‘ 𝑥 ) ) ‘ ( 𝑋 ‘ 𝑥 ) ) )
15		fvex	⊢ ( ( invg ‘ ( 𝑅 ‘ 𝐽 ) ) ‘ ( 𝑋 ‘ 𝐽 ) ) ∈ V
16	13 14 15	fvmpt	⊢ ( 𝐽 ∈ 𝐼 → ( ( 𝑥 ∈ 𝐼 ↦ ( ( invg ‘ ( 𝑅 ‘ 𝑥 ) ) ‘ ( 𝑋 ‘ 𝑥 ) ) ) ‘ 𝐽 ) = ( ( invg ‘ ( 𝑅 ‘ 𝐽 ) ) ‘ ( 𝑋 ‘ 𝐽 ) ) )
17	8 16	syl	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ ( ( invg ‘ ( 𝑅 ‘ 𝑥 ) ) ‘ ( 𝑋 ‘ 𝑥 ) ) ) ‘ 𝐽 ) = ( ( invg ‘ ( 𝑅 ‘ 𝐽 ) ) ‘ ( 𝑋 ‘ 𝐽 ) ) )
18	10 17	eqtrd	⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑋 ) ‘ 𝐽 ) = ( ( invg ‘ ( 𝑅 ‘ 𝐽 ) ) ‘ ( 𝑋 ‘ 𝐽 ) ) )