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 eqtrdi 
 |-  ( ( 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 } ) )