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 
|- .x. = ( .r ` R )
drngmcl.z 
|- .0. = ( 0g ` R )
Assertion drngmclOLD 
|- ( ( 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. } ) )