Theorem qrng0

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

	Ref	Expression
Hypothesis	qrng.q	$$⊢Q={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
Assertion	qrng0	$$⊢0=0_Q$$

Proof

Step	Hyp	Ref	Expression
1		qrng.q	$$⊢Q={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
2		qsubdrg	$$⊢\left(\mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\in \mathrm{DivRing}\right)$$
3	2	simpli	$$⊢\mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
4		subrgsubg	$$⊢\mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to \mathbb{Q}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$$
5		cnfld0	$$⊢0=0_{{ℂ}_{\mathrm{fld}}}$$
6	1 5	subg0	$$⊢\mathbb{Q}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\to 0=0_Q$$
7	3 4 6	mp2b	$$⊢0=0_Q$$