This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ascl0

Description: The scalar 0 embedded into a left module corresponds to the 0 of the left module if the left module is also a ring. (Contributed by AV, 31-Jul-2019)

Ref Expression
Hypotheses ascl0.a ⊢ A = algSc ⁡ W
ascl0.f ⊢ F = Scalar ⁡ W
ascl0.l ⊢ φ → W ∈ LMod
ascl0.r ⊢ φ → W ∈ Ring
Assertion ascl0 ⊢ φ → A ⁡ 0 F = 0 W

Proof

Step Hyp Ref Expression
1 ascl0.a ⊢ A = algSc ⁡ W
2 ascl0.f ⊢ F = Scalar ⁡ W
3 ascl0.l ⊢ φ → W ∈ LMod
4 ascl0.r ⊢ φ → W ∈ Ring
5 2 lmodfgrp ⊢ W ∈ LMod → F ∈ Grp
6 eqid ⊢ Base F = Base F
7 eqid ⊢ 0 F = 0 F
8 6 7 grpidcl ⊢ F ∈ Grp → 0 F ∈ Base F
9 eqid ⊢ ⋅ W = ⋅ W
10 eqid ⊢ 1 W = 1 W
11 1 2 6 9 10 asclval ⊢ 0 F ∈ Base F → A ⁡ 0 F = 0 F ⋅ W 1 W
12 3 5 8 11 4syl ⊢ φ → A ⁡ 0 F = 0 F ⋅ W 1 W
13 eqid ⊢ Base W = Base W
14 13 10 ringidcl ⊢ W ∈ Ring → 1 W ∈ Base W
15 4 14 syl ⊢ φ → 1 W ∈ Base W
16 eqid ⊢ 0 W = 0 W
17 13 2 9 7 16 lmod0vs ⊢ W ∈ LMod ∧ 1 W ∈ Base W → 0 F ⋅ W 1 W = 0 W
18 3 15 17 syl2anc ⊢ φ → 0 F ⋅ W 1 W = 0 W
19 12 18 eqtrd ⊢ φ → A ⁡ 0 F = 0 W