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