pwssub

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

	Ref	Expression
Hypotheses	pwsgrp.y	$⊢ Y = R ↑_{𝑠} I$
	pwsinvg.b	$⊢ B = {Base}_{Y}$
	pwssub.m	$⊢ M = -_{R}$
	pwssub.n	$⊢ \underset{˙}{-} = -_{Y}$
Assertion	pwssub	$⊢ ((R \in Grp \land I \in V) \land (F \in B \land G \in B)) \to F \underset{˙}{-} G = F M_{f} G$

Proof

Step	Hyp	Ref	Expression
1		pwsgrp.y	$⊢ Y = R ↑_{𝑠} I$
2		pwsinvg.b	$⊢ B = {Base}_{Y}$
3		pwssub.m	$⊢ M = -_{R}$
4		pwssub.n	$⊢ \underset{˙}{-} = -_{Y}$
5		simplr	$⊢ ((R \in Grp \land I \in V) \land (F \in B \land G \in B)) \to I \in V$
6		eqid	$⊢ {Base}_{R} = {Base}_{R}$
7		simpll	$⊢ ((R \in Grp \land I \in V) \land (F \in B \land G \in B)) \to R \in Grp$
8		simprl	$⊢ ((R \in Grp \land I \in V) \land (F \in B \land G \in B)) \to F \in B$
9	1 6 2 7 5 8	pwselbas	$⊢ ((R \in Grp \land I \in V) \land (F \in B \land G \in B)) \to F : I ⟶ {Base}_{R}$
10	9	ffvelcdmda	$⊢ (((R \in Grp \land I \in V) \land (F \in B \land G \in B)) \land x \in I) \to F (x) \in {Base}_{R}$
11		fvexd	$⊢ (((R \in Grp \land I \in V) \land (F \in B \land G \in B)) \land x \in I) \to {inv}_{g} (R) (G (x)) \in V$
12	9	feqmptd	$⊢ ((R \in Grp \land I \in V) \land (F \in B \land G \in B)) \to F = (x \in I ⟼ F (x))$
13		simprr	$⊢ ((R \in Grp \land I \in V) \land (F \in B \land G \in B)) \to G \in B$
14		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
15		eqid	$⊢ {inv}_{g} (Y) = {inv}_{g} (Y)$
16	1 2 14 15	pwsinvg	$⊢ (R \in Grp \land I \in V \land G \in B) \to {inv}_{g} (Y) (G) = {inv}_{g} (R) \circ G$
17	7 5 13 16	syl3anc	$⊢ ((R \in Grp \land I \in V) \land (F \in B \land G \in B)) \to {inv}_{g} (Y) (G) = {inv}_{g} (R) \circ G$
18	1 6 2 7 5 13	pwselbas	$⊢ ((R \in Grp \land I \in V) \land (F \in B \land G \in B)) \to G : I ⟶ {Base}_{R}$
19	18	ffvelcdmda	$⊢ (((R \in Grp \land I \in V) \land (F \in B \land G \in B)) \land x \in I) \to G (x) \in {Base}_{R}$
20	18	feqmptd	$⊢ ((R \in Grp \land I \in V) \land (F \in B \land G \in B)) \to G = (x \in I ⟼ G (x))$
21	6 14	grpinvf	$⊢ R \in Grp \to {inv}_{g} (R) : {Base}_{R} ⟶ {Base}_{R}$
22	21	ad2antrr	$⊢ ((R \in Grp \land I \in V) \land (F \in B \land G \in B)) \to {inv}_{g} (R) : {Base}_{R} ⟶ {Base}_{R}$
23	22	feqmptd	$⊢ ((R \in Grp \land I \in V) \land (F \in B \land G \in B)) \to {inv}_{g} (R) = (y \in {Base}_{R} ⟼ {inv}_{g} (R) (y))$
24		fveq2	$⊢ y = G (x) \to {inv}_{g} (R) (y) = {inv}_{g} (R) (G (x))$
25	19 20 23 24	fmptco	$⊢ ((R \in Grp \land I \in V) \land (F \in B \land G \in B)) \to {inv}_{g} (R) \circ G = (x \in I ⟼ {inv}_{g} (R) (G (x)))$
26	17 25	eqtrd	$⊢ ((R \in Grp \land I \in V) \land (F \in B \land G \in B)) \to {inv}_{g} (Y) (G) = (x \in I ⟼ {inv}_{g} (R) (G (x)))$
27	5 10 11 12 26	offval2	$⊢ ((R \in Grp \land I \in V) \land (F \in B \land G \in B)) \to F {+_{R}}_{f} {inv}_{g} (Y) (G) = (x \in I ⟼ F (x) +_{R} {inv}_{g} (R) (G (x)))$
28	1	pwsgrp	$⊢ (R \in Grp \land I \in V) \to Y \in Grp$
29	2 15	grpinvcl	$⊢ (Y \in Grp \land G \in B) \to {inv}_{g} (Y) (G) \in B$
30	28 13 29	syl2an2r	$⊢ ((R \in Grp \land I \in V) \land (F \in B \land G \in B)) \to {inv}_{g} (Y) (G) \in B$
31		eqid	$⊢ +_{R} = +_{R}$
32		eqid	$⊢ +_{Y} = +_{Y}$
33	1 2 7 5 8 30 31 32	pwsplusgval	$⊢ ((R \in Grp \land I \in V) \land (F \in B \land G \in B)) \to F +_{Y} {inv}_{g} (Y) (G) = F {+_{R}}_{f} {inv}_{g} (Y) (G)$
34	6 31 14 3	grpsubval	$⊢ (F (x) \in {Base}_{R} \land G (x) \in {Base}_{R}) \to F (x) M G (x) = F (x) +_{R} {inv}_{g} (R) (G (x))$
35	10 19 34	syl2anc	$⊢ (((R \in Grp \land I \in V) \land (F \in B \land G \in B)) \land x \in I) \to F (x) M G (x) = F (x) +_{R} {inv}_{g} (R) (G (x))$
36	35	mpteq2dva	$⊢ ((R \in Grp \land I \in V) \land (F \in B \land G \in B)) \to (x \in I ⟼ F (x) M G (x)) = (x \in I ⟼ F (x) +_{R} {inv}_{g} (R) (G (x)))$
37	27 33 36	3eqtr4d	$⊢ ((R \in Grp \land I \in V) \land (F \in B \land G \in B)) \to F +_{Y} {inv}_{g} (Y) (G) = (x \in I ⟼ F (x) M G (x))$
38	2 32 15 4	grpsubval	$⊢ (F \in B \land G \in B) \to F \underset{˙}{-} G = F +_{Y} {inv}_{g} (Y) (G)$
39	38	adantl	$⊢ ((R \in Grp \land I \in V) \land (F \in B \land G \in B)) \to F \underset{˙}{-} G = F +_{Y} {inv}_{g} (Y) (G)$
40	5 10 19 12 20	offval2	$⊢ ((R \in Grp \land I \in V) \land (F \in B \land G \in B)) \to F M_{f} G = (x \in I ⟼ F (x) M G (x))$
41	37 39 40	3eqtr4d	$⊢ ((R \in Grp \land I \in V) \land (F \in B \land G \in B)) \to F \underset{˙}{-} G = F M_{f} G$

Metamath Proof Explorer

Theorem pwssub

Proof