Step |
Hyp |
Ref |
Expression |
1 |
|
cnfldbas |
⊢ ℂ = ( Base ‘ ℂfld ) |
2 |
1
|
a1i |
⊢ ( ⊤ → ℂ = ( Base ‘ ℂfld ) ) |
3 |
|
cnfldadd |
⊢ + = ( +g ‘ ℂfld ) |
4 |
3
|
a1i |
⊢ ( ⊤ → + = ( +g ‘ ℂfld ) ) |
5 |
|
mpocnfldmul |
⊢ ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) = ( .r ‘ ℂfld ) |
6 |
5
|
a1i |
⊢ ( ⊤ → ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) = ( .r ‘ ℂfld ) ) |
7 |
|
addcl |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 + 𝑦 ) ∈ ℂ ) |
8 |
|
addass |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) |
9 |
|
0cn |
⊢ 0 ∈ ℂ |
10 |
|
addlid |
⊢ ( 𝑥 ∈ ℂ → ( 0 + 𝑥 ) = 𝑥 ) |
11 |
|
negcl |
⊢ ( 𝑥 ∈ ℂ → - 𝑥 ∈ ℂ ) |
12 |
|
id |
⊢ ( 𝑥 ∈ ℂ → 𝑥 ∈ ℂ ) |
13 |
11 12
|
addcomd |
⊢ ( 𝑥 ∈ ℂ → ( - 𝑥 + 𝑥 ) = ( 𝑥 + - 𝑥 ) ) |
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 |
|
mpomulf |
⊢ ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) : ( ℂ × ℂ ) ⟶ ℂ |
19 |
18
|
fovcl |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ∈ ℂ ) |
20 |
19
|
3adant1 |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ∈ ℂ ) |
21 |
|
mulass |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) ) |
22 |
|
mulcl |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) ∈ ℂ ) |
23 |
|
ovmpot |
⊢ ( ( ( 𝑥 · 𝑦 ) ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 · 𝑦 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) = ( ( 𝑥 · 𝑦 ) · 𝑧 ) ) |
24 |
22 23
|
stoic3 |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 · 𝑦 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) = ( ( 𝑥 · 𝑦 ) · 𝑧 ) ) |
25 |
|
simp1 |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → 𝑥 ∈ ℂ ) |
26 |
|
mulcl |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑦 · 𝑧 ) ∈ ℂ ) |
27 |
26
|
3adant1 |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑦 · 𝑧 ) ∈ ℂ ) |
28 |
|
ovmpot |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑦 · 𝑧 ) ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑦 · 𝑧 ) ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) ) |
29 |
25 27 28
|
syl2anc |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑦 · 𝑧 ) ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) ) |
30 |
21 24 29
|
3eqtr4d |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 · 𝑦 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) = ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑦 · 𝑧 ) ) ) |
31 |
|
ovmpot |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) = ( 𝑥 · 𝑦 ) ) |
32 |
31
|
3adant3 |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) = ( 𝑥 · 𝑦 ) ) |
33 |
32
|
oveq1d |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) = ( ( 𝑥 · 𝑦 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) ) |
34 |
|
ovmpot |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑦 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) = ( 𝑦 · 𝑧 ) ) |
35 |
34
|
3adant1 |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑦 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) = ( 𝑦 · 𝑧 ) ) |
36 |
35
|
oveq2d |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑦 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) ) = ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑦 · 𝑧 ) ) ) |
37 |
30 33 36
|
3eqtr4d |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) = ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑦 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) ) ) |
38 |
37
|
adantl |
⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ) → ( ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) = ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑦 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) ) ) |
39 |
|
adddi |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ) |
40 |
|
addcl |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑦 + 𝑧 ) ∈ ℂ ) |
41 |
40
|
3adant1 |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑦 + 𝑧 ) ∈ ℂ ) |
42 |
|
ovmpot |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑦 + 𝑧 ) ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑦 + 𝑧 ) ) = ( 𝑥 · ( 𝑦 + 𝑧 ) ) ) |
43 |
25 41 42
|
syl2anc |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑦 + 𝑧 ) ) = ( 𝑥 · ( 𝑦 + 𝑧 ) ) ) |
44 |
|
ovmpot |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) = ( 𝑥 · 𝑧 ) ) |
45 |
44
|
3adant2 |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) = ( 𝑥 · 𝑧 ) ) |
46 |
32 45
|
oveq12d |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) + ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ) |
47 |
39 43 46
|
3eqtr4d |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) + ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) ) ) |
48 |
47
|
adantl |
⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) + ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) ) ) |
49 |
|
adddir |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) |
50 |
|
ovmpot |
⊢ ( ( ( 𝑥 + 𝑦 ) ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 + 𝑦 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) = ( ( 𝑥 + 𝑦 ) · 𝑧 ) ) |
51 |
7 50
|
stoic3 |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 + 𝑦 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) = ( ( 𝑥 + 𝑦 ) · 𝑧 ) ) |
52 |
45 35
|
oveq12d |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) + ( 𝑦 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) |
53 |
49 51 52
|
3eqtr4d |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 + 𝑦 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) = ( ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) + ( 𝑦 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) ) ) |
54 |
53
|
adantl |
⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ) → ( ( 𝑥 + 𝑦 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) = ( ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) + ( 𝑦 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) ) ) |
55 |
|
1cnd |
⊢ ( ⊤ → 1 ∈ ℂ ) |
56 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
57 |
|
ovmpot |
⊢ ( ( 1 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 1 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑥 ) = ( 1 · 𝑥 ) ) |
58 |
56 57
|
mpan |
⊢ ( 𝑥 ∈ ℂ → ( 1 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑥 ) = ( 1 · 𝑥 ) ) |
59 |
|
mullid |
⊢ ( 𝑥 ∈ ℂ → ( 1 · 𝑥 ) = 𝑥 ) |
60 |
58 59
|
eqtrd |
⊢ ( 𝑥 ∈ ℂ → ( 1 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑥 ) = 𝑥 ) |
61 |
60
|
adantl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( 1 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑥 ) = 𝑥 ) |
62 |
|
ovmpot |
⊢ ( ( 𝑥 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 1 ) = ( 𝑥 · 1 ) ) |
63 |
56 62
|
mpan2 |
⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 1 ) = ( 𝑥 · 1 ) ) |
64 |
|
mulrid |
⊢ ( 𝑥 ∈ ℂ → ( 𝑥 · 1 ) = 𝑥 ) |
65 |
63 64
|
eqtrd |
⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 1 ) = 𝑥 ) |
66 |
65
|
adantl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 1 ) = 𝑥 ) |
67 |
|
mulcom |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) = ( 𝑦 · 𝑥 ) ) |
68 |
|
ovmpot |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑦 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑥 ) = ( 𝑦 · 𝑥 ) ) |
69 |
68
|
ancoms |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑦 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑥 ) = ( 𝑦 · 𝑥 ) ) |
70 |
67 31 69
|
3eqtr4d |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) = ( 𝑦 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑥 ) ) |
71 |
70
|
3adant1 |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) = ( 𝑦 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑥 ) ) |
72 |
2 4 6 17 20 38 48 54 55 61 66 71
|
iscrngd |
⊢ ( ⊤ → ℂfld ∈ CRing ) |
73 |
72
|
mptru |
⊢ ℂfld ∈ CRing |