Metamath Proof Explorer

Theorem issubrgd

Description: Prove a subring by closure (definition version). (Contributed by Stefan O'Rear, 7-Dec-2014)

Ref Expression
Hypotheses issubrgd.s ⊢ ( 𝜑 → 𝑆 = ( 𝐼 ↾s 𝐷 ) )
issubrgd.z ⊢ ( 𝜑 → 0 = ( 0g ‘ 𝐼 ) )
issubrgd.p ⊢ ( 𝜑 → + = ( +g ‘ 𝐼 ) )
issubrgd.ss ⊢ ( 𝜑 → 𝐷 ⊆ ( Base ‘ 𝐼 ) )
issubrgd.zcl ⊢ ( 𝜑 → 0 ∈ 𝐷 )
issubrgd.acl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑥 + 𝑦 ) ∈ 𝐷 )
issubrgd.ncl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( invg ‘ 𝐼 ) ‘ 𝑥 ) ∈ 𝐷 )
issubrgd.o ⊢ ( 𝜑 → 1 = ( 1r ‘ 𝐼 ) )
issubrgd.t ⊢ ( 𝜑 → · = ( .r ‘ 𝐼 ) )
issubrgd.ocl ⊢ ( 𝜑 → 1 ∈ 𝐷 )
issubrgd.tcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑥 · 𝑦 ) ∈ 𝐷 )
issubrgd.g ⊢ ( 𝜑 → 𝐼 ∈ Ring )
Assertion issubrgd ( 𝜑 → 𝐷 ∈ ( SubRing ‘ 𝐼 ) )

Proof

Step Hyp Ref Expression
1 issubrgd.s ⊢ ( 𝜑 → 𝑆 = ( 𝐼 ↾s 𝐷 ) )
2 issubrgd.z ⊢ ( 𝜑 → 0 = ( 0g ‘ 𝐼 ) )
3 issubrgd.p ⊢ ( 𝜑 → + = ( +g ‘ 𝐼 ) )
4 issubrgd.ss ⊢ ( 𝜑 → 𝐷 ⊆ ( Base ‘ 𝐼 ) )
5 issubrgd.zcl ⊢ ( 𝜑 → 0 ∈ 𝐷 )
6 issubrgd.acl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑥 + 𝑦 ) ∈ 𝐷 )
7 issubrgd.ncl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( invg ‘ 𝐼 ) ‘ 𝑥 ) ∈ 𝐷 )
8 issubrgd.o ⊢ ( 𝜑 → 1 = ( 1r ‘ 𝐼 ) )
9 issubrgd.t ⊢ ( 𝜑 → · = ( .r ‘ 𝐼 ) )
10 issubrgd.ocl ⊢ ( 𝜑 → 1 ∈ 𝐷 )
11 issubrgd.tcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑥 · 𝑦 ) ∈ 𝐷 )
12 issubrgd.g ⊢ ( 𝜑 → 𝐼 ∈ Ring )
13 ringgrp ⊢ ( 𝐼 ∈ Ring → 𝐼 ∈ Grp )
14 12 13 syl ⊢ ( 𝜑 → 𝐼 ∈ Grp )
15 1 2 3 4 5 6 7 14 issubgrpd2 ⊢ ( 𝜑 → 𝐷 ∈ ( SubGrp ‘ 𝐼 ) )
16 8 10 eqeltrrd ⊢ ( 𝜑 → ( 1r ‘ 𝐼 ) ∈ 𝐷 )
17 9 oveqdr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝑥 · 𝑦 ) = ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) )
18 11 3expb ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝐷 )
19 17 18 eqeltrrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) ∈ 𝐷 )
20 19 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) ∈ 𝐷 )
21 eqid ⊢ ( Base ‘ 𝐼 ) = ( Base ‘ 𝐼 )
22 eqid ⊢ ( 1r ‘ 𝐼 ) = ( 1r ‘ 𝐼 )
23 eqid ⊢ ( .r ‘ 𝐼 ) = ( .r ‘ 𝐼 )
24 21 22 23 issubrg2 ⊢ ( 𝐼 ∈ Ring → ( 𝐷 ∈ ( SubRing ‘ 𝐼 ) ↔ ( 𝐷 ∈ ( SubGrp ‘ 𝐼 ) ∧ ( 1r ‘ 𝐼 ) ∈ 𝐷 ∧ ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) ∈ 𝐷 ) ) )
25 12 24 syl ⊢ ( 𝜑 → ( 𝐷 ∈ ( SubRing ‘ 𝐼 ) ↔ ( 𝐷 ∈ ( SubGrp ‘ 𝐼 ) ∧ ( 1r ‘ 𝐼 ) ∈ 𝐷 ∧ ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( 𝑥 ( .r ‘ 𝐼 ) 𝑦 ) ∈ 𝐷 ) ) )
26 15 16 20 25 mpbir3and ⊢ ( 𝜑 → 𝐷 ∈ ( SubRing ‘ 𝐼 ) )