This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )