Metamath Proof Explorer

Theorem sdrgacs

Description: Closure property of division subrings. (Contributed by Mario Carneiro, 3-Oct-2015)

Ref Expression
Hypothesis subrgacs.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion sdrgacs ( 𝑅 ∈ DivRing → ( SubDRing ‘ 𝑅 ) ∈ ( ACS ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 subrgacs.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 eqid ⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
3 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
4 2 3 issdrg2 ⊢ ( 𝑠 ∈ ( SubDRing ‘ 𝑅 ) ↔ ( 𝑅 ∈ DivRing ∧ 𝑠 ∈ ( SubRing ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( 𝑠 ∖ { ( 0g ‘ 𝑅 ) } ) ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝑠 ) )
5 3anass ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑠 ∈ ( SubRing ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( 𝑠 ∖ { ( 0g ‘ 𝑅 ) } ) ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝑠 ) ↔ ( 𝑅 ∈ DivRing ∧ ( 𝑠 ∈ ( SubRing ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( 𝑠 ∖ { ( 0g ‘ 𝑅 ) } ) ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝑠 ) ) )
6 4 5 bitri ⊢ ( 𝑠 ∈ ( SubDRing ‘ 𝑅 ) ↔ ( 𝑅 ∈ DivRing ∧ ( 𝑠 ∈ ( SubRing ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( 𝑠 ∖ { ( 0g ‘ 𝑅 ) } ) ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝑠 ) ) )
7 6 baib ⊢ ( 𝑅 ∈ DivRing → ( 𝑠 ∈ ( SubDRing ‘ 𝑅 ) ↔ ( 𝑠 ∈ ( SubRing ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( 𝑠 ∖ { ( 0g ‘ 𝑅 ) } ) ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝑠 ) ) )
8 1 subrgss ⊢ ( 𝑠 ∈ ( SubRing ‘ 𝑅 ) → 𝑠 ⊆ 𝐵 )
9 velpw ⊢ ( 𝑠 ∈ 𝒫 𝐵 ↔ 𝑠 ⊆ 𝐵 )
10 8 9 sylibr ⊢ ( 𝑠 ∈ ( SubRing ‘ 𝑅 ) → 𝑠 ∈ 𝒫 𝐵 )
11 10 adantl ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑠 ∈ ( SubRing ‘ 𝑅 ) ) → 𝑠 ∈ 𝒫 𝐵 )
12 iftrue ⊢ ( 𝑥 = ( 0g ‘ 𝑅 ) → if ( 𝑥 = ( 0g ‘ 𝑅 ) , 𝑥 , ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ) = 𝑥 )
13 12 eleq1d ⊢ ( 𝑥 = ( 0g ‘ 𝑅 ) → ( if ( 𝑥 = ( 0g ‘ 𝑅 ) , 𝑥 , ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ) ∈ 𝑦 ↔ 𝑥 ∈ 𝑦 ) )
14 13 biimprd ⊢ ( 𝑥 = ( 0g ‘ 𝑅 ) → ( 𝑥 ∈ 𝑦 → if ( 𝑥 = ( 0g ‘ 𝑅 ) , 𝑥 , ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ) ∈ 𝑦 ) )
15 eldifsni ⊢ ( 𝑥 ∈ ( 𝑦 ∖ { ( 0g ‘ 𝑅 ) } ) → 𝑥 ≠ ( 0g ‘ 𝑅 ) )
16 15 necon2bi ⊢ ( 𝑥 = ( 0g ‘ 𝑅 ) → ¬ 𝑥 ∈ ( 𝑦 ∖ { ( 0g ‘ 𝑅 ) } ) )
17 16 pm2.21d ⊢ ( 𝑥 = ( 0g ‘ 𝑅 ) → ( 𝑥 ∈ ( 𝑦 ∖ { ( 0g ‘ 𝑅 ) } ) → ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝑦 ) )
18 14 17 2thd ⊢ ( 𝑥 = ( 0g ‘ 𝑅 ) → ( ( 𝑥 ∈ 𝑦 → if ( 𝑥 = ( 0g ‘ 𝑅 ) , 𝑥 , ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ) ∈ 𝑦 ) ↔ ( 𝑥 ∈ ( 𝑦 ∖ { ( 0g ‘ 𝑅 ) } ) → ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝑦 ) ) )
19 eldifsn ⊢ ( 𝑥 ∈ ( 𝑦 ∖ { ( 0g ‘ 𝑅 ) } ) ↔ ( 𝑥 ∈ 𝑦 ∧ 𝑥 ≠ ( 0g ‘ 𝑅 ) ) )
20 19 rbaibr ⊢ ( 𝑥 ≠ ( 0g ‘ 𝑅 ) → ( 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ ( 𝑦 ∖ { ( 0g ‘ 𝑅 ) } ) ) )
21 ifnefalse ⊢ ( 𝑥 ≠ ( 0g ‘ 𝑅 ) → if ( 𝑥 = ( 0g ‘ 𝑅 ) , 𝑥 , ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ) = ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) )
22 21 eleq1d ⊢ ( 𝑥 ≠ ( 0g ‘ 𝑅 ) → ( if ( 𝑥 = ( 0g ‘ 𝑅 ) , 𝑥 , ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ) ∈ 𝑦 ↔ ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝑦 ) )
23 20 22 imbi12d ⊢ ( 𝑥 ≠ ( 0g ‘ 𝑅 ) → ( ( 𝑥 ∈ 𝑦 → if ( 𝑥 = ( 0g ‘ 𝑅 ) , 𝑥 , ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ) ∈ 𝑦 ) ↔ ( 𝑥 ∈ ( 𝑦 ∖ { ( 0g ‘ 𝑅 ) } ) → ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝑦 ) ) )
24 18 23 pm2.61ine ⊢ ( ( 𝑥 ∈ 𝑦 → if ( 𝑥 = ( 0g ‘ 𝑅 ) , 𝑥 , ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ) ∈ 𝑦 ) ↔ ( 𝑥 ∈ ( 𝑦 ∖ { ( 0g ‘ 𝑅 ) } ) → ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝑦 ) )
25 24 ralbii2 ⊢ ( ∀ 𝑥 ∈ 𝑦 if ( 𝑥 = ( 0g ‘ 𝑅 ) , 𝑥 , ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ) ∈ 𝑦 ↔ ∀ 𝑥 ∈ ( 𝑦 ∖ { ( 0g ‘ 𝑅 ) } ) ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝑦 )
26 difeq1 ⊢ ( 𝑦 = 𝑠 → ( 𝑦 ∖ { ( 0g ‘ 𝑅 ) } ) = ( 𝑠 ∖ { ( 0g ‘ 𝑅 ) } ) )
27 eleq2w ⊢ ( 𝑦 = 𝑠 → ( ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝑦 ↔ ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝑠 ) )
28 26 27 raleqbidv ⊢ ( 𝑦 = 𝑠 → ( ∀ 𝑥 ∈ ( 𝑦 ∖ { ( 0g ‘ 𝑅 ) } ) ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝑦 ↔ ∀ 𝑥 ∈ ( 𝑠 ∖ { ( 0g ‘ 𝑅 ) } ) ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝑠 ) )
29 25 28 syl5bb ⊢ ( 𝑦 = 𝑠 → ( ∀ 𝑥 ∈ 𝑦 if ( 𝑥 = ( 0g ‘ 𝑅 ) , 𝑥 , ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ) ∈ 𝑦 ↔ ∀ 𝑥 ∈ ( 𝑠 ∖ { ( 0g ‘ 𝑅 ) } ) ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝑠 ) )
30 29 elrab3 ⊢ ( 𝑠 ∈ 𝒫 𝐵 → ( 𝑠 ∈ { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 if ( 𝑥 = ( 0g ‘ 𝑅 ) , 𝑥 , ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ) ∈ 𝑦 } ↔ ∀ 𝑥 ∈ ( 𝑠 ∖ { ( 0g ‘ 𝑅 ) } ) ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝑠 ) )
31 11 30 syl ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑠 ∈ ( SubRing ‘ 𝑅 ) ) → ( 𝑠 ∈ { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 if ( 𝑥 = ( 0g ‘ 𝑅 ) , 𝑥 , ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ) ∈ 𝑦 } ↔ ∀ 𝑥 ∈ ( 𝑠 ∖ { ( 0g ‘ 𝑅 ) } ) ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝑠 ) )
32 31 pm5.32da ⊢ ( 𝑅 ∈ DivRing → ( ( 𝑠 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑠 ∈ { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 if ( 𝑥 = ( 0g ‘ 𝑅 ) , 𝑥 , ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ) ∈ 𝑦 } ) ↔ ( 𝑠 ∈ ( SubRing ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( 𝑠 ∖ { ( 0g ‘ 𝑅 ) } ) ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝑠 ) ) )
33 7 32 bitr4d ⊢ ( 𝑅 ∈ DivRing → ( 𝑠 ∈ ( SubDRing ‘ 𝑅 ) ↔ ( 𝑠 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑠 ∈ { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 if ( 𝑥 = ( 0g ‘ 𝑅 ) , 𝑥 , ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ) ∈ 𝑦 } ) ) )
34 elin ⊢ ( 𝑠 ∈ ( ( SubRing ‘ 𝑅 ) ∩ { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 if ( 𝑥 = ( 0g ‘ 𝑅 ) , 𝑥 , ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ) ∈ 𝑦 } ) ↔ ( 𝑠 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑠 ∈ { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 if ( 𝑥 = ( 0g ‘ 𝑅 ) , 𝑥 , ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ) ∈ 𝑦 } ) )
35 33 34 bitr4di ⊢ ( 𝑅 ∈ DivRing → ( 𝑠 ∈ ( SubDRing ‘ 𝑅 ) ↔ 𝑠 ∈ ( ( SubRing ‘ 𝑅 ) ∩ { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 if ( 𝑥 = ( 0g ‘ 𝑅 ) , 𝑥 , ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ) ∈ 𝑦 } ) ) )
36 35 eqrdv ⊢ ( 𝑅 ∈ DivRing → ( SubDRing ‘ 𝑅 ) = ( ( SubRing ‘ 𝑅 ) ∩ { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 if ( 𝑥 = ( 0g ‘ 𝑅 ) , 𝑥 , ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ) ∈ 𝑦 } ) )
37 1 fvexi ⊢ 𝐵 ∈ V
38 mreacs ⊢ ( 𝐵 ∈ V → ( ACS ‘ 𝐵 ) ∈ ( Moore ‘ 𝒫 𝐵 ) )
39 37 38 mp1i ⊢ ( 𝑅 ∈ DivRing → ( ACS ‘ 𝐵 ) ∈ ( Moore ‘ 𝒫 𝐵 ) )
40 drngring ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
41 1 subrgacs ⊢ ( 𝑅 ∈ Ring → ( SubRing ‘ 𝑅 ) ∈ ( ACS ‘ 𝐵 ) )
42 40 41 syl ⊢ ( 𝑅 ∈ DivRing → ( SubRing ‘ 𝑅 ) ∈ ( ACS ‘ 𝐵 ) )
43 simplr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 = ( 0g ‘ 𝑅 ) ) → 𝑥 ∈ 𝐵 )
44 df-ne ⊢ ( 𝑥 ≠ ( 0g ‘ 𝑅 ) ↔ ¬ 𝑥 = ( 0g ‘ 𝑅 ) )
45 1 3 2 drnginvrcl ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ ( 0g ‘ 𝑅 ) ) → ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝐵 )
46 45 3expa ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑅 ) ) → ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝐵 )
47 44 46 sylan2br ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑥 ∈ 𝐵 ) ∧ ¬ 𝑥 = ( 0g ‘ 𝑅 ) ) → ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝐵 )
48 43 47 ifclda ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑥 ∈ 𝐵 ) → if ( 𝑥 = ( 0g ‘ 𝑅 ) , 𝑥 , ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ) ∈ 𝐵 )
49 48 ralrimiva ⊢ ( 𝑅 ∈ DivRing → ∀ 𝑥 ∈ 𝐵 if ( 𝑥 = ( 0g ‘ 𝑅 ) , 𝑥 , ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ) ∈ 𝐵 )
50 acsfn1 ⊢ ( ( 𝐵 ∈ V ∧ ∀ 𝑥 ∈ 𝐵 if ( 𝑥 = ( 0g ‘ 𝑅 ) , 𝑥 , ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ) ∈ 𝐵 ) → { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 if ( 𝑥 = ( 0g ‘ 𝑅 ) , 𝑥 , ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ) ∈ 𝑦 } ∈ ( ACS ‘ 𝐵 ) )
51 37 49 50 sylancr ⊢ ( 𝑅 ∈ DivRing → { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 if ( 𝑥 = ( 0g ‘ 𝑅 ) , 𝑥 , ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ) ∈ 𝑦 } ∈ ( ACS ‘ 𝐵 ) )
52 mreincl ⊢ ( ( ( ACS ‘ 𝐵 ) ∈ ( Moore ‘ 𝒫 𝐵 ) ∧ ( SubRing ‘ 𝑅 ) ∈ ( ACS ‘ 𝐵 ) ∧ { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 if ( 𝑥 = ( 0g ‘ 𝑅 ) , 𝑥 , ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ) ∈ 𝑦 } ∈ ( ACS ‘ 𝐵 ) ) → ( ( SubRing ‘ 𝑅 ) ∩ { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 if ( 𝑥 = ( 0g ‘ 𝑅 ) , 𝑥 , ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ) ∈ 𝑦 } ) ∈ ( ACS ‘ 𝐵 ) )
53 39 42 51 52 syl3anc ⊢ ( 𝑅 ∈ DivRing → ( ( SubRing ‘ 𝑅 ) ∩ { 𝑦 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝑦 if ( 𝑥 = ( 0g ‘ 𝑅 ) , 𝑥 , ( ( invr ‘ 𝑅 ) ‘ 𝑥 ) ) ∈ 𝑦 } ) ∈ ( ACS ‘ 𝐵 ) )
54 36 53 eqeltrd ⊢ ( 𝑅 ∈ DivRing → ( SubDRing ‘ 𝑅 ) ∈ ( ACS ‘ 𝐵 ) )