This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem grpnpcan

Description: Cancellation law for subtraction ( npcan analog). (Contributed by NM, 19-Apr-2014)

		Ref	Expression
	Hypotheses	grpsubadd.b	\|- B = ( Base ` G )
		grpsubadd.p	\|- .+ = ( +g ` G )
		grpsubadd.m	\|- .- = ( -g ` G )
	Assertion	grpnpcan	\|- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( ( X .- Y ) .+ Y ) = X )

Proof

Step	Hyp	Ref	Expression
1		grpsubadd.b	\|- B = ( Base ` G )
2		grpsubadd.p	\|- .+ = ( +g ` G )
3		grpsubadd.m	\|- .- = ( -g ` G )
4		eqid	\|- ( invg ` G ) = ( invg ` G )
5	1 4	grpinvcl	\|- ( ( G e. Grp /\ Y e. B ) -> ( ( invg ` G ) ` Y ) e. B )
6	5	3adant2	\|- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( ( invg ` G ) ` Y ) e. B )
7	1 2	grpcl	\|- ( ( G e. Grp /\ X e. B /\ ( ( invg ` G ) ` Y ) e. B ) -> ( X .+ ( ( invg ` G ) ` Y ) ) e. B )
8	6 7	syld3an3	\|- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( X .+ ( ( invg ` G ) ` Y ) ) e. B )
9	1 2 4 3	grpsubval	\|- ( ( ( X .+ ( ( invg ` G ) ` Y ) ) e. B /\ ( ( invg ` G ) ` Y ) e. B ) -> ( ( X .+ ( ( invg ` G ) ` Y ) ) .- ( ( invg ` G ) ` Y ) ) = ( ( X .+ ( ( invg ` G ) ` Y ) ) .+ ( ( invg ` G ) ` ( ( invg ` G ) ` Y ) ) ) )
10	8 6 9	syl2anc	\|- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( ( X .+ ( ( invg ` G ) ` Y ) ) .- ( ( invg ` G ) ` Y ) ) = ( ( X .+ ( ( invg ` G ) ` Y ) ) .+ ( ( invg ` G ) ` ( ( invg ` G ) ` Y ) ) ) )
11	1 2 3	grppncan	\|- ( ( G e. Grp /\ X e. B /\ ( ( invg ` G ) ` Y ) e. B ) -> ( ( X .+ ( ( invg ` G ) ` Y ) ) .- ( ( invg ` G ) ` Y ) ) = X )
12	6 11	syld3an3	\|- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( ( X .+ ( ( invg ` G ) ` Y ) ) .- ( ( invg ` G ) ` Y ) ) = X )
13	1 2 4 3	grpsubval	\|- ( ( X e. B /\ Y e. B ) -> ( X .- Y ) = ( X .+ ( ( invg ` G ) ` Y ) ) )
14	13	3adant1	\|- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( X .- Y ) = ( X .+ ( ( invg ` G ) ` Y ) ) )
15	14	eqcomd	\|- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( X .+ ( ( invg ` G ) ` Y ) ) = ( X .- Y ) )
16	1 4	grpinvinv	\|- ( ( G e. Grp /\ Y e. B ) -> ( ( invg ` G ) ` ( ( invg ` G ) ` Y ) ) = Y )
17	16	3adant2	\|- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( ( invg ` G ) ` ( ( invg ` G ) ` Y ) ) = Y )
18	15 17	oveq12d	\|- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( ( X .+ ( ( invg ` G ) ` Y ) ) .+ ( ( invg ` G ) ` ( ( invg ` G ) ` Y ) ) ) = ( ( X .- Y ) .+ Y ) )
19	10 12 18	3eqtr3rd	\|- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( ( X .- Y ) .+ Y ) = X )