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 = algSc ⁡ W
asclinvg.r ⊢ R = Scalar ⁡ W
asclinvg.k ⊢ B = Base R
asclinvg.i ⊢ I = inv g ⁡ R
asclinvg.j ⊢ J = inv g ⁡ W
Assertion asclinvg ⊢ W ∈ LMod ∧ W ∈ Ring ∧ C ∈ B → J ⁡ A ⁡ C = A ⁡ I ⁡ C

Proof

Step Hyp Ref Expression
1 asclinvg.a ⊢ A = algSc ⁡ W
2 asclinvg.r ⊢ R = Scalar ⁡ W
3 asclinvg.k ⊢ B = Base R
4 asclinvg.i ⊢ I = inv g ⁡ R
5 asclinvg.j ⊢ J = inv g ⁡ W
6 simp2 ⊢ W ∈ LMod ∧ W ∈ Ring ∧ C ∈ B → W ∈ Ring
7 simp1 ⊢ W ∈ LMod ∧ W ∈ Ring ∧ C ∈ B → W ∈ LMod
8 1 2 6 7 asclghm ⊢ W ∈ LMod ∧ W ∈ Ring ∧ C ∈ B → A ∈ R GrpHom W
9 simp3 ⊢ W ∈ LMod ∧ W ∈ Ring ∧ C ∈ B → C ∈ B
10 3 4 5 ghminv ⊢ A ∈ R GrpHom W ∧ C ∈ B → A ⁡ I ⁡ C = J ⁡ A ⁡ C
11 10 eqcomd ⊢ A ∈ R GrpHom W ∧ C ∈ B → J ⁡ A ⁡ C = A ⁡ I ⁡ C
12 8 9 11 syl2anc ⊢ W ∈ LMod ∧ W ∈ Ring ∧ C ∈ B → J ⁡ A ⁡ C = A ⁡ I ⁡ C