Theorem m2detleiblem7

Description: Lemma 7 for m2detleib . (Contributed by AV, 20-Dec-2018)

	Ref	Expression
Hypotheses	m2detleiblem1.n	|- N = { 1 , 2 }
	m2detleiblem1.p	|- P = ( Base ` ( SymGrp ` N ) )
	m2detleiblem1.y	|- Y = ( ZRHom ` R )
	m2detleiblem1.s	|- S = ( pmSgn ` N )
	m2detleiblem1.o	|- .1. = ( 1r ` R )
	m2detleiblem1.i	|- I = ( invg ` R )
	m2detleiblem1.t	|- .x. = ( .r ` R )
	m2detleiblem1.m	|- .- = ( -g ` R )
Assertion	m2detleiblem7	|- ( ( R e. Ring /\ X e. ( Base ` R ) /\ Z e. ( Base ` R ) ) -> ( X ( +g ` R ) ( ( I ` .1. ) .x. Z ) ) = ( X .- Z ) )

Proof

Step	Hyp	Ref	Expression
1		m2detleiblem1.n	|- N = { 1 , 2 }
2		m2detleiblem1.p	|- P = ( Base ` ( SymGrp ` N ) )
3		m2detleiblem1.y	|- Y = ( ZRHom ` R )
4		m2detleiblem1.s	|- S = ( pmSgn ` N )
5		m2detleiblem1.o	|- .1. = ( 1r ` R )
6		m2detleiblem1.i	|- I = ( invg ` R )
7		m2detleiblem1.t	|- .x. = ( .r ` R )
8		m2detleiblem1.m	|- .- = ( -g ` R )
9		eqid	|- ( Base ` R ) = ( Base ` R )
10		simpl	|- ( ( R e. Ring /\ Z e. ( Base ` R ) ) -> R e. Ring )
11		simpr	|- ( ( R e. Ring /\ Z e. ( Base ` R ) ) -> Z e. ( Base ` R ) )
12	9 7 5 6 10 11	ringnegl	|- ( ( R e. Ring /\ Z e. ( Base ` R ) ) -> ( ( I ` .1. ) .x. Z ) = ( I ` Z ) )
13	12	3adant2	|- ( ( R e. Ring /\ X e. ( Base ` R ) /\ Z e. ( Base ` R ) ) -> ( ( I ` .1. ) .x. Z ) = ( I ` Z ) )
14	13	oveq2d	|- ( ( R e. Ring /\ X e. ( Base ` R ) /\ Z e. ( Base ` R ) ) -> ( X ( +g ` R ) ( ( I ` .1. ) .x. Z ) ) = ( X ( +g ` R ) ( I ` Z ) ) )
15		eqid	|- ( +g ` R ) = ( +g ` R )
16	9 15 6 8	grpsubval	|- ( ( X e. ( Base ` R ) /\ Z e. ( Base ` R ) ) -> ( X .- Z ) = ( X ( +g ` R ) ( I ` Z ) ) )
17	16	3adant1	|- ( ( R e. Ring /\ X e. ( Base ` R ) /\ Z e. ( Base ` R ) ) -> ( X .- Z ) = ( X ( +g ` R ) ( I ` Z ) ) )
18	14 17	eqtr4d	|- ( ( R e. Ring /\ X e. ( Base ` R ) /\ Z e. ( Base ` R ) ) -> ( X ( +g ` R ) ( ( I ` .1. ) .x. Z ) ) = ( X .- Z ) )