Metamath Proof Explorer


Theorem qrng0

Description: The zero element of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014)

Ref Expression
Hypothesis qrng.q 𝑄 = ( ℂflds ℚ )
Assertion qrng0 0 = ( 0g𝑄 )

Proof

Step Hyp Ref Expression
1 qrng.q 𝑄 = ( ℂflds ℚ )
2 qsubdrg ( ℚ ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂflds ℚ ) ∈ 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𝑄 )