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 eqtrdi ⊢ ( ( 𝑅 ∈ 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 ∧ 𝐴 ∈ ( 𝑋 ∖ { 𝑍 } ) ∧ 𝐵 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( 𝐴 𝐻 𝐵 ) ∈ ( 𝑋 ∖ { 𝑍 } ) )