Description: The zero element of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014)
Ref | Expression | ||
---|---|---|---|
Hypothesis | qrng.q | ⊢ 𝑄 = ( ℂfld ↾s ℚ ) | |
Assertion | qrng0 | ⊢ 0 = ( 0g ‘ 𝑄 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | qrng.q | ⊢ 𝑄 = ( ℂfld ↾s ℚ ) | |
2 | qsubdrg | ⊢ ( ℚ ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s ℚ ) ∈ DivRing ) | |
3 | 2 | simpli | ⊢ ℚ ∈ ( SubRing ‘ ℂfld ) |
4 | subrgsubg | ⊢ ( ℚ ∈ ( SubRing ‘ ℂfld ) → ℚ ∈ ( SubGrp ‘ ℂfld ) ) | |
5 | cnfld0 | ⊢ 0 = ( 0g ‘ ℂfld ) | |
6 | 1 5 | subg0 | ⊢ ( ℚ ∈ ( SubGrp ‘ ℂfld ) → 0 = ( 0g ‘ 𝑄 ) ) |
7 | 3 4 6 | mp2b | ⊢ 0 = ( 0g ‘ 𝑄 ) |