Metamath Proof Explorer

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 โŠข ๐ต = ( Base โ€˜ ๐‘… )
drngmcl.t โŠข ยท = ( .r โ€˜ ๐‘… )
drngmcl.z โŠข 0 = ( 0g โ€˜ ๐‘… )
Assertion drngmcl ( ( ๐‘… โˆˆ DivRing โˆง ๐‘‹ โˆˆ ( ๐ต โˆ– { 0 } ) โˆง ๐‘Œ โˆˆ ( ๐ต โˆ– { 0 } ) ) โ†’ ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ( ๐ต โˆ– { 0 } ) )

Proof

Step Hyp Ref Expression
1 drngmcl.b โŠข ๐ต = ( Base โ€˜ ๐‘… )
2 drngmcl.t โŠข ยท = ( .r โ€˜ ๐‘… )
3 drngmcl.z โŠข 0 = ( 0g โ€˜ ๐‘… )
4 eqid โŠข ( ( mulGrp โ€˜ ๐‘… ) โ†พs ( ๐ต โˆ– { 0 } ) ) = ( ( mulGrp โ€˜ ๐‘… ) โ†พs ( ๐ต โˆ– { 0 } ) )
5 1 3 4 drngmgp โŠข ( ๐‘… โˆˆ DivRing โ†’ ( ( mulGrp โ€˜ ๐‘… ) โ†พs ( ๐ต โˆ– { 0 } ) ) โˆˆ Grp )
6 difss โŠข ( ๐ต โˆ– { 0 } ) โŠ† ๐ต
7 eqid โŠข ( mulGrp โ€˜ ๐‘… ) = ( mulGrp โ€˜ ๐‘… )
8 7 1 mgpbas โŠข ๐ต = ( Base โ€˜ ( mulGrp โ€˜ ๐‘… ) )
9 4 8 ressbas2 โŠข ( ( ๐ต โˆ– { 0 } ) โŠ† ๐ต โ†’ ( ๐ต โˆ– { 0 } ) = ( Base โ€˜ ( ( mulGrp โ€˜ ๐‘… ) โ†พs ( ๐ต โˆ– { 0 } ) ) ) )
10 6 9 ax-mp โŠข ( ๐ต โˆ– { 0 } ) = ( Base โ€˜ ( ( mulGrp โ€˜ ๐‘… ) โ†พs ( ๐ต โˆ– { 0 } ) ) )
11 1 fvexi โŠข ๐ต โˆˆ V
12 difexg โŠข ( ๐ต โˆˆ V โ†’ ( ๐ต โˆ– { 0 } ) โˆˆ V )
13 7 2 mgpplusg โŠข ยท = ( +g โ€˜ ( mulGrp โ€˜ ๐‘… ) )
14 4 13 ressplusg โŠข ( ( ๐ต โˆ– { 0 } ) โˆˆ V โ†’ ยท = ( +g โ€˜ ( ( mulGrp โ€˜ ๐‘… ) โ†พs ( ๐ต โˆ– { 0 } ) ) ) )
15 11 12 14 mp2b โŠข ยท = ( +g โ€˜ ( ( mulGrp โ€˜ ๐‘… ) โ†พs ( ๐ต โˆ– { 0 } ) ) )
16 10 15 grpcl โŠข ( ( ( ( mulGrp โ€˜ ๐‘… ) โ†พs ( ๐ต โˆ– { 0 } ) ) โˆˆ Grp โˆง ๐‘‹ โˆˆ ( ๐ต โˆ– { 0 } ) โˆง ๐‘Œ โˆˆ ( ๐ต โˆ– { 0 } ) ) โ†’ ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ( ๐ต โˆ– { 0 } ) )
17 5 16 syl3an1 โŠข ( ( ๐‘… โˆˆ DivRing โˆง ๐‘‹ โˆˆ ( ๐ต โˆ– { 0 } ) โˆง ๐‘Œ โˆˆ ( ๐ต โˆ– { 0 } ) ) โ†’ ( ๐‘‹ ยท ๐‘Œ ) โˆˆ ( ๐ต โˆ– { 0 } ) )