Metamath Proof Explorer

Theorem issubrngd2

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

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

Proof

Step Hyp Ref Expression
1 issubrngd.s ⊢ ( 𝜑 → 𝑆 = ( 𝐼 ↾s 𝐷 ) )
2 issubrngd.z ⊢ ( 𝜑 → 0 = ( 0g ‘ 𝐼 ) )
3 issubrngd.p ⊢ ( 𝜑 → + = ( +g ‘ 𝐼 ) )
4 issubrngd.ss ⊢ ( 𝜑 → 𝐷 ⊆ ( Base ‘ 𝐼 ) )
5 issubrngd.zcl ⊢ ( 𝜑 → 0 ∈ 𝐷 )
6 issubrngd.acl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑥 + 𝑦 ) ∈ 𝐷 )
7 issubrngd.ncl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( invg ‘ 𝐼 ) ‘ 𝑥 ) ∈ 𝐷 )
8 issubrngd.o ⊢ ( 𝜑 → 1 = ( 1r ‘ 𝐼 ) )
9 issubrngd.t ⊢ ( 𝜑 → · = ( .r ‘ 𝐼 ) )
10 issubrngd.ocl ⊢ ( 𝜑 → 1 ∈ 𝐷 )
11 issubrngd.tcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑥 · 𝑦 ) ∈ 𝐷 )
12 issubrngd.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 ‘ 𝐼 ) )