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 eqtrdi ⊢ 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