Theorem drngmcl

Description: The product of two nonzero elements of a division ring is nonzero. (Contributed by NM, 7-Sep-2011)

	Ref	Expression
Hypotheses	drngmcl.b	$$⊢B={\mathrm{Base}}_R$$
	drngmcl.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	drngmcl.z	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	drngmcl	$$⊢\left(R\in \mathrm{DivRing}\wedge X\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge Y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to X\underset{\dot{}}{·}Y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		drngmcl.b	$$⊢B={\mathrm{Base}}_R$$
2		drngmcl.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		drngmcl.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		eqid	$$⊢{\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)={\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
5	1 3 4	drngmgp	$$⊢R\in \mathrm{DivRing}\to {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\in \mathrm{Grp}$$
6		difss	$$⊢B\setminus \left\{\underset{\dot{}}{0}\right\}\subseteq B$$
7		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
8	7 1	mgpbas	$$⊢B={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
9	4 8	ressbas2	$$⊢B\setminus \left\{\underset{\dot{}}{0}\right\}\subseteq B\to B\setminus \left\{\underset{\dot{}}{0}\right\}={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}$$
10	6 9	ax-mp	$$⊢B\setminus \left\{\underset{\dot{}}{0}\right\}={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}$$
11	1	fvexi	$$⊢B\in \mathrm{V}$$
12		difexg	$$⊢B\in \mathrm{V}\to B\setminus \left\{\underset{\dot{}}{0}\right\}\in \mathrm{V}$$
13	7 2	mgpplusg	$$⊢\underset{\dot{}}{·}={+}_{{\mathrm{mulGrp}}_R}$$
14	4 13	ressplusg	$$⊢B\setminus \left\{\underset{\dot{}}{0}\right\}\in \mathrm{V}\to \underset{\dot{}}{·}={+}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}$$
15	11 12 14	mp2b	$$⊢\underset{\dot{}}{·}={+}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}$$
16	10 15	grpcl	$$⊢\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\in \mathrm{Grp}\wedge X\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge Y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to X\underset{\dot{}}{·}Y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
17	5 16	syl3an1	$$⊢\left(R\in \mathrm{DivRing}\wedge X\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge Y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to X\underset{\dot{}}{·}Y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$