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 = ( Base ` R )
	drngmcl.t	|- .x. = ( .r ` R )
	drngmcl.z	|- .0. = ( 0g ` R )
Assertion	drngmcl	|- ( ( R e. DivRing /\ X e. ( B \ { .0. } ) /\ Y e. ( B \ { .0. } ) ) -> ( X .x. Y ) e. ( B \ { .0. } ) )

Proof

Step	Hyp	Ref	Expression
1		drngmcl.b	|- B = ( Base ` R )
2		drngmcl.t	|- .x. = ( .r ` R )
3		drngmcl.z	|- .0. = ( 0g ` R )
4		eqid	|- ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) = ( ( mulGrp ` R ) |`s ( B \ { .0. } ) )
5	1 3 4	drngmgp	|- ( R e. DivRing -> ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp )
6		difss	|- ( B \ { .0. } ) C_ B
7		eqid	|- ( mulGrp ` R ) = ( mulGrp ` R )
8	7 1	mgpbas	|- B = ( Base ` ( mulGrp ` R ) )
9	4 8	ressbas2	|- ( ( B \ { .0. } ) C_ B -> ( B \ { .0. } ) = ( Base ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) )
10	6 9	ax-mp	|- ( B \ { .0. } ) = ( Base ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) )
11	1	fvexi	|- B e. _V
12		difexg	|- ( B e. _V -> ( B \ { .0. } ) e. _V )
13	7 2	mgpplusg	|- .x. = ( +g ` ( mulGrp ` R ) )
14	4 13	ressplusg	|- ( ( B \ { .0. } ) e. _V -> .x. = ( +g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) )
15	11 12 14	mp2b	|- .x. = ( +g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) )
16	10 15	grpcl	|- ( ( ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp /\ X e. ( B \ { .0. } ) /\ Y e. ( B \ { .0. } ) ) -> ( X .x. Y ) e. ( B \ { .0. } ) )
17	5 16	syl3an1	|- ( ( R e. DivRing /\ X e. ( B \ { .0. } ) /\ Y e. ( B \ { .0. } ) ) -> ( X .x. Y ) e. ( B \ { .0. } ) )