Metamath Proof Explorer

Theorem cncrngOLD

Description: Obsolete version of cncrng as of 30-Apr-2025. (Contributed by Mario Carneiro, 8-Jan-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion cncrngOLD ℂfld ∈ CRing

Proof

Step Hyp Ref Expression
1 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
2 1 a1i ⊢ ( ⊤ → ℂ = ( Base ‘ ℂfld ) )
3 cnfldadd ⊢ + = ( +g ‘ ℂfld )
4 3 a1i ⊢ ( ⊤ → + = ( +g ‘ ℂfld ) )
5 cnfldmul ⊢ · = ( .r ‘ ℂfld )
6 5 a1i ⊢ ( ⊤ → · = ( .r ‘ ℂfld ) )
7 addcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 + 𝑦 ) ∈ ℂ )
8 addass ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
9 0cn ⊢ 0 ∈ ℂ
10 addlid ⊢ ( 𝑥 ∈ ℂ → ( 0 + 𝑥 ) = 𝑥 )
11 negcl ⊢ ( 𝑥 ∈ ℂ → - 𝑥 ∈ ℂ )
12 addcom ⊢ ( ( - 𝑥 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( - 𝑥 + 𝑥 ) = ( 𝑥 + - 𝑥 ) )
13 11 12 mpancom ⊢ ( 𝑥 ∈ ℂ → ( - 𝑥 + 𝑥 ) = ( 𝑥 + - 𝑥 ) )
14 negid ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 + - 𝑥 ) = 0 )
15 13 14 eqtrd ⊢ ( 𝑥 ∈ ℂ → ( - 𝑥 + 𝑥 ) = 0 )
16 1 3 7 8 9 10 11 15 isgrpi ⊢ ℂfld ∈ Grp
17 16 a1i ⊢ ( ⊤ → ℂfld ∈ Grp )
18 mulcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
19 18 3adant1 ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
20 mulass ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) )
21 20 adantl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) )
22 adddi ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) )
23 22 adantl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ) → ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) )
24 adddir ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) )
25 24 adantl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ) → ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) )
26 1cnd ⊢ ( ⊤ → 1 ∈ ℂ )
27 mullid ⊢ ( 𝑥 ∈ ℂ → ( 1 · 𝑥 ) = 𝑥 )
28 27 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( 1 · 𝑥 ) = 𝑥 )
29 mulrid ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 · 1 ) = 𝑥 )
30 29 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( 𝑥 · 1 ) = 𝑥 )
31 mulcom ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) = ( 𝑦 · 𝑥 ) )
32 31 3adant1 ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) = ( 𝑦 · 𝑥 ) )
33 2 4 6 17 19 21 23 25 26 28 30 32 iscrngd ⊢ ( ⊤ → ℂfld ∈ CRing )
34 33 mptru ⊢ ℂfld ∈ CRing