This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem drngmclOLD

Description: Obsolete version of drngmcl as of 25-Jun-2025. The product of two nonzero elements of a division ring is nonzero. (Contributed by NM, 7-Sep-2011) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	drngmcl.b	$⊢ B = {Base}_{R}$
		drngmcl.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
		drngmcl.z	$⊢ \underset{˙}{0} = 0_{R}$
	Assertion	drngmclOLD	$⊢ (R \in DivRing \land X \in (B ∖ \{\underset{˙}{0}\}) \land Y \in (B ∖ \{\underset{˙}{0}\})) \to X \underset{˙}{\cdot} Y \in (B ∖ \{\underset{˙}{0}\})$

Proof

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