prdsinvgd2

Description: Negation of a single coordinate in a structure product. (Contributed by Stefan O'Rear, 11-Jan-2015)

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

Metamath Proof Explorer