Description: Derive the associative law for complex number addition addass to demonstrate the use of the properties of a normed subcomplex vector space for the complex numbers. (Contributed by NM, 12-Jan-2008) (Revised by AV, 9-Oct-2021) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | cnncvsaddassdemo | |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cnring | |- CCfld e. Ring |
|
| 2 | ringgrp | |- ( CCfld e. Ring -> CCfld e. Grp ) |
|
| 3 | 1 2 | ax-mp | |- CCfld e. Grp |
| 4 | cnfldbas | |- CC = ( Base ` CCfld ) |
|
| 5 | cnfldadd | |- + = ( +g ` CCfld ) |
|
| 6 | 4 5 | grpass | |- ( ( CCfld e. Grp /\ ( A e. CC /\ B e. CC /\ C e. CC ) ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) ) |
| 7 | 3 6 | mpan | |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) ) |