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 ⨉ 𝑠 R
prdsinvgd2.i ⊢ φ → I ∈ W
prdsinvgd2.s ⊢ φ → S ∈ V
prdsinvgd2.r ⊢ φ → R : I ⟶ Grp
prdsinvgd2.b ⊢ B = Base Y
prdsinvgd2.n ⊢ N = inv g ⁡ Y
prdsinvgd2.x ⊢ φ → X ∈ B
prdsinvgd2.j ⊢ φ → J ∈ I
Assertion prdsinvgd2 ⊢ φ → N ⁡ X ⁡ J = inv g ⁡ R ⁡ J ⁡ X ⁡ J

Proof

Step Hyp Ref Expression
1 prdsinvgd2.y ⊢ Y = S ⨉ 𝑠 R
2 prdsinvgd2.i ⊢ φ → I ∈ W
3 prdsinvgd2.s ⊢ φ → S ∈ V
4 prdsinvgd2.r ⊢ φ → R : I ⟶ Grp
5 prdsinvgd2.b ⊢ B = Base Y
6 prdsinvgd2.n ⊢ N = inv g ⁡ Y
7 prdsinvgd2.x ⊢ φ → X ∈ B
8 prdsinvgd2.j ⊢ φ → J ∈ I
9 1 2 3 4 5 6 7 prdsinvgd ⊢ φ → N ⁡ X = x ∈ I ⟼ inv g ⁡ R ⁡ x ⁡ X ⁡ x
10 9 fveq1d ⊢ φ → N ⁡ X ⁡ J = x ∈ I ⟼ inv g ⁡ R ⁡ x ⁡ X ⁡ x ⁡ J
11 2fveq3 ⊢ x = J → inv g ⁡ R ⁡ x = inv g ⁡ R ⁡ J
12 fveq2 ⊢ x = J → X ⁡ x = X ⁡ J
13 11 12 fveq12d ⊢ x = J → inv g ⁡ R ⁡ x ⁡ X ⁡ x = inv g ⁡ R ⁡ J ⁡ X ⁡ J
14 eqid ⊢ x ∈ I ⟼ inv g ⁡ R ⁡ x ⁡ X ⁡ x = x ∈ I ⟼ inv g ⁡ R ⁡ x ⁡ X ⁡ x
15 fvex ⊢ inv g ⁡ R ⁡ J ⁡ X ⁡ J ∈ V
16 13 14 15 fvmpt ⊢ J ∈ I → x ∈ I ⟼ inv g ⁡ R ⁡ x ⁡ X ⁡ x ⁡ J = inv g ⁡ R ⁡ J ⁡ X ⁡ J
17 8 16 syl ⊢ φ → x ∈ I ⟼ inv g ⁡ R ⁡ x ⁡ X ⁡ x ⁡ J = inv g ⁡ R ⁡ J ⁡ X ⁡ J
18 10 17 eqtrd ⊢ φ → N ⁡ X ⁡ J = inv g ⁡ R ⁡ J ⁡ X ⁡ J