pwsinvg

Description: Negation in a group power. (Contributed by Mario Carneiro, 11-Jan-2015)

	Ref	Expression
Hypotheses	pwsgrp.y	$⊢ Y = R ↑_{𝑠} I$
	pwsinvg.b	$⊢ B = {Base}_{Y}$
	pwsinvg.m	$⊢ M = {inv}_{g} (R)$
	pwsinvg.n	$⊢ N = {inv}_{g} (Y)$
Assertion	pwsinvg	$⊢ (R \in Grp \land I \in V \land X \in B) \to N (X) = M \circ X$

Proof

Step	Hyp	Ref	Expression
1		pwsgrp.y	$⊢ Y = R ↑_{𝑠} I$
2		pwsinvg.b	$⊢ B = {Base}_{Y}$
3		pwsinvg.m	$⊢ M = {inv}_{g} (R)$
4		pwsinvg.n	$⊢ N = {inv}_{g} (Y)$
5		eqid	$⊢ Scalar (R) ⨉_{𝑠} (I \times \{R\}) = Scalar (R) ⨉_{𝑠} (I \times \{R\})$
6		simp2	$⊢ (R \in Grp \land I \in V \land X \in B) \to I \in V$
7		fvexd	$⊢ (R \in Grp \land I \in V \land X \in B) \to Scalar (R) \in V$
8		simp1	$⊢ (R \in Grp \land I \in V \land X \in B) \to R \in Grp$
9		fconst6g	$⊢ R \in Grp \to (I \times \{R\}) : I ⟶ Grp$
10	8 9	syl	$⊢ (R \in Grp \land I \in V \land X \in B) \to (I \times \{R\}) : I ⟶ Grp$
11		eqid	$⊢ {Base}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))} = {Base}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))}$
12		eqid	$⊢ {inv}_{g} (Scalar (R) ⨉_{𝑠} (I \times \{R\})) = {inv}_{g} (Scalar (R) ⨉_{𝑠} (I \times \{R\}))$
13		simp3	$⊢ (R \in Grp \land I \in V \land X \in B) \to X \in B$
14		eqid	$⊢ Scalar (R) = Scalar (R)$
15	1 14	pwsval	$⊢ (R \in Grp \land I \in V) \to Y = Scalar (R) ⨉_{𝑠} (I \times \{R\})$
16	15	3adant3	$⊢ (R \in Grp \land I \in V \land X \in B) \to Y = Scalar (R) ⨉_{𝑠} (I \times \{R\})$
17	16	fveq2d	$⊢ (R \in Grp \land I \in V \land X \in B) \to {Base}_{Y} = {Base}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))}$
18	2 17	syl5eq	$⊢ (R \in Grp \land I \in V \land X \in B) \to B = {Base}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))}$
19	13 18	eleqtrd	$⊢ (R \in Grp \land I \in V \land X \in B) \to X \in {Base}_{(Scalar (R) ⨉_{𝑠} (I \times \{R\}))}$
20	5 6 7 10 11 12 19	prdsinvgd	$⊢ (R \in Grp \land I \in V \land X \in B) \to {inv}_{g} (Scalar (R) ⨉_{𝑠} (I \times \{R\})) (X) = (x \in I ⟼ {inv}_{g} ((I \times \{R\}) (x)) (X (x)))$
21		fvconst2g	$⊢ (R \in Grp \land x \in I) \to (I \times \{R\}) (x) = R$
22	8 21	sylan	$⊢ ((R \in Grp \land I \in V \land X \in B) \land x \in I) \to (I \times \{R\}) (x) = R$
23	22	fveq2d	$⊢ ((R \in Grp \land I \in V \land X \in B) \land x \in I) \to {inv}_{g} ((I \times \{R\}) (x)) = {inv}_{g} (R)$
24	23 3	eqtr4di	$⊢ ((R \in Grp \land I \in V \land X \in B) \land x \in I) \to {inv}_{g} ((I \times \{R\}) (x)) = M$
25	24	fveq1d	$⊢ ((R \in Grp \land I \in V \land X \in B) \land x \in I) \to {inv}_{g} ((I \times \{R\}) (x)) (X (x)) = M (X (x))$
26	25	mpteq2dva	$⊢ (R \in Grp \land I \in V \land X \in B) \to (x \in I ⟼ {inv}_{g} ((I \times \{R\}) (x)) (X (x))) = (x \in I ⟼ M (X (x)))$
27	20 26	eqtrd	$⊢ (R \in Grp \land I \in V \land X \in B) \to {inv}_{g} (Scalar (R) ⨉_{𝑠} (I \times \{R\})) (X) = (x \in I ⟼ M (X (x)))$
28	16	fveq2d	$⊢ (R \in Grp \land I \in V \land X \in B) \to {inv}_{g} (Y) = {inv}_{g} (Scalar (R) ⨉_{𝑠} (I \times \{R\}))$
29	4 28	syl5eq	$⊢ (R \in Grp \land I \in V \land X \in B) \to N = {inv}_{g} (Scalar (R) ⨉_{𝑠} (I \times \{R\}))$
30	29	fveq1d	$⊢ (R \in Grp \land I \in V \land X \in B) \to N (X) = {inv}_{g} (Scalar (R) ⨉_{𝑠} (I \times \{R\})) (X)$
31		eqid	$⊢ {Base}_{R} = {Base}_{R}$
32	1 31 2 8 6 13	pwselbas	$⊢ (R \in Grp \land I \in V \land X \in B) \to X : I ⟶ {Base}_{R}$
33	32	ffvelrnda	$⊢ ((R \in Grp \land I \in V \land X \in B) \land x \in I) \to X (x) \in {Base}_{R}$
34	32	feqmptd	$⊢ (R \in Grp \land I \in V \land X \in B) \to X = (x \in I ⟼ X (x))$
35	31 3	grpinvf	$⊢ R \in Grp \to M : {Base}_{R} ⟶ {Base}_{R}$
36	8 35	syl	$⊢ (R \in Grp \land I \in V \land X \in B) \to M : {Base}_{R} ⟶ {Base}_{R}$
37	36	feqmptd	$⊢ (R \in Grp \land I \in V \land X \in B) \to M = (y \in {Base}_{R} ⟼ M (y))$
38		fveq2	$⊢ y = X (x) \to M (y) = M (X (x))$
39	33 34 37 38	fmptco	$⊢ (R \in Grp \land I \in V \land X \in B) \to M \circ X = (x \in I ⟼ M (X (x)))$
40	27 30 39	3eqtr4d	$⊢ (R \in Grp \land I \in V \land X \in B) \to N (X) = M \circ X$

Metamath Proof Explorer

Theorem pwsinvg

Proof