# Metamath Proof Explorer

## Theorem divrngcl

Description: The product of two nonzero elements of a division ring is nonzero. (Contributed by Jeff Madsen, 9-Jun-2010)

Ref Expression
Hypotheses isdivrng1.1
`|- G = ( 1st ` R )`
isdivrng1.2
`|- H = ( 2nd ` R )`
isdivrng1.3
`|- Z = ( GId ` G )`
isdivrng1.4
`|- X = ran G`
Assertion divrngcl
`|- ( ( R e. DivRingOps /\ A e. ( X \ { Z } ) /\ B e. ( X \ { Z } ) ) -> ( A H B ) e. ( X \ { Z } ) )`

### Proof

Step Hyp Ref Expression
1 isdivrng1.1
` |-  G = ( 1st ` R )`
2 isdivrng1.2
` |-  H = ( 2nd ` R )`
3 isdivrng1.3
` |-  Z = ( GId ` G )`
4 isdivrng1.4
` |-  X = ran G`
5 1 2 3 4 isdrngo1
` |-  ( R e. DivRingOps <-> ( R e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) )`
6 ovres
` |-  ( ( A e. ( X \ { Z } ) /\ B e. ( X \ { Z } ) ) -> ( A ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) B ) = ( A H B ) )`
` |-  ( ( ( R e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) /\ ( A e. ( X \ { Z } ) /\ B e. ( X \ { Z } ) ) ) -> ( A ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) B ) = ( A H B ) )`
8 eqid
` |-  ran ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) = ran ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) )`
9 8 grpocl
` |-  ( ( ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp /\ A e. ran ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) /\ B e. ran ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) ) -> ( A ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) B ) e. ran ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) )`
10 9 3expib
` |-  ( ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp -> ( ( A e. ran ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) /\ B e. ran ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) ) -> ( A ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) B ) e. ran ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) ) )`
` |-  ( ( R e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) -> ( ( A e. ran ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) /\ B e. ran ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) ) -> ( A ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) B ) e. ran ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) ) )`
12 grporndm
` |-  ( ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp -> ran ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) = dom dom ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) )`
` |-  ( ( R e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) -> ran ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) = dom dom ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) )`
14 difss
` |-  ( X \ { Z } ) C_ X`
15 xpss12
` |-  ( ( ( X \ { Z } ) C_ X /\ ( X \ { Z } ) C_ X ) -> ( ( X \ { Z } ) X. ( X \ { Z } ) ) C_ ( X X. X ) )`
16 14 14 15 mp2an
` |-  ( ( X \ { Z } ) X. ( X \ { Z } ) ) C_ ( X X. X )`
17 1 2 4 rngosm
` |-  ( R e. RingOps -> H : ( X X. X ) --> X )`
18 17 fdmd
` |-  ( R e. RingOps -> dom H = ( X X. X ) )`
19 16 18 sseqtrrid
` |-  ( R e. RingOps -> ( ( X \ { Z } ) X. ( X \ { Z } ) ) C_ dom H )`
20 ssdmres
` |-  ( ( ( X \ { Z } ) X. ( X \ { Z } ) ) C_ dom H <-> dom ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) = ( ( X \ { Z } ) X. ( X \ { Z } ) ) )`
21 19 20 sylib
` |-  ( R e. RingOps -> dom ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) = ( ( X \ { Z } ) X. ( X \ { Z } ) ) )`
` |-  ( ( R e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) -> dom ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) = ( ( X \ { Z } ) X. ( X \ { Z } ) ) )`
23 22 dmeqd
` |-  ( ( R e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) -> dom dom ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) = dom ( ( X \ { Z } ) X. ( X \ { Z } ) ) )`
24 dmxpid
` |-  dom ( ( X \ { Z } ) X. ( X \ { Z } ) ) = ( X \ { Z } )`
25 23 24 syl6eq
` |-  ( ( R e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) -> dom dom ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) = ( X \ { Z } ) )`
26 13 25 eqtrd
` |-  ( ( R e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) -> ran ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) = ( X \ { Z } ) )`
27 26 eleq2d
` |-  ( ( R e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) -> ( A e. ran ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) <-> A e. ( X \ { Z } ) ) )`
28 26 eleq2d
` |-  ( ( R e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) -> ( B e. ran ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) <-> B e. ( X \ { Z } ) ) )`
29 27 28 anbi12d
` |-  ( ( R e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) -> ( ( A e. ran ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) /\ B e. ran ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) ) <-> ( A e. ( X \ { Z } ) /\ B e. ( X \ { Z } ) ) ) )`
30 26 eleq2d
` |-  ( ( R e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) -> ( ( A ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) B ) e. ran ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) <-> ( A ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) B ) e. ( X \ { Z } ) ) )`
31 11 29 30 3imtr3d
` |-  ( ( R e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) -> ( ( A e. ( X \ { Z } ) /\ B e. ( X \ { Z } ) ) -> ( A ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) B ) e. ( X \ { Z } ) ) )`
32 31 imp
` |-  ( ( ( R e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) /\ ( A e. ( X \ { Z } ) /\ B e. ( X \ { Z } ) ) ) -> ( A ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) B ) e. ( X \ { Z } ) )`
33 7 32 eqeltrrd
` |-  ( ( ( R e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) /\ ( A e. ( X \ { Z } ) /\ B e. ( X \ { Z } ) ) ) -> ( A H B ) e. ( X \ { Z } ) )`
34 33 3impb
` |-  ( ( ( R e. RingOps /\ ( H |` ( ( X \ { Z } ) X. ( X \ { Z } ) ) ) e. GrpOp ) /\ A e. ( X \ { Z } ) /\ B e. ( X \ { Z } ) ) -> ( A H B ) e. ( X \ { Z } ) )`
35 5 34 syl3an1b
` |-  ( ( R e. DivRingOps /\ A e. ( X \ { Z } ) /\ B e. ( X \ { Z } ) ) -> ( A H B ) e. ( X \ { Z } ) )`