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 𝐺 = ( 1st𝑅 )
isdivrng1.2 𝐻 = ( 2nd𝑅 )
isdivrng1.3 𝑍 = ( GId ‘ 𝐺 )
isdivrng1.4 𝑋 = ran 𝐺
Assertion divrngcl ( ( 𝑅 ∈ DivRingOps ∧ 𝐴 ∈ ( 𝑋 ∖ { 𝑍 } ) ∧ 𝐵 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( 𝐴 𝐻 𝐵 ) ∈ ( 𝑋 ∖ { 𝑍 } ) )

Proof

Step Hyp Ref Expression
1 isdivrng1.1 𝐺 = ( 1st𝑅 )
2 isdivrng1.2 𝐻 = ( 2nd𝑅 )
3 isdivrng1.3 𝑍 = ( GId ‘ 𝐺 )
4 isdivrng1.4 𝑋 = ran 𝐺
5 1 2 3 4 isdrngo1 ( 𝑅 ∈ DivRingOps ↔ ( 𝑅 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) )
6 ovres ( ( 𝐴 ∈ ( 𝑋 ∖ { 𝑍 } ) ∧ 𝐵 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( 𝐴 ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) 𝐵 ) = ( 𝐴 𝐻 𝐵 ) )
7 6 adantl ( ( ( 𝑅 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) ∧ ( 𝐴 ∈ ( 𝑋 ∖ { 𝑍 } ) ∧ 𝐵 ∈ ( 𝑋 ∖ { 𝑍 } ) ) ) → ( 𝐴 ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) 𝐵 ) = ( 𝐴 𝐻 𝐵 ) )
8 eqid ran ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) = ran ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) )
9 8 grpocl ( ( ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ∧ 𝐴 ∈ ran ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∧ 𝐵 ∈ ran ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ) → ( 𝐴 ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) 𝐵 ) ∈ ran ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) )
10 9 3expib ( ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp → ( ( 𝐴 ∈ ran ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∧ 𝐵 ∈ ran ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ) → ( 𝐴 ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) 𝐵 ) ∈ ran ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ) )
11 10 adantl ( ( 𝑅 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) → ( ( 𝐴 ∈ ran ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∧ 𝐵 ∈ ran ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ) → ( 𝐴 ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) 𝐵 ) ∈ ran ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ) )
12 grporndm ( ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp → ran ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) = dom dom ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) )
13 12 adantl ( ( 𝑅 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) → ran ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) = dom dom ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) )
14 difss ( 𝑋 ∖ { 𝑍 } ) ⊆ 𝑋
15 xpss12 ( ( ( 𝑋 ∖ { 𝑍 } ) ⊆ 𝑋 ∧ ( 𝑋 ∖ { 𝑍 } ) ⊆ 𝑋 ) → ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ⊆ ( 𝑋 × 𝑋 ) )
16 14 14 15 mp2an ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ⊆ ( 𝑋 × 𝑋 )
17 1 2 4 rngosm ( 𝑅 ∈ RingOps → 𝐻 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
18 17 fdmd ( 𝑅 ∈ RingOps → dom 𝐻 = ( 𝑋 × 𝑋 ) )
19 16 18 sseqtrrid ( 𝑅 ∈ RingOps → ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ⊆ dom 𝐻 )
20 ssdmres ( ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ⊆ dom 𝐻 ↔ dom ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) = ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) )
21 19 20 sylib ( 𝑅 ∈ RingOps → dom ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) = ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) )
22 21 adantr ( ( 𝑅 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) → dom ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) = ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) )
23 22 dmeqd ( ( 𝑅 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) → dom dom ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) = dom ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) )
24 dmxpid dom ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) = ( 𝑋 ∖ { 𝑍 } )
25 23 24 syl6eq ( ( 𝑅 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) → dom dom ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) = ( 𝑋 ∖ { 𝑍 } ) )
26 13 25 eqtrd ( ( 𝑅 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) → ran ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) = ( 𝑋 ∖ { 𝑍 } ) )
27 26 eleq2d ( ( 𝑅 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) → ( 𝐴 ∈ ran ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ↔ 𝐴 ∈ ( 𝑋 ∖ { 𝑍 } ) ) )
28 26 eleq2d ( ( 𝑅 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) → ( 𝐵 ∈ ran ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ↔ 𝐵 ∈ ( 𝑋 ∖ { 𝑍 } ) ) )
29 27 28 anbi12d ( ( 𝑅 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) → ( ( 𝐴 ∈ ran ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∧ 𝐵 ∈ ran ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ) ↔ ( 𝐴 ∈ ( 𝑋 ∖ { 𝑍 } ) ∧ 𝐵 ∈ ( 𝑋 ∖ { 𝑍 } ) ) ) )
30 26 eleq2d ( ( 𝑅 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) → ( ( 𝐴 ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) 𝐵 ) ∈ ran ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ↔ ( 𝐴 ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) 𝐵 ) ∈ ( 𝑋 ∖ { 𝑍 } ) ) )
31 11 29 30 3imtr3d ( ( 𝑅 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) → ( ( 𝐴 ∈ ( 𝑋 ∖ { 𝑍 } ) ∧ 𝐵 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( 𝐴 ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) 𝐵 ) ∈ ( 𝑋 ∖ { 𝑍 } ) ) )
32 31 imp ( ( ( 𝑅 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) ∧ ( 𝐴 ∈ ( 𝑋 ∖ { 𝑍 } ) ∧ 𝐵 ∈ ( 𝑋 ∖ { 𝑍 } ) ) ) → ( 𝐴 ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) 𝐵 ) ∈ ( 𝑋 ∖ { 𝑍 } ) )
33 7 32 eqeltrrd ( ( ( 𝑅 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) ∧ ( 𝐴 ∈ ( 𝑋 ∖ { 𝑍 } ) ∧ 𝐵 ∈ ( 𝑋 ∖ { 𝑍 } ) ) ) → ( 𝐴 𝐻 𝐵 ) ∈ ( 𝑋 ∖ { 𝑍 } ) )
34 33 3impb ( ( ( 𝑅 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) ∧ 𝐴 ∈ ( 𝑋 ∖ { 𝑍 } ) ∧ 𝐵 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( 𝐴 𝐻 𝐵 ) ∈ ( 𝑋 ∖ { 𝑍 } ) )
35 5 34 syl3an1b ( ( 𝑅 ∈ DivRingOps ∧ 𝐴 ∈ ( 𝑋 ∖ { 𝑍 } ) ∧ 𝐵 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( 𝐴 𝐻 𝐵 ) ∈ ( 𝑋 ∖ { 𝑍 } ) )