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 = 1 st R
isdivrng1.2 H = 2 nd R
isdivrng1.3 Z = GId G
isdivrng1.4 X = ran G
Assertion divrngcl R DivRingOps A X Z B X Z A H B X Z

Proof

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