Theorem cnsubglem

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

	Ref	Expression
Hypotheses	cnsubglem.1	⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ )
	cnsubglem.2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 + 𝑦 ) ∈ 𝐴 )
	cnsubglem.3	⊢ ( 𝑥 ∈ 𝐴 → - 𝑥 ∈ 𝐴 )
	cnsubglem.4	⊢ 𝐵 ∈ 𝐴
Assertion	cnsubglem	⊢ 𝐴 ∈ ( SubGrp ‘ ℂfld )

Proof

Step	Hyp	Ref	Expression
1		cnsubglem.1	⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ )
2		cnsubglem.2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 + 𝑦 ) ∈ 𝐴 )
3		cnsubglem.3	⊢ ( 𝑥 ∈ 𝐴 → - 𝑥 ∈ 𝐴 )
4		cnsubglem.4	⊢ 𝐵 ∈ 𝐴
5	1	ssriv	⊢ 𝐴 ⊆ ℂ
6	4	ne0ii	⊢ 𝐴 ≠ ∅
7	2	ralrimiva	⊢ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐴 ( 𝑥 + 𝑦 ) ∈ 𝐴 )
8		cnfldneg	⊢ ( 𝑥 ∈ ℂ → ( ( invg ‘ ℂfld ) ‘ 𝑥 ) = - 𝑥 )
9	1 8	syl	⊢ ( 𝑥 ∈ 𝐴 → ( ( invg ‘ ℂfld ) ‘ 𝑥 ) = - 𝑥 )
10	9 3	eqeltrd	⊢ ( 𝑥 ∈ 𝐴 → ( ( invg ‘ ℂfld ) ‘ 𝑥 ) ∈ 𝐴 )
11	7 10	jca	⊢ ( 𝑥 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 + 𝑦 ) ∈ 𝐴 ∧ ( ( invg ‘ ℂfld ) ‘ 𝑥 ) ∈ 𝐴 ) )
12	11	rgen	⊢ ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 + 𝑦 ) ∈ 𝐴 ∧ ( ( invg ‘ ℂfld ) ‘ 𝑥 ) ∈ 𝐴 )
13		cnring	⊢ ℂfld ∈ Ring
14		ringgrp	⊢ ( ℂfld ∈ Ring → ℂfld ∈ Grp )
15		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
16		cnfldadd	⊢ + = ( +g ‘ ℂfld )
17		eqid	⊢ ( invg ‘ ℂfld ) = ( invg ‘ ℂfld )
18	15 16 17	issubg2	⊢ ( ℂfld ∈ Grp → ( 𝐴 ∈ ( SubGrp ‘ ℂfld ) ↔ ( 𝐴 ⊆ ℂ ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 + 𝑦 ) ∈ 𝐴 ∧ ( ( invg ‘ ℂfld ) ‘ 𝑥 ) ∈ 𝐴 ) ) ) )
19	13 14 18	mp2b	⊢ ( 𝐴 ∈ ( SubGrp ‘ ℂfld ) ↔ ( 𝐴 ⊆ ℂ ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 + 𝑦 ) ∈ 𝐴 ∧ ( ( invg ‘ ℂfld ) ‘ 𝑥 ) ∈ 𝐴 ) ) )
20	5 6 12 19	mpbir3an	⊢ 𝐴 ∈ ( SubGrp ‘ ℂfld )