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 𝑌 = ( 𝑆 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 ‘ ( 𝑅𝐽 ) ) ‘ ( 𝑋𝐽 ) ) )