Metamath Proof Explorer

Theorem issubdrg

Description: Characterize the subfields of a division ring. (Contributed by Mario Carneiro, 3-Dec-2014)

Ref Expression
Hypotheses issubdrg.s ⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
issubdrg.z ⊢ 0 = ( 0g ‘ 𝑅 )
issubdrg.i ⊢ 𝐼 = ( invr ‘ 𝑅 )
Assertion issubdrg ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) → ( 𝑆 ∈ DivRing ↔ ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 issubdrg.s ⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
2 issubdrg.z ⊢ 0 = ( 0g ‘ 𝑅 )
3 issubdrg.i ⊢ 𝐼 = ( invr ‘ 𝑅 )
4 simpllr ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝑆 ∈ DivRing ) ∧ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ) → 𝐴 ∈ ( SubRing ‘ 𝑅 ) )
5 1 subrgring ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝑆 ∈ Ring )
6 4 5 syl ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝑆 ∈ DivRing ) ∧ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ) → 𝑆 ∈ Ring )
7 eldifsn ⊢ ( 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 0 ) )
8 7 bilani ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝑆 ∈ DivRing ) ∧ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 0 ) )
9 8 simpld ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝑆 ∈ DivRing ) ∧ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ) → 𝑥 ∈ 𝐴 )
10 1 subrgbas ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 = ( Base ‘ 𝑆 ) )
11 4 10 syl ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝑆 ∈ DivRing ) ∧ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ) → 𝐴 = ( Base ‘ 𝑆 ) )
12 9 11 eleqtrd ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝑆 ∈ DivRing ) ∧ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ) → 𝑥 ∈ ( Base ‘ 𝑆 ) )
13 8 simprd ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝑆 ∈ DivRing ) ∧ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ) → 𝑥 ≠ 0 )
14 1 2 subrg0 ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 0 = ( 0g ‘ 𝑆 ) )
15 4 14 syl ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝑆 ∈ DivRing ) ∧ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ) → 0 = ( 0g ‘ 𝑆 ) )
16 13 15 neeqtrd ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝑆 ∈ DivRing ) ∧ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ) → 𝑥 ≠ ( 0g ‘ 𝑆 ) )
17 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
18 eqid ⊢ ( Unit ‘ 𝑆 ) = ( Unit ‘ 𝑆 )
19 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
20 17 18 19 drngunit ⊢ ( 𝑆 ∈ DivRing → ( 𝑥 ∈ ( Unit ‘ 𝑆 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) )
21 20 ad2antlr ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝑆 ∈ DivRing ) ∧ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ) → ( 𝑥 ∈ ( Unit ‘ 𝑆 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) )
22 12 16 21 mpbir2and ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝑆 ∈ DivRing ) ∧ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ) → 𝑥 ∈ ( Unit ‘ 𝑆 ) )
23 eqid ⊢ ( invr ‘ 𝑆 ) = ( invr ‘ 𝑆 )
24 18 23 17 ringinvcl ⊢ ( ( 𝑆 ∈ Ring ∧ 𝑥 ∈ ( Unit ‘ 𝑆 ) ) → ( ( invr ‘ 𝑆 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑆 ) )
25 6 22 24 syl2anc ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝑆 ∈ DivRing ) ∧ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ) → ( ( invr ‘ 𝑆 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑆 ) )
26 1 3 18 23 subrginv ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥 ∈ ( Unit ‘ 𝑆 ) ) → ( 𝐼 ‘ 𝑥 ) = ( ( invr ‘ 𝑆 ) ‘ 𝑥 ) )
27 4 22 26 syl2anc ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝑆 ∈ DivRing ) ∧ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ) → ( 𝐼 ‘ 𝑥 ) = ( ( invr ‘ 𝑆 ) ‘ 𝑥 ) )
28 25 27 11 3eltr4d ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝑆 ∈ DivRing ) ∧ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ) → ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 )
29 28 ralrimiva ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝑆 ∈ DivRing ) → ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 )
30 5 ad2antlr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 ) → 𝑆 ∈ Ring )
31 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
32 1 31 18 subrguss ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( Unit ‘ 𝑆 ) ⊆ ( Unit ‘ 𝑅 ) )
33 32 ad2antlr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 ) → ( Unit ‘ 𝑆 ) ⊆ ( Unit ‘ 𝑅 ) )
34 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
35 34 31 2 isdrng ⊢ ( 𝑅 ∈ DivRing ↔ ( 𝑅 ∈ Ring ∧ ( Unit ‘ 𝑅 ) = ( ( Base ‘ 𝑅 ) ∖ { 0 } ) ) )
36 35 simprbi ⊢ ( 𝑅 ∈ DivRing → ( Unit ‘ 𝑅 ) = ( ( Base ‘ 𝑅 ) ∖ { 0 } ) )
37 36 ad2antrr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 ) → ( Unit ‘ 𝑅 ) = ( ( Base ‘ 𝑅 ) ∖ { 0 } ) )
38 33 37 sseqtrd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 ) → ( Unit ‘ 𝑆 ) ⊆ ( ( Base ‘ 𝑅 ) ∖ { 0 } ) )
39 17 18 unitss ⊢ ( Unit ‘ 𝑆 ) ⊆ ( Base ‘ 𝑆 )
40 10 ad2antlr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 ) → 𝐴 = ( Base ‘ 𝑆 ) )
41 39 40 sseqtrrid ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 ) → ( Unit ‘ 𝑆 ) ⊆ 𝐴 )
42 38 41 ssind ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 ) → ( Unit ‘ 𝑆 ) ⊆ ( ( ( Base ‘ 𝑅 ) ∖ { 0 } ) ∩ 𝐴 ) )
43 34 subrgss ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 ⊆ ( Base ‘ 𝑅 ) )
44 43 ad2antlr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 ) → 𝐴 ⊆ ( Base ‘ 𝑅 ) )
45 difin2 ⊢ ( 𝐴 ⊆ ( Base ‘ 𝑅 ) → ( 𝐴 ∖ { 0 } ) = ( ( ( Base ‘ 𝑅 ) ∖ { 0 } ) ∩ 𝐴 ) )
46 44 45 syl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 ) → ( 𝐴 ∖ { 0 } ) = ( ( ( Base ‘ 𝑅 ) ∖ { 0 } ) ∩ 𝐴 ) )
47 42 46 sseqtrrd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 ) → ( Unit ‘ 𝑆 ) ⊆ ( 𝐴 ∖ { 0 } ) )
48 43 ad2antlr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 ) ) → 𝐴 ⊆ ( Base ‘ 𝑅 ) )
49 simprl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 ) ) → 𝑥 ∈ ( 𝐴 ∖ { 0 } ) )
50 49 7 sylib ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 0 ) )
51 50 simpld ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 ) ) → 𝑥 ∈ 𝐴 )
52 48 51 sseldd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
53 50 simprd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 ) ) → 𝑥 ≠ 0 )
54 34 31 2 drngunit ⊢ ( 𝑅 ∈ DivRing → ( 𝑥 ∈ ( Unit ‘ 𝑅 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ≠ 0 ) ) )
55 54 ad2antrr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 ) ) → ( 𝑥 ∈ ( Unit ‘ 𝑅 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ≠ 0 ) ) )
56 52 53 55 mpbir2and ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 ) ) → 𝑥 ∈ ( Unit ‘ 𝑅 ) )
57 simprr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 ) ) → ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 )
58 1 31 18 3 subrgunit ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( 𝑥 ∈ ( Unit ‘ 𝑆 ) ↔ ( 𝑥 ∈ ( Unit ‘ 𝑅 ) ∧ 𝑥 ∈ 𝐴 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 ) ) )
59 58 ad2antlr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 ) ) → ( 𝑥 ∈ ( Unit ‘ 𝑆 ) ↔ ( 𝑥 ∈ ( Unit ‘ 𝑅 ) ∧ 𝑥 ∈ 𝐴 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 ) ) )
60 56 51 57 59 mpbir3and ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 ) ) → 𝑥 ∈ ( Unit ‘ 𝑆 ) )
61 60 expr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ) → ( ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 → 𝑥 ∈ ( Unit ‘ 𝑆 ) ) )
62 61 ralimdva ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) → ( ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 → ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) 𝑥 ∈ ( Unit ‘ 𝑆 ) ) )
63 62 imp ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 ) → ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) 𝑥 ∈ ( Unit ‘ 𝑆 ) )
64 dfss3 ⊢ ( ( 𝐴 ∖ { 0 } ) ⊆ ( Unit ‘ 𝑆 ) ↔ ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) 𝑥 ∈ ( Unit ‘ 𝑆 ) )
65 63 64 sylibr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 ) → ( 𝐴 ∖ { 0 } ) ⊆ ( Unit ‘ 𝑆 ) )
66 47 65 eqssd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 ) → ( Unit ‘ 𝑆 ) = ( 𝐴 ∖ { 0 } ) )
67 14 ad2antlr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 ) → 0 = ( 0g ‘ 𝑆 ) )
68 67 sneqd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 ) → { 0 } = { ( 0g ‘ 𝑆 ) } )
69 40 68 difeq12d ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 ) → ( 𝐴 ∖ { 0 } ) = ( ( Base ‘ 𝑆 ) ∖ { ( 0g ‘ 𝑆 ) } ) )
70 66 69 eqtrd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 ) → ( Unit ‘ 𝑆 ) = ( ( Base ‘ 𝑆 ) ∖ { ( 0g ‘ 𝑆 ) } ) )
71 17 18 19 isdrng ⊢ ( 𝑆 ∈ DivRing ↔ ( 𝑆 ∈ Ring ∧ ( Unit ‘ 𝑆 ) = ( ( Base ‘ 𝑆 ) ∖ { ( 0g ‘ 𝑆 ) } ) ) )
72 30 70 71 sylanbrc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 ) → 𝑆 ∈ DivRing )
73 29 72 impbida ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) → ( 𝑆 ∈ DivRing ↔ ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ( 𝐼 ‘ 𝑥 ) ∈ 𝐴 ) )