environ
vocabularies HIDDEN, ARYTM_3, FUNCT_1, RELAT_1, RLVECT_1, VECTSP_1, ALGSTR_0, TARSKI, INT_1, FUNCT_2, VECTSP_2, VECTSP10, STRUCT_0, SUBSET_1, SUPINF_2, NAT_1, CARD_1, MESFUNC1, INT_3, GROUP_1, ARYTM_1, ORDINAL1, INT_2, QUOFIELD, MSSUBFAM, BINOP_1, GROUP_6, MOD_4, LATTICES, NUMBERS, IDEAL_1, C0SP1, ZFMISC_1, FUNCSDOM, RING_2, FINSET_1, XXREAL_0, WELLORD1, REALSET1, XBOOLE_0, EC_PF_1, BINOP_2, COMPLFLD, GAUSSINT, XCMPLX_0, REAL_1, RING_3, RAT_1, NEWTON;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, ORDINAL1, FUNCT_2, BINOP_1, REALSET1, XCMPLX_0, XXREAL_0, XREAL_0, CARD_1, BINOP_2, XXREAL_2, NAT_1, INT_1, INT_2, NAT_D, RAT_1, INT_3, NUMBERS, NEWTON, MATRLIN2, STRUCT_0, MOD_4, BINOM, ALGSTR_0, GROUP_1, GROUP_6, RLVECT_1, GCD_1, VECTSP_2, VECTSP_1, GR_CY_1, COMPLFLD, VECTSP10, EC_PF_1, GAUSSINT, IDEAL_1, QUOFIELD, C0SP1, RING_1, RING_2;
definitions TARSKI, XBOOLE_0, FUNCT_2, XREAL_0, RAT_1, INT_1, STRUCT_0, ALGSTR_0, VECTSP_1, REALSET1, GROUP_1, GROUP_6, RLVECT_1, QUOFIELD, RING_2;
theorems GROUP_1, GROUP_6, VECTSP_1, VECTSP_2, FUNCT_2, TARSKI, BINOM, INT_1, INT_2, INT_3, FUNCT_1, RLVECT_1, RING_2, EC_PF_1, XREAL_1, NAT_2, XXREAL_0, ORDINAL1, XBOOLE_0, IDEAL_1, XCMPLX_1, XXREAL_2, C0SP1, NAT_1, QUOFIELD, GR_CY_1, GAUSSINT, SUBSET_1, GCD_1, NUMBERS, RELAT_1, ZFMISC_1, BINOP_2, COMPLFLD, RAT_1, EC_PF_2, XCMPLX_0, PEPIN, PRE_FF, WSIERP_1;
schemes NAT_1, INT_1, FUNCT_2;
registrations ORDINAL1, XXREAL_0, XREAL_0, RELSET_1, VECTSP_1, STRUCT_0, MEMBERED, NUMBERS, XBOOLE_0, RAT_1, RLVECT_1, INT_1, INT_3, COMPLFLD, REALSET1, TOPALG_7, GAUSSINT, NAT_1, ALGSTR_1, SUBSET_1, RELAT_1, FUNCT_2, ALGSTR_0, QUOFIELD, GROUP_6, MOD_4, RINGCAT1, RING_1, C0SP1, GRCAT_1, XCMPLX_0, XXREAL_2, FOMODEL0, RING_2, NAT_2, FUNCT_1, CARD_1, EC_PF_1;
constructors HIDDEN, BINOM, QUOFIELD, MOD_4, REALSET1, BINOP_2, GCD_1, RINGCAT1, XXREAL_2, RING_2, GAUSSINT, GR_CY_1, EC_PF_1, NAT_D, MATRLIN2, TOPALG_7;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
equalities BINOP_1, REALSET1, XCMPLX_0, STRUCT_0, ALGSTR_0, VECTSP_1, QUOFIELD, COMPLEX1, VECTSP10, INT_3, GAUSSINT, XBOOLE_0, RAT_1, INT_1, MATRLIN2;
expansions STRUCT_0, GROUP_1, VECTSP_1, XBOOLE_0, FUNCT_1, RINGCAT1, QUOFIELD, GROUP_6, TARSKI, RING_2, RAT_1, INT_1;
set I = INT.Ring ;
Lm2:
( the carrier of F_Real is Subset of the carrier of F_Complex & the addF of F_Real = the addF of F_Complex || the carrier of F_Real & the multF of F_Real = the multF of F_Complex || the carrier of F_Real & 1. F_Complex = 1. F_Real & 0. F_Complex = 0. F_Real )
by NUMBERS:11, COMPLFLD:def 1, Th2, Th3;
Lm3:
for u, v being Integer
for p, q being Element of INT.Ring st u = p & v = q holds
( u divides v iff p divides q )
Lm4:
( the carrier of INT.Ring c= the carrier of F_Rat & the addF of INT.Ring = the addF of F_Rat || the carrier of INT.Ring & the multF of INT.Ring = the multF of F_Rat || the carrier of INT.Ring & 1. INT.Ring = 1. F_Rat & 0. INT.Ring = 0. F_Rat )
by NUMBERS:14, Th4, Th5;
Lm5:
for R being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for a being Element of R
for i being Integer holds (i + 1) '*' a = (i '*' a) + a
Lm6:
for R being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for a being Element of R
for i being Integer holds (i - 1) '*' a = (i '*' a) - a
Lm7:
for R being Ring
for S being b1 -isomorphic Ring
for f being Isomorphism of R,S holds
( f " is additive & f " is multiplicative & f " is unity-preserving & f " is isomorphism )
Lm8:
for i being Integer holds i '*' (1. INT.Ring) = i
Lm9:
for n being Nat holds n '*' (1. F_Complex) = n
Lm10:
for F being Field
for x being Element of (PrimeField F) holds x is Element of F
Lm11:
for F being Field
for a, b being Element of F
for x, y being Element of (PrimeField F) st a = x & b = y holds
a + b = x + y
Lm12:
for F being Field
for a, b being Element of F
for x, y being Element of (PrimeField F) st a = x & b = y holds
a * b = x * y
Lm13:
for F being Field
for K being Subfield of F holds carrier/\ F c= the carrier of K
Lm14:
for p being Prime
for F being Field
for x being Element of (Z/ p)
for y being Element of INT.Ring st x = y holds
(canHom_Z/ (p,F)) . x = y '*' (1. F)