Description: The additive neutral element of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023)
Ref | Expression | ||
---|---|---|---|
Hypotheses | drgext.b | ⊢ 𝐵 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑈 ) | |
drgext.1 | ⊢ ( 𝜑 → 𝐸 ∈ DivRing ) | ||
drgext.2 | ⊢ ( 𝜑 → 𝑈 ∈ ( SubRing ‘ 𝐸 ) ) | ||
Assertion | drgext0g | ⊢ ( 𝜑 → ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐵 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | drgext.b | ⊢ 𝐵 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑈 ) | |
2 | drgext.1 | ⊢ ( 𝜑 → 𝐸 ∈ DivRing ) | |
3 | drgext.2 | ⊢ ( 𝜑 → 𝑈 ∈ ( SubRing ‘ 𝐸 ) ) | |
4 | 1 | a1i | ⊢ ( 𝜑 → 𝐵 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑈 ) ) |
5 | eqidd | ⊢ ( 𝜑 → ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐸 ) ) | |
6 | eqid | ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 ) | |
7 | 6 | subrgss | ⊢ ( 𝑈 ∈ ( SubRing ‘ 𝐸 ) → 𝑈 ⊆ ( Base ‘ 𝐸 ) ) |
8 | 3 7 | syl | ⊢ ( 𝜑 → 𝑈 ⊆ ( Base ‘ 𝐸 ) ) |
9 | 4 5 8 | sralmod0 | ⊢ ( 𝜑 → ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐵 ) ) |