Metamath Proof Explorer

Theorem cnmsubglem

Description: Lemma for rpmsubg and friends. (Contributed by Mario Carneiro, 21-Jun-2015)

Ref Expression
Hypotheses cnmgpabl.m ⊢ 𝑀 = ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) )
cnmsubglem.1 ⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ )
cnmsubglem.2 ⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ≠ 0 )
cnmsubglem.3 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 · 𝑦 ) ∈ 𝐴 )
cnmsubglem.4 ⊢ 1 ∈ 𝐴
cnmsubglem.5 ⊢ ( 𝑥 ∈ 𝐴 → ( 1 / 𝑥 ) ∈ 𝐴 )
Assertion cnmsubglem 𝐴 ∈ ( SubGrp ‘ 𝑀 )

Proof

Step Hyp Ref Expression
1 cnmgpabl.m ⊢ 𝑀 = ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) )
2 cnmsubglem.1 ⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ )
3 cnmsubglem.2 ⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ≠ 0 )
4 cnmsubglem.3 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 · 𝑦 ) ∈ 𝐴 )
5 cnmsubglem.4 ⊢ 1 ∈ 𝐴
6 cnmsubglem.5 ⊢ ( 𝑥 ∈ 𝐴 → ( 1 / 𝑥 ) ∈ 𝐴 )
7 eldifsn ⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
8 2 3 7 sylanbrc ⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( ℂ ∖ { 0 } ) )
9 8 ssriv ⊢ 𝐴 ⊆ ( ℂ ∖ { 0 } )
10 5 ne0ii ⊢ 𝐴 ≠ ∅
11 4 ralrimiva ⊢ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 )
12 cnfldinv ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) → ( ( invr ‘ ℂfld ) ‘ 𝑥 ) = ( 1 / 𝑥 ) )
13 2 3 12 syl2anc ⊢ ( 𝑥 ∈ 𝐴 → ( ( invr ‘ ℂfld ) ‘ 𝑥 ) = ( 1 / 𝑥 ) )
14 13 6 eqeltrd ⊢ ( 𝑥 ∈ 𝐴 → ( ( invr ‘ ℂfld ) ‘ 𝑥 ) ∈ 𝐴 )
15 11 14 jca ⊢ ( 𝑥 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ∧ ( ( invr ‘ ℂfld ) ‘ 𝑥 ) ∈ 𝐴 ) )
16 15 rgen ⊢ ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ∧ ( ( invr ‘ ℂfld ) ‘ 𝑥 ) ∈ 𝐴 )
17 1 cnmgpabl ⊢ 𝑀 ∈ Abel
18 ablgrp ⊢ ( 𝑀 ∈ Abel → 𝑀 ∈ Grp )
19 difss ⊢ ( ℂ ∖ { 0 } ) ⊆ ℂ
20 eqid ⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
21 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
22 20 21 mgpbas ⊢ ℂ = ( Base ‘ ( mulGrp ‘ ℂfld ) )
23 1 22 ressbas2 ⊢ ( ( ℂ ∖ { 0 } ) ⊆ ℂ → ( ℂ ∖ { 0 } ) = ( Base ‘ 𝑀 ) )
24 19 23 ax-mp ⊢ ( ℂ ∖ { 0 } ) = ( Base ‘ 𝑀 )
25 cnex ⊢ ℂ ∈ V
26 difexg ⊢ ( ℂ ∈ V → ( ℂ ∖ { 0 } ) ∈ V )
27 cnfldmul ⊢ · = ( .r ‘ ℂfld )
28 20 27 mgpplusg ⊢ · = ( +g ‘ ( mulGrp ‘ ℂfld ) )
29 1 28 ressplusg ⊢ ( ( ℂ ∖ { 0 } ) ∈ V → · = ( +g ‘ 𝑀 ) )
30 25 26 29 mp2b ⊢ · = ( +g ‘ 𝑀 )
31 cnfld0 ⊢ 0 = ( 0g ‘ ℂfld )
32 cndrng ⊢ ℂfld ∈ DivRing
33 21 31 32 drngui ⊢ ( ℂ ∖ { 0 } ) = ( Unit ‘ ℂfld )
34 eqid ⊢ ( invr ‘ ℂfld ) = ( invr ‘ ℂfld )
35 33 1 34 invrfval ⊢ ( invr ‘ ℂfld ) = ( invg ‘ 𝑀 )
36 24 30 35 issubg2 ⊢ ( 𝑀 ∈ Grp → ( 𝐴 ∈ ( SubGrp ‘ 𝑀 ) ↔ ( 𝐴 ⊆ ( ℂ ∖ { 0 } ) ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ∧ ( ( invr ‘ ℂfld ) ‘ 𝑥 ) ∈ 𝐴 ) ) ) )
37 17 18 36 mp2b ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝑀 ) ↔ ( 𝐴 ⊆ ( ℂ ∖ { 0 } ) ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ∧ ( ( invr ‘ ℂfld ) ‘ 𝑥 ) ∈ 𝐴 ) ) )
38 9 10 16 37 mpbir3an ⊢ 𝐴 ∈ ( SubGrp ‘ 𝑀 )