Theorem cnsubdrglem

Description: Lemma for resubdrg and friends. (Contributed by Mario Carneiro, 4-Dec-2014)

	Ref	Expression
Hypotheses	cnsubglem.1	⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ )
	cnsubglem.2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 + 𝑦 ) ∈ 𝐴 )
	cnsubglem.3	⊢ ( 𝑥 ∈ 𝐴 → - 𝑥 ∈ 𝐴 )
	cnsubrglem.4	⊢ 1 ∈ 𝐴
	cnsubrglem.5	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 · 𝑦 ) ∈ 𝐴 )
	cnsubrglem.6	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 0 ) → ( 1 / 𝑥 ) ∈ 𝐴 )
Assertion	cnsubdrglem	⊢ ( 𝐴 ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s 𝐴 ) ∈ DivRing )

Proof

Step	Hyp	Ref	Expression
1		cnsubglem.1	⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ )
2		cnsubglem.2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 + 𝑦 ) ∈ 𝐴 )
3		cnsubglem.3	⊢ ( 𝑥 ∈ 𝐴 → - 𝑥 ∈ 𝐴 )
4		cnsubrglem.4	⊢ 1 ∈ 𝐴
5		cnsubrglem.5	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 · 𝑦 ) ∈ 𝐴 )
6		cnsubrglem.6	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 0 ) → ( 1 / 𝑥 ) ∈ 𝐴 )
7	1 2 3 4 5	cnsubrglem	⊢ 𝐴 ∈ ( SubRing ‘ ℂfld )
8		cndrng	⊢ ℂfld ∈ DivRing
9		eqid	⊢ ( ℂfld ↾s 𝐴 ) = ( ℂfld ↾s 𝐴 )
10		cnfld0	⊢ 0 = ( 0g ‘ ℂfld )
11		eqid	⊢ ( invr ‘ ℂfld ) = ( invr ‘ ℂfld )
12	9 10 11	issubdrg	⊢ ( ( ℂfld ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ ℂfld ) ) → ( ( ℂfld ↾s 𝐴 ) ∈ DivRing ↔ ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ( ( invr ‘ ℂfld ) ‘ 𝑥 ) ∈ 𝐴 ) )
13	8 7 12	mp2an	⊢ ( ( ℂfld ↾s 𝐴 ) ∈ DivRing ↔ ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ( ( invr ‘ ℂfld ) ‘ 𝑥 ) ∈ 𝐴 )
14		cnring	⊢ ℂfld ∈ Ring
15	1	ssriv	⊢ 𝐴 ⊆ ℂ
16		ssdif	⊢ ( 𝐴 ⊆ ℂ → ( 𝐴 ∖ { 0 } ) ⊆ ( ℂ ∖ { 0 } ) )
17	15 16	ax-mp	⊢ ( 𝐴 ∖ { 0 } ) ⊆ ( ℂ ∖ { 0 } )
18	17	sseli	⊢ ( 𝑥 ∈ ( 𝐴 ∖ { 0 } ) → 𝑥 ∈ ( ℂ ∖ { 0 } ) )
19		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
20	19 10 8	drngui	⊢ ( ℂ ∖ { 0 } ) = ( Unit ‘ ℂfld )
21		cnflddiv	⊢ / = ( /r ‘ ℂfld )
22		cnfld1	⊢ 1 = ( 1r ‘ ℂfld )
23	19 20 21 22 11	ringinvdv	⊢ ( ( ℂfld ∈ Ring ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( ( invr ‘ ℂfld ) ‘ 𝑥 ) = ( 1 / 𝑥 ) )
24	14 18 23	sylancr	⊢ ( 𝑥 ∈ ( 𝐴 ∖ { 0 } ) → ( ( invr ‘ ℂfld ) ‘ 𝑥 ) = ( 1 / 𝑥 ) )
25		eldifsn	⊢ ( 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 0 ) )
26	25 6	sylbi	⊢ ( 𝑥 ∈ ( 𝐴 ∖ { 0 } ) → ( 1 / 𝑥 ) ∈ 𝐴 )
27	24 26	eqeltrd	⊢ ( 𝑥 ∈ ( 𝐴 ∖ { 0 } ) → ( ( invr ‘ ℂfld ) ‘ 𝑥 ) ∈ 𝐴 )
28	13 27	mprgbir	⊢ ( ℂfld ↾s 𝐴 ) ∈ DivRing
29	7 28	pm3.2i	⊢ ( 𝐴 ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s 𝐴 ) ∈ DivRing )