Description: Scalars are commutative after being lifted.
However, the scalars themselves are not necessarily commutative if the algebra is not a faithful module. For example, Let F be the 2 by 2 upper triangular matrix algebra over a commutative ring W . It is provable that F is in general non-commutative. Define scalar multiplication C .x. X as multipying the top-left entry, which is a "vector" element of W , of the "scalar" C , which is now an upper triangular matrix, with the "vector" X e. ( BaseW ) .
Equivalently, the algebra scalar lifting function is not necessarily injective unless the algebra is faithful. Therefore, all "scalar injection" was renamed.
Alternate proof involves assa2ass , assa2ass2 , and asclval , by setting X and Y the multiplicative identity of the algebra.
(Contributed by Zhi Wang, 11-Sep-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | asclelbasALT.a | ⊢ 𝐴 = ( algSc ‘ 𝑊 ) | |
| asclelbasALT.f | ⊢ 𝐹 = ( Scalar ‘ 𝑊 ) | ||
| asclelbasALT.b | ⊢ 𝐵 = ( Base ‘ 𝐹 ) | ||
| asclelbasALT.w | ⊢ ( 𝜑 → 𝑊 ∈ AssAlg ) | ||
| asclelbasALT.c | ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 ) | ||
| asclcom.m | ⊢ ∗ = ( .r ‘ 𝐹 ) | ||
| asclcom.d | ⊢ ( 𝜑 → 𝐷 ∈ 𝐵 ) | ||
| Assertion | asclcom | ⊢ ( 𝜑 → ( 𝐴 ‘ ( 𝐶 ∗ 𝐷 ) ) = ( 𝐴 ‘ ( 𝐷 ∗ 𝐶 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | asclelbasALT.a | ⊢ 𝐴 = ( algSc ‘ 𝑊 ) | |
| 2 | asclelbasALT.f | ⊢ 𝐹 = ( Scalar ‘ 𝑊 ) | |
| 3 | asclelbasALT.b | ⊢ 𝐵 = ( Base ‘ 𝐹 ) | |
| 4 | asclelbasALT.w | ⊢ ( 𝜑 → 𝑊 ∈ AssAlg ) | |
| 5 | asclelbasALT.c | ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 ) | |
| 6 | asclcom.m | ⊢ ∗ = ( .r ‘ 𝐹 ) | |
| 7 | asclcom.d | ⊢ ( 𝜑 → 𝐷 ∈ 𝐵 ) | |
| 8 | 1 2 3 4 7 | asclelbas | ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐷 ) ∈ ( Base ‘ 𝑊 ) ) |
| 9 | eqid | ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 ) | |
| 10 | eqid | ⊢ ( .r ‘ 𝑊 ) = ( .r ‘ 𝑊 ) | |
| 11 | eqid | ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 ) | |
| 12 | 1 2 3 9 10 11 | asclmul1 | ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝐶 ∈ 𝐵 ∧ ( 𝐴 ‘ 𝐷 ) ∈ ( Base ‘ 𝑊 ) ) → ( ( 𝐴 ‘ 𝐶 ) ( .r ‘ 𝑊 ) ( 𝐴 ‘ 𝐷 ) ) = ( 𝐶 ( ·𝑠 ‘ 𝑊 ) ( 𝐴 ‘ 𝐷 ) ) ) |
| 13 | 1 2 3 9 10 11 | asclmul2 | ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝐶 ∈ 𝐵 ∧ ( 𝐴 ‘ 𝐷 ) ∈ ( Base ‘ 𝑊 ) ) → ( ( 𝐴 ‘ 𝐷 ) ( .r ‘ 𝑊 ) ( 𝐴 ‘ 𝐶 ) ) = ( 𝐶 ( ·𝑠 ‘ 𝑊 ) ( 𝐴 ‘ 𝐷 ) ) ) |
| 14 | 12 13 | eqtr4d | ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝐶 ∈ 𝐵 ∧ ( 𝐴 ‘ 𝐷 ) ∈ ( Base ‘ 𝑊 ) ) → ( ( 𝐴 ‘ 𝐶 ) ( .r ‘ 𝑊 ) ( 𝐴 ‘ 𝐷 ) ) = ( ( 𝐴 ‘ 𝐷 ) ( .r ‘ 𝑊 ) ( 𝐴 ‘ 𝐶 ) ) ) |
| 15 | 4 5 8 14 | syl3anc | ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝐶 ) ( .r ‘ 𝑊 ) ( 𝐴 ‘ 𝐷 ) ) = ( ( 𝐴 ‘ 𝐷 ) ( .r ‘ 𝑊 ) ( 𝐴 ‘ 𝐶 ) ) ) |
| 16 | 1 2 3 10 6 | ascldimul | ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) → ( 𝐴 ‘ ( 𝐶 ∗ 𝐷 ) ) = ( ( 𝐴 ‘ 𝐶 ) ( .r ‘ 𝑊 ) ( 𝐴 ‘ 𝐷 ) ) ) |
| 17 | 4 5 7 16 | syl3anc | ⊢ ( 𝜑 → ( 𝐴 ‘ ( 𝐶 ∗ 𝐷 ) ) = ( ( 𝐴 ‘ 𝐶 ) ( .r ‘ 𝑊 ) ( 𝐴 ‘ 𝐷 ) ) ) |
| 18 | 1 2 3 10 6 | ascldimul | ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝐷 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) → ( 𝐴 ‘ ( 𝐷 ∗ 𝐶 ) ) = ( ( 𝐴 ‘ 𝐷 ) ( .r ‘ 𝑊 ) ( 𝐴 ‘ 𝐶 ) ) ) |
| 19 | 4 7 5 18 | syl3anc | ⊢ ( 𝜑 → ( 𝐴 ‘ ( 𝐷 ∗ 𝐶 ) ) = ( ( 𝐴 ‘ 𝐷 ) ( .r ‘ 𝑊 ) ( 𝐴 ‘ 𝐶 ) ) ) |
| 20 | 15 17 19 | 3eqtr4d | ⊢ ( 𝜑 → ( 𝐴 ‘ ( 𝐶 ∗ 𝐷 ) ) = ( 𝐴 ‘ ( 𝐷 ∗ 𝐶 ) ) ) |