ablsub2inv

Description: Abelian group subtraction of two inverses. (Contributed by Stefan O'Rear, 24-May-2015)

	Ref	Expression
Hypotheses	ablsub2inv.b	\|- B = ( Base ` G )
	ablsub2inv.m	\|- .- = ( -g ` G )
	ablsub2inv.n	\|- N = ( invg ` G )
	ablsub2inv.g	\|- ( ph -> G e. Abel )
	ablsub2inv.x	\|- ( ph -> X e. B )
	ablsub2inv.y	\|- ( ph -> Y e. B )
Assertion	ablsub2inv	\|- ( ph -> ( ( N ` X ) .- ( N ` Y ) ) = ( Y .- X ) )

Proof

Step	Hyp	Ref	Expression
1		ablsub2inv.b	\|- B = ( Base ` G )
2		ablsub2inv.m	\|- .- = ( -g ` G )
3		ablsub2inv.n	\|- N = ( invg ` G )
4		ablsub2inv.g	\|- ( ph -> G e. Abel )
5		ablsub2inv.x	\|- ( ph -> X e. B )
6		ablsub2inv.y	\|- ( ph -> Y e. B )
7		eqid	\|- ( +g ` G ) = ( +g ` G )
8		ablgrp	\|- ( G e. Abel -> G e. Grp )
9	4 8	syl	\|- ( ph -> G e. Grp )
10	1 3	grpinvcl	\|- ( ( G e. Grp /\ X e. B ) -> ( N ` X ) e. B )
11	9 5 10	syl2anc	\|- ( ph -> ( N ` X ) e. B )
12	1 7 2 3 9 11 6	grpsubinv	\|- ( ph -> ( ( N ` X ) .- ( N ` Y ) ) = ( ( N ` X ) ( +g ` G ) Y ) )
13	1 7	ablcom	\|- ( ( G e. Abel /\ ( N ` X ) e. B /\ Y e. B ) -> ( ( N ` X ) ( +g ` G ) Y ) = ( Y ( +g ` G ) ( N ` X ) ) )
14	4 11 6 13	syl3anc	\|- ( ph -> ( ( N ` X ) ( +g ` G ) Y ) = ( Y ( +g ` G ) ( N ` X ) ) )
15	1 3	grpinvinv	\|- ( ( G e. Grp /\ Y e. B ) -> ( N ` ( N ` Y ) ) = Y )
16	9 6 15	syl2anc	\|- ( ph -> ( N ` ( N ` Y ) ) = Y )
17	16	oveq1d	\|- ( ph -> ( ( N ` ( N ` Y ) ) ( +g ` G ) ( N ` X ) ) = ( Y ( +g ` G ) ( N ` X ) ) )
18	14 17	eqtr4d	\|- ( ph -> ( ( N ` X ) ( +g ` G ) Y ) = ( ( N ` ( N ` Y ) ) ( +g ` G ) ( N ` X ) ) )
19	1 3	grpinvcl	\|- ( ( G e. Grp /\ Y e. B ) -> ( N ` Y ) e. B )
20	9 6 19	syl2anc	\|- ( ph -> ( N ` Y ) e. B )
21	1 7 3	grpinvadd	\|- ( ( G e. Grp /\ X e. B /\ ( N ` Y ) e. B ) -> ( N ` ( X ( +g ` G ) ( N ` Y ) ) ) = ( ( N ` ( N ` Y ) ) ( +g ` G ) ( N ` X ) ) )
22	9 5 20 21	syl3anc	\|- ( ph -> ( N ` ( X ( +g ` G ) ( N ` Y ) ) ) = ( ( N ` ( N ` Y ) ) ( +g ` G ) ( N ` X ) ) )
23	18 22	eqtr4d	\|- ( ph -> ( ( N ` X ) ( +g ` G ) Y ) = ( N ` ( X ( +g ` G ) ( N ` Y ) ) ) )
24	1 7 3 2	grpsubval	\|- ( ( X e. B /\ Y e. B ) -> ( X .- Y ) = ( X ( +g ` G ) ( N ` Y ) ) )
25	5 6 24	syl2anc	\|- ( ph -> ( X .- Y ) = ( X ( +g ` G ) ( N ` Y ) ) )
26	25	fveq2d	\|- ( ph -> ( N ` ( X .- Y ) ) = ( N ` ( X ( +g ` G ) ( N ` Y ) ) ) )
27	23 26	eqtr4d	\|- ( ph -> ( ( N ` X ) ( +g ` G ) Y ) = ( N ` ( X .- Y ) ) )
28	1 2 3	grpinvsub	\|- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( N ` ( X .- Y ) ) = ( Y .- X ) )
29	9 5 6 28	syl3anc	\|- ( ph -> ( N ` ( X .- Y ) ) = ( Y .- X ) )
30	12 27 29	3eqtrd	\|- ( ph -> ( ( N ` X ) .- ( N ` Y ) ) = ( Y .- X ) )

Metamath Proof Explorer

Theorem ablsub2inv

Proof