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

Metamath Proof Explorer

Theorem cnfld1OLD

Description: Obsolete version of cnfld1 as of 30-Apr-2025. (Contributed by Stefan O'Rear, 27-Nov-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion cnfld1OLD 1 = ( 1r ‘ ℂfld )

Proof

Step Hyp Ref Expression
1 ax-1cn ⊢ 1 ∈ ℂ
2 mullid ⊢ ( 𝑥 ∈ ℂ → ( 1 · 𝑥 ) = 𝑥 )
3 mulrid ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 · 1 ) = 𝑥 )
4 2 3 jca ⊢ ( 𝑥 ∈ ℂ → ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 1 ) = 𝑥 ) )
5 4 rgen ⊢ ∀ 𝑥 ∈ ℂ ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 1 ) = 𝑥 )
6 1 5 pm3.2i ⊢ ( 1 ∈ ℂ ∧ ∀ 𝑥 ∈ ℂ ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 1 ) = 𝑥 ) )
7 cnring ⊢ ℂfld ∈ Ring
8 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
9 cnfldmul ⊢ · = ( .r ‘ ℂfld )
10 eqid ⊢ ( 1r ‘ ℂfld ) = ( 1r ‘ ℂfld )
11 8 9 10 isringid ⊢ ( ℂfld ∈ Ring → ( ( 1 ∈ ℂ ∧ ∀ 𝑥 ∈ ℂ ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 1 ) = 𝑥 ) ) ↔ ( 1r ‘ ℂfld ) = 1 ) )
12 7 11 ax-mp ⊢ ( ( 1 ∈ ℂ ∧ ∀ 𝑥 ∈ ℂ ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 1 ) = 𝑥 ) ) ↔ ( 1r ‘ ℂfld ) = 1 )
13 6 12 mpbi ⊢ ( 1r ‘ ℂfld ) = 1
14 13 eqcomi ⊢ 1 = ( 1r ‘ ℂfld )