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 ) )
7 6 adantl
 |-  ( ( ( 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 } ) ) ) ) )
11 10 adantl
 |-  ( ( 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 } ) ) ) )
13 12 adantl
 |-  ( ( 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 } ) ) )
22 21 adantr
 |-  ( ( 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 } ) )