Theorem qrng0

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 ‘ 𝑄 )

Proof

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 ‘ 𝑄 )