Metamath Proof Explorer

Theorem asclcntr

Description: The algebra scalar lifting function maps into the center of the algebra. Equivalently, a lifted scalar is a center of the algebra. (Contributed by Zhi Wang, 11-Sep-2025)

Ref Expression
Hypotheses asclelbasALT.a ⊢ A = algSc ⁡ W
asclelbasALT.f ⊢ F = Scalar ⁡ W
asclelbasALT.b ⊢ B = Base F
asclelbasALT.w ⊢ φ → W ∈ AssAlg
asclelbasALT.c ⊢ φ → C ∈ B
asclcntr.m ⊢ M = mulGrp W
Assertion asclcntr ⊢ φ → A ⁡ C ∈ Cntr ⁡ M

Proof

Step Hyp Ref Expression
1 asclelbasALT.a ⊢ A = algSc ⁡ W
2 asclelbasALT.f ⊢ F = Scalar ⁡ W
3 asclelbasALT.b ⊢ B = Base F
4 asclelbasALT.w ⊢ φ → W ∈ AssAlg
5 asclelbasALT.c ⊢ φ → C ∈ B
6 asclcntr.m ⊢ M = mulGrp W
7 eqid ⊢ Base W = Base W
8 eqid ⊢ Cntr ⁡ M = Cntr ⁡ M
9 1 2 3 4 5 asclelbas ⊢ φ → A ⁡ C ∈ Base W
10 4 adantr ⊢ φ ∧ x ∈ Base W → W ∈ AssAlg
11 5 adantr ⊢ φ ∧ x ∈ Base W → C ∈ B
12 simpr ⊢ φ ∧ x ∈ Base W → x ∈ Base W
13 eqid ⊢ ⋅ W = ⋅ W
14 eqid ⊢ ⋅ W = ⋅ W
15 1 2 3 7 13 14 asclmul1 ⊢ W ∈ AssAlg ∧ C ∈ B ∧ x ∈ Base W → A ⁡ C ⋅ W x = C ⋅ W x
16 1 2 3 7 13 14 asclmul2 ⊢ W ∈ AssAlg ∧ C ∈ B ∧ x ∈ Base W → x ⋅ W A ⁡ C = C ⋅ W x
17 15 16 eqtr4d ⊢ W ∈ AssAlg ∧ C ∈ B ∧ x ∈ Base W → A ⁡ C ⋅ W x = x ⋅ W A ⁡ C
18 10 11 12 17 syl3anc ⊢ φ ∧ x ∈ Base W → A ⁡ C ⋅ W x = x ⋅ W A ⁡ C
19 7 6 8 9 18 elmgpcntrd ⊢ φ → A ⁡ C ∈ Cntr ⁡ M