Metamath Proof Explorer

Theorem isdrngo3

Description: A division ring is a ring in which 1 =/= 0 and every nonzero element is invertible. (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypotheses isdivrng1.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
isdivrng1.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
isdivrng1.3 ⊢ 𝑍 = ( GId ‘ 𝐺 )
isdivrng1.4 ⊢ 𝑋 = ran 𝐺
isdivrng2.5 ⊢ 𝑈 = ( GId ‘ 𝐻 )
Assertion isdrngo3 ( 𝑅 ∈ DivRingOps ↔ ( 𝑅 ∈ RingOps ∧ ( 𝑈 ≠ 𝑍 ∧ ∀ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐻 𝑥 ) = 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 isdivrng1.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 isdivrng1.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3 isdivrng1.3 ⊢ 𝑍 = ( GId ‘ 𝐺 )
4 isdivrng1.4 ⊢ 𝑋 = ran 𝐺
5 isdivrng2.5 ⊢ 𝑈 = ( GId ‘ 𝐻 )
6 1 2 3 4 5 isdrngo2 ⊢ ( 𝑅 ∈ DivRingOps ↔ ( 𝑅 ∈ RingOps ∧ ( 𝑈 ≠ 𝑍 ∧ ∀ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑥 ) = 𝑈 ) ) )
7 eldifi ⊢ ( 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) → 𝑥 ∈ 𝑋 )
8 difss ⊢ ( 𝑋 ∖ { 𝑍 } ) ⊆ 𝑋
9 ssrexv ⊢ ( ( 𝑋 ∖ { 𝑍 } ) ⊆ 𝑋 → ( ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑥 ) = 𝑈 → ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐻 𝑥 ) = 𝑈 ) )
10 8 9 ax-mp ⊢ ( ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑥 ) = 𝑈 → ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐻 𝑥 ) = 𝑈 )
11 neeq1 ⊢ ( ( 𝑦 𝐻 𝑥 ) = 𝑈 → ( ( 𝑦 𝐻 𝑥 ) ≠ 𝑍 ↔ 𝑈 ≠ 𝑍 ) )
12 11 biimparc ⊢ ( ( 𝑈 ≠ 𝑍 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑈 ) → ( 𝑦 𝐻 𝑥 ) ≠ 𝑍 )
13 3 4 1 2 rngolz ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑋 ) → ( 𝑍 𝐻 𝑥 ) = 𝑍 )
14 oveq1 ⊢ ( 𝑦 = 𝑍 → ( 𝑦 𝐻 𝑥 ) = ( 𝑍 𝐻 𝑥 ) )
15 14 eqeq1d ⊢ ( 𝑦 = 𝑍 → ( ( 𝑦 𝐻 𝑥 ) = 𝑍 ↔ ( 𝑍 𝐻 𝑥 ) = 𝑍 ) )
16 13 15 syl5ibrcom ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑋 ) → ( 𝑦 = 𝑍 → ( 𝑦 𝐻 𝑥 ) = 𝑍 ) )
17 16 necon3d ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑦 𝐻 𝑥 ) ≠ 𝑍 → 𝑦 ≠ 𝑍 ) )
18 17 imp ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 𝐻 𝑥 ) ≠ 𝑍 ) → 𝑦 ≠ 𝑍 )
19 12 18 sylan2 ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑈 ≠ 𝑍 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑈 ) ) → 𝑦 ≠ 𝑍 )
20 19 an4s ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑈 ) ) → 𝑦 ≠ 𝑍 )
21 20 anassrs ⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 𝐻 𝑥 ) = 𝑈 ) → 𝑦 ≠ 𝑍 )
22 pm3.2 ⊢ ( 𝑦 ∈ 𝑋 → ( 𝑦 ≠ 𝑍 → ( 𝑦 ∈ 𝑋 ∧ 𝑦 ≠ 𝑍 ) ) )
23 21 22 syl5com ⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 𝐻 𝑥 ) = 𝑈 ) → ( 𝑦 ∈ 𝑋 → ( 𝑦 ∈ 𝑋 ∧ 𝑦 ≠ 𝑍 ) ) )
24 eldifsn ⊢ ( 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ↔ ( 𝑦 ∈ 𝑋 ∧ 𝑦 ≠ 𝑍 ) )
25 23 24 imbitrrdi ⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 𝐻 𝑥 ) = 𝑈 ) → ( 𝑦 ∈ 𝑋 → 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ) )
26 25 imdistanda ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑦 𝐻 𝑥 ) = 𝑈 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑦 𝐻 𝑥 ) = 𝑈 ∧ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ) ) )
27 ancom ⊢ ( ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑈 ) ↔ ( ( 𝑦 𝐻 𝑥 ) = 𝑈 ∧ 𝑦 ∈ 𝑋 ) )
28 ancom ⊢ ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ∧ ( 𝑦 𝐻 𝑥 ) = 𝑈 ) ↔ ( ( 𝑦 𝐻 𝑥 ) = 𝑈 ∧ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ) )
29 26 27 28 3imtr4g ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑈 ) → ( 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ∧ ( 𝑦 𝐻 𝑥 ) = 𝑈 ) ) )
30 29 reximdv2 ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ) ∧ 𝑥 ∈ 𝑋 ) → ( ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐻 𝑥 ) = 𝑈 → ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑥 ) = 𝑈 ) )
31 10 30 impbid2 ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ) ∧ 𝑥 ∈ 𝑋 ) → ( ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑥 ) = 𝑈 ↔ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐻 𝑥 ) = 𝑈 ) )
32 7 31 sylan2 ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ) ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑥 ) = 𝑈 ↔ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐻 𝑥 ) = 𝑈 ) )
33 32 ralbidva ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ) → ( ∀ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑥 ) = 𝑈 ↔ ∀ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐻 𝑥 ) = 𝑈 ) )
34 33 pm5.32da ⊢ ( 𝑅 ∈ RingOps → ( ( 𝑈 ≠ 𝑍 ∧ ∀ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑥 ) = 𝑈 ) ↔ ( 𝑈 ≠ 𝑍 ∧ ∀ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐻 𝑥 ) = 𝑈 ) ) )
35 34 pm5.32i ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝑈 ≠ 𝑍 ∧ ∀ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑥 ) = 𝑈 ) ) ↔ ( 𝑅 ∈ RingOps ∧ ( 𝑈 ≠ 𝑍 ∧ ∀ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐻 𝑥 ) = 𝑈 ) ) )
36 6 35 bitri ⊢ ( 𝑅 ∈ DivRingOps ↔ ( 𝑅 ∈ RingOps ∧ ( 𝑈 ≠ 𝑍 ∧ ∀ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐻 𝑥 ) = 𝑈 ) ) )