# Metamath Proof Explorer

## Theorem asclinvg

Description: The group inverse (negation) of a lifted scalar is the lifted negation of the scalar. (Contributed by AV, 2-Sep-2019)

Ref Expression
Hypotheses asclinvg.a ${⊢}{A}=\mathrm{algSc}\left({W}\right)$
asclinvg.r ${⊢}{R}=\mathrm{Scalar}\left({W}\right)$
asclinvg.k ${⊢}{B}={\mathrm{Base}}_{{R}}$
asclinvg.i ${⊢}{I}={inv}_{g}\left({R}\right)$
asclinvg.j ${⊢}{J}={inv}_{g}\left({W}\right)$
Assertion asclinvg ${⊢}\left({W}\in \mathrm{LMod}\wedge {W}\in \mathrm{Ring}\wedge {C}\in {B}\right)\to {J}\left({A}\left({C}\right)\right)={A}\left({I}\left({C}\right)\right)$

### Proof

Step Hyp Ref Expression
1 asclinvg.a ${⊢}{A}=\mathrm{algSc}\left({W}\right)$
2 asclinvg.r ${⊢}{R}=\mathrm{Scalar}\left({W}\right)$
3 asclinvg.k ${⊢}{B}={\mathrm{Base}}_{{R}}$
4 asclinvg.i ${⊢}{I}={inv}_{g}\left({R}\right)$
5 asclinvg.j ${⊢}{J}={inv}_{g}\left({W}\right)$
6 simp2 ${⊢}\left({W}\in \mathrm{LMod}\wedge {W}\in \mathrm{Ring}\wedge {C}\in {B}\right)\to {W}\in \mathrm{Ring}$
7 simp1 ${⊢}\left({W}\in \mathrm{LMod}\wedge {W}\in \mathrm{Ring}\wedge {C}\in {B}\right)\to {W}\in \mathrm{LMod}$
8 1 2 6 7 asclghm ${⊢}\left({W}\in \mathrm{LMod}\wedge {W}\in \mathrm{Ring}\wedge {C}\in {B}\right)\to {A}\in \left({R}\mathrm{GrpHom}{W}\right)$
9 simp3 ${⊢}\left({W}\in \mathrm{LMod}\wedge {W}\in \mathrm{Ring}\wedge {C}\in {B}\right)\to {C}\in {B}$
10 3 4 5 ghminv ${⊢}\left({A}\in \left({R}\mathrm{GrpHom}{W}\right)\wedge {C}\in {B}\right)\to {A}\left({I}\left({C}\right)\right)={J}\left({A}\left({C}\right)\right)$
11 10 eqcomd ${⊢}\left({A}\in \left({R}\mathrm{GrpHom}{W}\right)\wedge {C}\in {B}\right)\to {J}\left({A}\left({C}\right)\right)={A}\left({I}\left({C}\right)\right)$
12 8 9 11 syl2anc ${⊢}\left({W}\in \mathrm{LMod}\wedge {W}\in \mathrm{Ring}\wedge {C}\in {B}\right)\to {J}\left({A}\left({C}\right)\right)={A}\left({I}\left({C}\right)\right)$