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

Metamath Proof Explorer

Theorem cnsubrglem

Description: Lemma for resubdrg and friends. (Contributed by Mario Carneiro, 4-Dec-2014) Avoid ax-mulf . (Revised by GG, 30-Apr-2025)

Ref Expression
Hypotheses cnsubglem.1 ⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ )
cnsubglem.2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 + 𝑦 ) ∈ 𝐴 )
cnsubglem.3 ⊢ ( 𝑥 ∈ 𝐴 → - 𝑥 ∈ 𝐴 )
cnsubrglem.4 ⊢ 1 ∈ 𝐴
cnsubrglem.5 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 · 𝑦 ) ∈ 𝐴 )
Assertion cnsubrglem 𝐴 ∈ ( 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 1 adantr ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → 𝑥 ∈ ℂ )
8 1 ax-gen ⊢ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ )
9 eleq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
10 eleq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ ℂ ↔ 𝑦 ∈ ℂ ) )
11 9 10 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ ) ↔ ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ℂ ) ) )
12 11 spvv ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ ) → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ℂ ) )
13 8 12 ax-mp ⊢ ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ℂ )
14 13 adantl ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℂ )
15 7 14 jca ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) )
16 ovmpot ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) = ( 𝑥 · 𝑦 ) )
17 15 16 syl ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) = ( 𝑥 · 𝑦 ) )
18 17 eqcomd ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 · 𝑦 ) = ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) )
19 18 eleq1d ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 · 𝑦 ) ∈ 𝐴 ↔ ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ∈ 𝐴 ) )
20 5 19 mpbid ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ∈ 𝐴 )
21 20 rgen2 ⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ∈ 𝐴
22 cnring ⊢ ℂfld ∈ Ring
23 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
24 cnfld1 ⊢ 1 = ( 1r ‘ ℂfld )
25 mpocnfldmul ⊢ ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) = ( .r ‘ ℂfld )
26 23 24 25 issubrg2 ⊢ ( ℂfld ∈ Ring → ( 𝐴 ∈ ( SubRing ‘ ℂfld ) ↔ ( 𝐴 ∈ ( SubGrp ‘ ℂfld ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ∈ 𝐴 ) ) )
27 22 26 ax-mp ⊢ ( 𝐴 ∈ ( SubRing ‘ ℂfld ) ↔ ( 𝐴 ∈ ( SubGrp ‘ ℂfld ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ∈ 𝐴 ) )
28 6 4 21 27 mpbir3an ⊢ 𝐴 ∈ ( SubRing ‘ ℂfld )