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