# Metamath Proof Explorer

## 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 ) )`
` |-  ( ( R e. Ring /\ X e. ( Base ` R ) /\ Z e. ( Base ` R ) ) -> ( ( I ` .1. ) .x. Z ) = ( I ` Z ) )`
` |-  ( ( R e. Ring /\ X e. ( Base ` R ) /\ Z e. ( Base ` R ) ) -> ( X ( +g ` R ) ( ( I ` .1. ) .x. Z ) ) = ( X ( +g ` R ) ( I ` Z ) ) )`
` |-  ( +g ` R ) = ( +g ` R )`
` |-  ( ( X e. ( Base ` R ) /\ Z e. ( Base ` R ) ) -> ( X .- Z ) = ( X ( +g ` R ) ( I ` Z ) ) )`
` |-  ( ( R e. Ring /\ X e. ( Base ` R ) /\ Z e. ( Base ` R ) ) -> ( X .- Z ) = ( X ( +g ` R ) ( I ` Z ) ) )`
` |-  ( ( R e. Ring /\ X e. ( Base ` R ) /\ Z e. ( Base ` R ) ) -> ( X ( +g ` R ) ( ( I ` .1. ) .x. Z ) ) = ( X .- Z ) )`