Description: Two ways of saying the scalar injection is one-to-one. (Contributed by SN, 3-Jul-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | asclf1.a | ⊢ 𝐴 = ( algSc ‘ 𝑊 ) | |
| asclf1.b | ⊢ 𝐵 = ( Base ‘ 𝑊 ) | ||
| asclf1.s | ⊢ 𝑆 = ( Scalar ‘ 𝑊 ) | ||
| asclf1.k | ⊢ 𝐾 = ( Base ‘ 𝑆 ) | ||
| asclf1.0 | ⊢ 0 = ( 0g ‘ 𝑊 ) | ||
| asclf1.n | ⊢ 𝑁 = ( 0g ‘ 𝑆 ) | ||
| asclf1.r | ⊢ ( 𝜑 → 𝑊 ∈ Ring ) | ||
| asclf1.m | ⊢ ( 𝜑 → 𝑊 ∈ LMod ) | ||
| Assertion | asclf1 | ⊢ ( 𝜑 → ( 𝐴 : 𝐾 –1-1→ 𝐵 ↔ ∀ 𝑠 ∈ 𝐾 ( ( 𝐴 ‘ 𝑠 ) = 0 → 𝑠 = 𝑁 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | asclf1.a | ⊢ 𝐴 = ( algSc ‘ 𝑊 ) | |
| 2 | asclf1.b | ⊢ 𝐵 = ( Base ‘ 𝑊 ) | |
| 3 | asclf1.s | ⊢ 𝑆 = ( Scalar ‘ 𝑊 ) | |
| 4 | asclf1.k | ⊢ 𝐾 = ( Base ‘ 𝑆 ) | |
| 5 | asclf1.0 | ⊢ 0 = ( 0g ‘ 𝑊 ) | |
| 6 | asclf1.n | ⊢ 𝑁 = ( 0g ‘ 𝑆 ) | |
| 7 | asclf1.r | ⊢ ( 𝜑 → 𝑊 ∈ Ring ) | |
| 8 | asclf1.m | ⊢ ( 𝜑 → 𝑊 ∈ LMod ) | |
| 9 | 1 3 7 8 | asclghm | ⊢ ( 𝜑 → 𝐴 ∈ ( 𝑆 GrpHom 𝑊 ) ) |
| 10 | 4 2 6 5 | ghmf1 | ⊢ ( 𝐴 ∈ ( 𝑆 GrpHom 𝑊 ) → ( 𝐴 : 𝐾 –1-1→ 𝐵 ↔ ∀ 𝑠 ∈ 𝐾 ( ( 𝐴 ‘ 𝑠 ) = 0 → 𝑠 = 𝑁 ) ) ) |
| 11 | 9 10 | syl | ⊢ ( 𝜑 → ( 𝐴 : 𝐾 –1-1→ 𝐵 ↔ ∀ 𝑠 ∈ 𝐾 ( ( 𝐴 ‘ 𝑠 ) = 0 → 𝑠 = 𝑁 ) ) ) |