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

Metamath Proof Explorer

Theorem cnsubrglemOLD

Description: Obsolete version of cnsubrglem as of 30-Apr-2025. (Contributed by Mario Carneiro, 4-Dec-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses cnsubglem.1 ⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ )
cnsubglem.2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 + 𝑦 ) ∈ 𝐴 )
cnsubglem.3 ⊢ ( 𝑥 ∈ 𝐴 → - 𝑥 ∈ 𝐴 )
cnsubrglem.4 ⊢ 1 ∈ 𝐴
cnsubrglem.5 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 · 𝑦 ) ∈ 𝐴 )
Assertion cnsubrglemOLD 𝐴 ∈ ( SubRing ‘ ℂfld )

Proof

Step Hyp Ref Expression
1 cnsubglem.1 ⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ )
2 cnsubglem.2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 + 𝑦 ) ∈ 𝐴 )
3 cnsubglem.3 ⊢ ( 𝑥 ∈ 𝐴 → - 𝑥 ∈ 𝐴 )
4 cnsubrglem.4 ⊢ 1 ∈ 𝐴
5 cnsubrglem.5 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 · 𝑦 ) ∈ 𝐴 )
6 1 2 3 4 cnsubglem ⊢ 𝐴 ∈ ( SubGrp ‘ ℂfld )
7 5 rgen2 ⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴
8 cnring ⊢ ℂfld ∈ Ring
9 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
10 cnfld1 ⊢ 1 = ( 1r ‘ ℂfld )
11 cnfldmul ⊢ · = ( .r ‘ ℂfld )
12 9 10 11 issubrg2 ⊢ ( ℂfld ∈ Ring → ( 𝐴 ∈ ( SubRing ‘ ℂfld ) ↔ ( 𝐴 ∈ ( SubGrp ‘ ℂfld ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) )
13 8 12 ax-mp ⊢ ( 𝐴 ∈ ( SubRing ‘ ℂfld ) ↔ ( 𝐴 ∈ ( SubGrp ‘ ℂfld ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) )
14 6 4 7 13 mpbir3an ⊢ 𝐴 ∈ ( SubRing ‘ ℂfld )