Theorem fprodsub 14742

Description: The "difference" (or "quotient") of two finite composites.

Hypotheses

Ref	Expression
fprodsub.1	|- X = ran G
fprodsub.2	|- D = ( /g ` G)

Assertion

Ref	Expression
fprodsub	|- ((N e. (ZZ>=` M) /\ A.k e. (M...N)(A e. X /\ B e. X) /\ G e. Abel) -> prod_k e. (M...N)G(ADB) = (prod_k e. (M...N)GADprod_k e. (M...N)GB))

Distinct variable groups:   D,k   k,G   k,M   k,N   k,X

Proof of Theorem fprodsub

Step	Hyp	Ref	Expression
1		fprodsub.1	. . . 4 |- X = ran G
2		eleq2 1958	. . . . . . . 8 |- (X = ran G -> (A e. X <-> A e. ran G))
3		eleq2 1958	. . . . . . . 8 |- (X = ran G -> (B e. X <-> B e. ran G))
4	2, 3	anbi12d 690	. . . . . . 7 |- (X = ran G -> ((A e. X /\ B e. X) <-> (A e. ran G /\ B e. ran G)))
5	4	ralbidv 2123	. . . . . 6 |- (X = ran G -> (A.k e. (M...N)(A e. X /\ B e. X) <-> A.k e. (M...N)(A e. ran G /\ B e. ran G)))
6	5	3anbi2d 1173	. . . . 5 |- (X = ran G -> ((N e. (ZZ>=` M) /\ A.k e. (M...N)(A e. X /\ B e. X) /\ G e. Abel) <-> (N e. (ZZ>=` M) /\ A.k e. (M...N)(A e. ran G /\ B e. ran G) /\ G e. Abel)))
7		fprodsub.2	. . . . . 6 |- D = ( /g ` G)
8		rneq 4186	. . . . . . . . . . . . . 14 |- (g = G -> ran g = ran G)
9	8	eleq2d 1964	. . . . . . . . . . . . 13 |- (g = G -> (A e. ran g <-> A e. ran G))
10	8	eleq2d 1964	. . . . . . . . . . . . 13 |- (g = G -> (B e. ran g <-> B e. ran G))
11	9, 10	anbi12d 690	. . . . . . . . . . . 12 |- (g = G -> ((A e. ran g /\ B e. ran g) <-> (A e. ran G /\ B e. ran G)))
12	11	ralbidv 2123	. . . . . . . . . . 11 |- (g = G -> (A.k e. (M...N)(A e. ran g /\ B e. ran g) <-> A.k e. (M...N)(A e. ran G /\ B e. ran G)))
13		fveq2 4681	. . . . . . . . . . . . 13 |- (g = G -> ( /g ` g) = ( /g ` G))
14	13	eqeq2d 1895	. . . . . . . . . . . 12 |- (g = G -> (D = ( /g ` g) <-> D = ( /g ` G)))
15		prodeq3 14663	. . . . . . . . . . . . 13 |- (g = G -> prod_k e. (M...N)g(ADB) = prod_k e. (M...N)G(ADB))
16		eqidd 1885	. . . . . . . . . . . . . 14 |- (g = G -> (M...N) = (M...N))
17		id 73	. . . . . . . . . . . . . 14 |- (g = G -> g = G)
18		eqidd 1885	. . . . . . . . . . . . . . . . 17 |- (g = G -> A = A)
19		fveq2 4681	. . . . . . . . . . . . . . . . . 18 |- (g = G -> (inv` g) = (inv` G))
20	19	fveq1d 4683	. . . . . . . . . . . . . . . . 17 |- (g = G -> ((inv` g)` B) = ((inv` G)` B))
21	17, 18, 20	opreq123d 10153	. . . . . . . . . . . . . . . 16 |- (g = G -> (Ag((inv` g)` B)) = (AG((inv` G)` B)))
22	21	adantr 425	. . . . . . . . . . . . . . 15 |- ((g = G /\ k e. (M...N)) -> (Ag((inv` g)` B)) = (AG((inv` G)` B)))
23	22	r19.21aiva 2176	. . . . . . . . . . . . . 14 |- (g = G -> A.k e. (M...N)(Ag((inv` g)` B)) = (AG((inv` G)` B)))
24		visset 2295	. . . . . . . . . . . . . 14 |- g e. _V
25	16, 17, 23, 24	prodeq123d 14665	. . . . . . . . . . . . 13 |- (g = G -> prod_k e. (M...N)g(Ag((inv` g)` B)) = prod_k e. (M...N)G(AG((inv` G)` B)))
26	15, 25	eqeq12d 1899	. . . . . . . . . . . 12 |- (g = G -> (prod_k e. (M...N)g(ADB) = prod_k e. (M...N)g(Ag((inv` g)` B)) <-> prod_k e. (M...N)G(ADB) = prod_k e. (M...N)G(AG((inv` G)` B))))
27	14, 26	imbi12d 688	. . . . . . . . . . 11 |- (g = G -> ((D = ( /g ` g) -> prod_k e. (M...N)g(ADB) = prod_k e. (M...N)g(Ag((inv` g)` B))) <-> (D = ( /g ` G) -> prod_k e. (M...N)G(ADB) = prod_k e. (M...N)G(AG((inv` G)` B)))))
28	12, 27	imbi12d 688	. . . . . . . . . 10 |- (g = G -> ((A.k e. (M...N)(A e. ran g /\ B e. ran g) -> (D = ( /g ` g) -> prod_k e. (M...N)g(ADB) = prod_k e. (M...N)g(Ag((inv` g)` B)))) <-> (A.k e. (M...N)(A e. ran G /\ B e. ran G) -> (D = ( /g ` G) -> prod_k e. (M...N)G(ADB) = prod_k e. (M...N)G(AG((inv` G)` B))))))
29	28	imbi2d 674	. . . . . . . . 9 |- (g = G -> ((N e. (ZZ>=` M) -> (A.k e. (M...N)(A e. ran g /\ B e. ran g) -> (D = ( /g ` g) -> prod_k e. (M...N)g(ADB) = prod_k e. (M...N)g(Ag((inv` g)` B))))) <-> (N e. (ZZ>=` M) -> (A.k e. (M...N)(A e. ran G /\ B e. ran G) -> (D = ( /g ` G) -> prod_k e. (M...N)G(ADB) = prod_k e. (M...N)G(AG((inv` G)` B)))))))
30		opreq 4888	. . . . . . . . . . . . . . . 16 |- (D = ( /g ` g) -> (ADB) = (A( /g ` g)B))
31	30	eqeq1d 1892	. . . . . . . . . . . . . . 15 |- (D = ( /g ` g) -> ((ADB) = (Ag((inv` g)` B)) <-> (A( /g ` g)B) = (Ag((inv` g)` B))))
32	31	ralbidv 2123	. . . . . . . . . . . . . 14 |- (D = ( /g ` g) -> (A.k e. (M...N)(ADB) = (Ag((inv` g)` B)) <-> A.k e. (M...N)(A( /g ` g)B) = (Ag((inv` g)` B))))
33		simplr 449	. . . . . . . . . . . . . . . . . . . 20 |- (((N e. (ZZ>=` M) /\ g e. Abel) /\ (A e. ran g /\ B e. ran g)) -> g e. Abel)
34		simprl 450	. . . . . . . . . . . . . . . . . . . 20 |- (((N e. (ZZ>=` M) /\ g e. Abel) /\ (A e. ran g /\ B e. ran g)) -> A e. ran g)
35		simprr 451	. . . . . . . . . . . . . . . . . . . 20 |- (((N e. (ZZ>=` M) /\ g e. Abel) /\ (A e. ran g /\ B e. ran g)) -> B e. ran g)
36		eqid 1884	. . . . . . . . . . . . . . . . . . . . . 22 |- ran g = ran g
37		eqid 1884	. . . . . . . . . . . . . . . . . . . . . 22 |- (inv` g) = (inv` g)
38		eqid 1884	. . . . . . . . . . . . . . . . . . . . . 22 |- ( /g ` g) = ( /g ` g)
39	36, 37, 38	grpdivval 9367	. . . . . . . . . . . . . . . . . . . . 21 |- ((g e. Grp /\ A e. ran g /\ B e. ran g) -> (A( /g ` g)B) = (Ag((inv` g)` B)))
40		ablgrp 9410	. . . . . . . . . . . . . . . . . . . . 21 |- (g e. Abel -> g e. Grp)
41	39, 40	syl3an1 1130	. . . . . . . . . . . . . . . . . . . 20 |- ((g e. Abel /\ A e. ran g /\ B e. ran g) -> (A( /g ` g)B) = (Ag((inv` g)` B)))
42	33, 34, 35, 41	syl111anc 1100	. . . . . . . . . . . . . . . . . . 19 |- (((N e. (ZZ>=` M) /\ g e. Abel) /\ (A e. ran g /\ B e. ran g)) -> (A( /g ` g)B) = (Ag((inv` g)` B)))
43	42	ex 402	. . . . . . . . . . . . . . . . . 18 |- ((N e. (ZZ>=` M) /\ g e. Abel) -> ((A e. ran g /\ B e. ran g) -> (A( /g ` g)B) = (Ag((inv` g)` B))))
44	43	ralimdv 2172	. . . . . . . . . . . . . . . . 17 |- ((N e. (ZZ>=` M) /\ g e. Abel) -> (A.k e. (M...N)(A e. ran g /\ B e. ran g) -> A.k e. (M...N)(A( /g ` g)B) = (Ag((inv` g)` B))))
45	44	ex 402	. . . . . . . . . . . . . . . 16 |- (N e. (ZZ>=` M) -> (g e. Abel -> (A.k e. (M...N)(A e. ran g /\ B e. ran g) -> A.k e. (M...N)(A( /g ` g)B) = (Ag((inv` g)` B)))))
46	45	com23 36	. . . . . . . . . . . . . . 15 |- (N e. (ZZ>=` M) -> (A.k e. (M...N)(A e. ran g /\ B e. ran g) -> (g e. Abel -> A.k e. (M...N)(A( /g ` g)B) = (Ag((inv` g)` B)))))
47	46	3imp 1061	. . . . . . . . . . . . . 14 |- ((N e. (ZZ>=` M) /\ A.k e. (M...N)(A e. ran g /\ B e. ran g) /\ g e. Abel) -> A.k e. (M...N)(A( /g ` g)B) = (Ag((inv` g)` B)))
48	32, 47	syl5cbir 228	. . . . . . . . . . . . 13 |- ((N e. (ZZ>=` M) /\ A.k e. (M...N)(A e. ran g /\ B e. ran g) /\ g e. Abel) -> (D = ( /g ` g) -> A.k e. (M...N)(ADB) = (Ag((inv` g)` B))))
49	48	imp 377	. . . . . . . . . . . 12 |- (((N e. (ZZ>=` M) /\ A.k e. (M...N)(A e. ran g /\ B e. ran g) /\ g e. Abel) /\ D = ( /g ` g)) -> A.k e. (M...N)(ADB) = (Ag((inv` g)` B)))
50	49, 24	prodeq3d 14668	. . . . . . . . . . 11 |- (((N e. (ZZ>=` M) /\ A.k e. (M...N)(A e. ran g /\ B e. ran g) /\ g e. Abel) /\ D = ( /g ` g)) -> prod_k e. (M...N)g(ADB) = prod_k e. (M...N)g(Ag((inv` g)` B)))
51	50	3exp1 1084	. . . . . . . . . 10 |- (N e. (ZZ>=` M) -> (A.k e. (M...N)(A e. ran g /\ B e. ran g) -> (g e. Abel -> (D = ( /g ` g) -> prod_k e. (M...N)g(ADB) = prod_k e. (M...N)g(Ag((inv` g)` B))))))
52	51	com3r 39	. . . . . . . . 9 |- (g e. Abel -> (N e. (ZZ>=` M) -> (A.k e. (M...N)(A e. ran g /\ B e. ran g) -> (D = ( /g ` g) -> prod_k e. (M...N)g(ADB) = prod_k e. (M...N)g(Ag((inv` g)` B))))))
53	29, 52	vtoclga 2352	. . . . . . . 8 |- (G e. Abel -> (N e. (ZZ>=` M) -> (A.k e. (M...N)(A e. ran G /\ B e. ran G) -> (D = ( /g ` G) -> prod_k e. (M...N)G(ADB) = prod_k e. (M...N)G(AG((inv` G)` B))))))
54	53	com3l 38	. . . . . . 7 |- (N e. (ZZ>=` M) -> (A.k e. (M...N)(A e. ran G /\ B e. ran G) -> (G e. Abel -> (D = ( /g ` G) -> prod_k e. (M...N)G(ADB) = prod_k e. (M...N)G(AG((inv` G)` B))))))
55	54	3imp 1061	. . . . . 6 |- ((N e. (ZZ>=` M) /\ A.k e. (M...N)(A e. ran G /\ B e. ran G) /\ G e. Abel) -> (D = ( /g ` G) -> prod_k e. (M...N)G(ADB) = prod_k e. (M...N)G(AG((inv` G)` B))))
56	7, 55	mpi 55	. . . . 5 |- ((N e. (ZZ>=` M) /\ A.k e. (M...N)(A e. ran G /\ B e. ran G) /\ G e. Abel) -> prod_k e. (M...N)G(ADB) = prod_k e. (M...N)G(AG((inv` G)` B)))
57	6, 56	syl6bi 231	. . . 4 |- (X = ran G -> ((N e. (ZZ>=` M) /\ A.k e. (M...N)(A e. X /\ B e. X) /\ G e. Abel) -> prod_k e. (M...N)G(ADB) = prod_k e. (M...N)G(AG((inv` G)` B))))
58	1, 57	ax-mp 7	. . 3 |- ((N e. (ZZ>=` M) /\ A.k e. (M...N)(A e. X /\ B e. X) /\ G e. Abel) -> prod_k e. (M...N)G(ADB) = prod_k e. (M...N)G(AG((inv` G)` B)))
59		simp1 876	. . . 4 |- ((N e. (ZZ>=` M) /\ A.k e. (M...N)(A e. X /\ B e. X) /\ G e. Abel) -> N e. (ZZ>=` M))
60		ablgrp 9410	. . . . . . . . . . 11 |- (G e. Abel -> G e. Grp)
61		grprndm 9334	. . . . . . . . . . . 12 |- (G e. Grp -> ran G = dom dom G)
62	61, 1	syl5eq 1940	. . . . . . . . . . 11 |- (G e. Grp -> X = dom dom G)
63	60, 62	syl 12	. . . . . . . . . 10 |- (G e. Abel -> X = dom dom G)
64	63	eleq2d 1964	. . . . . . . . 9 |- (G e. Abel -> (A e. X <-> A e. dom dom G))
65	64	biimpd 170	. . . . . . . 8 |- (G e. Abel -> (A e. X -> A e. dom dom G))
66		eqid 1884	. . . . . . . . . . . 12 |- (inv` G) = (inv` G)
67	1, 66	grpinvcl 9352	. . . . . . . . . . 11 |- ((G e. Grp /\ B e. X) -> ((inv` G)` B) e. X)
68	62	adantr 425	. . . . . . . . . . 11 |- ((G e. Grp /\ B e. X) -> X = dom dom G)
69	67, 68	eleqtrd 1973	. . . . . . . . . 10 |- ((G e. Grp /\ B e. X) -> ((inv` G)` B) e. dom dom G)
70	69	ex 402	. . . . . . . . 9 |- (G e. Grp -> (B e. X -> ((inv` G)` B) e. dom dom G))
71	60, 70	syl 12	. . . . . . . 8 |- (G e. Abel -> (B e. X -> ((inv` G)` B) e. dom dom G))
72	65, 71	anim12d 617	. . . . . . 7 |- (G e. Abel -> ((A e. X /\ B e. X) -> (A e. dom dom G /\ ((inv` G)` B) e. dom dom G)))
73	72	ralimdv 2172	. . . . . 6 |- (G e. Abel -> (A.k e. (M...N)(A e. X /\ B e. X) -> A.k e. (M...N)(A e. dom dom G /\ ((inv` G)` B) e. dom dom G)))
74	73	impcom 378	. . . . 5 |- ((A.k e. (M...N)(A e. X /\ B e. X) /\ G e. Abel) -> A.k e. (M...N)(A e. dom dom G /\ ((inv` G)` B) e. dom dom G))
75	74	3adant1 894	. . . 4 |- ((N e. (ZZ>=` M) /\ A.k e. (M...N)(A e. X /\ B e. X) /\ G e. Abel) -> A.k e. (M...N)(A e. dom dom G /\ ((inv` G)` B) e. dom dom G))
76		ablcomgrp 14702	. . . . . 6 |- (G e. Abel -> G e. (Grp i^i Com1))
77		grpmnd 10393	. . . . . . . . 9 |- (G e. Grp -> G e. Mnd)
78		mndissmgrp 10386	. . . . . . . . 9 |- (G e. Mnd -> G e. SemiGrp)
79	77, 78	syl 12	. . . . . . . 8 |- (G e. Grp -> G e. SemiGrp)
80	79	anim1i 361	. . . . . . 7 |- ((G e. Grp /\ G e. Com1) -> (G e. SemiGrp /\ G e. Com1))
81		elin 2786	. . . . . . 7 |- (G e. (Grp i^i Com1) <-> (G e. Grp /\ G e. Com1))
82		elin 2786	. . . . . . 7 |- (G e. (SemiGrp i^i Com1) <-> (G e. SemiGrp /\ G e. Com1))
83	80, 81, 82	3imtr4i 236	. . . . . 6 |- (G e. (Grp i^i Com1) -> G e. (SemiGrp i^i Com1))
84	76, 83	syl 12	. . . . 5 |- (G e. Abel -> G e. (SemiGrp i^i Com1))
85	84	3ad2ant3 899	. . . 4 |- ((N e. (ZZ>=` M) /\ A.k e. (M...N)(A e. X /\ B e. X) /\ G e. Abel) -> G e. (SemiGrp i^i Com1))
86		eqid 1884	. . . . 5 |- dom dom G = dom dom G
87	86	fprodadd 14713	. . . 4 |- ((N e. (ZZ>=` M) /\ A.k e. (M...N)(A e. dom dom G /\ ((inv` G)` B) e. dom dom G) /\ G e. (SemiGrp i^i Com1)) -> prod_k e. (M...N)G(AG((inv` G)` B)) = (prod_k e. (M...N)GAGprod_k e. (M...N)G((inv` G)` B)))
88	59, 75, 85, 87	syl111anc 1100	. . 3 |- ((N e. (ZZ>=` M) /\ A.k e. (M...N)(A e. X /\ B e. X) /\ G e. Abel) -> prod_k e. (M...N)G(AG((inv` G)` B)) = (prod_k e. (M...N)GAGprod_k e. (M...N)G((inv` G)` B)))
89	1, 66	fprodneg 14741	. . . . . 6 |- ((N e. (ZZ>=` M) /\ A.k e. (M...N)B e. X /\ G e. Abel) -> ((inv` G)` prod_k e. (M...N)GB) = prod_k e. (M...N)G((inv` G)` B))
90		simpr 350	. . . . . . 7 |- ((A e. X /\ B e. X) -> B e. X)
91	90	ralimi 2168	. . . . . 6 |- (A.k e. (M...N)(A e. X /\ B e. X) -> A.k e. (M...N)B e. X)
92	89, 91	syl3an2 1131	. . . . 5 |- ((N e. (ZZ>=` M) /\ A.k e. (M...N)(A e. X /\ B e. X) /\ G e. Abel) -> ((inv` G)` prod_k e. (M...N)GB) = prod_k e. (M...N)G((inv` G)` B))
93	92	eqcomd 1889	. . . 4 |- ((N e. (ZZ>=` M) /\ A.k e. (M...N)(A e. X /\ B e. X) /\ G e. Abel) -> prod_k e. (M...N)G((inv` G)` B) = ((inv` G)` prod_k e. (M...N)GB))
94	93	opreq2d 4898	. . 3 |- ((N e. (ZZ>=` M) /\ A.k e. (M...N)(A e. X /\ B e. X) /\ G e. Abel) -> (prod_k e. (M...N)GAGprod_k e. (M...N)G((inv` G)` B)) = (prod_k e. (M...N)GAG((inv` G)` prod_k e. (M...N)GB)))
95	58, 88, 94	3eqtrd 1929	. 2 |- ((N e. (ZZ>=` M) /\ A.k e. (M...N)(A e. X /\ B e. X) /\ G e. Abel) -> prod_k e. (M...N)G(ADB) = (prod_k e. (M...N)GAG((inv` G)` prod_k e. (M...N)GB)))
96		simp3 878	. . 3 |- ((N e. (ZZ>=` M) /\ A.k e. (M...N)(A e. X /\ B e. X) /\ G e. Abel) -> G e. Abel)
97	60, 77	syl 12	. . . . . 6 |- (G e. Abel -> G e. Mnd)
98		mndmgmid 10389	. . . . . 6 |- (G e. Mnd -> G e. (Magma i^i ExId ))
99	97, 98	syl 12	. . . . 5 |- (G e. Abel -> G e. (Magma i^i ExId ))
100	99	3ad2ant3 899	. . . 4 |- ((N e. (ZZ>=` M) /\ A.k e. (M...N)(A e. X /\ B e. X) /\ G e. Abel) -> G e. (Magma i^i ExId ))
101		simpl 346	. . . . . 6 |- ((A e. X /\ B e. X) -> A e. X)
102	101	ralimi 2168	. . . . 5 |- (A.k e. (M...N)(A e. X /\ B e. X) -> A.k e. (M...N)A e. X)
103	102	3ad2ant2 898	. . . 4 |- ((N e. (ZZ>=` M) /\ A.k e. (M...N)(A e. X /\ B e. X) /\ G e. Abel) -> A.k e. (M...N)A e. X)
104	1	clfsebsr 14709	. . . 4 |- ((N e. (ZZ>=` M) /\ G e. (Magma i^i ExId ) /\ A.k e. (M...N)A e. X) -> prod_k e. (M...N)GA e. X)
105	59, 100, 103, 104	syl111anc 1100	. . 3 |- ((N e. (ZZ>=` M) /\ A.k e. (M...N)(A e. X /\ B e. X) /\ G e. Abel) -> prod_k e. (M...N)GA e. X)
106	91	3ad2ant2 898	. . . 4 |- ((N e. (ZZ>=` M) /\ A.k e. (M...N)(A e. X /\ B e. X) /\ G e. Abel) -> A.k e. (M...N)B e. X)
107	1	clfsebsr 14709	. . . 4 |- ((N e. (ZZ>=` M) /\ G e. (Magma i^i ExId ) /\ A.k e. (M...N)B e. X) -> prod_k e. (M...N)GB e. X)
108	59, 100, 106, 107	syl111anc 1100	. . 3 |- ((N e. (ZZ>=` M) /\ A.k e. (M...N)(A e. X /\ B e. X) /\ G e. Abel) -> prod_k e. (M...N)GB e. X)
109	1, 66, 7	grpdivval 9367	. . . 4 |- ((G e. Grp /\ prod_k e. (M...N)GA e. X /\ prod_k e. (M...N)GB e. X) -> (prod_k e. (M...N)GADprod_k e. (M...N)GB) = (prod_k e. (M...N)GAG((inv` G)` prod_k e. (M...N)GB)))
110	109, 60	syl3an1 1130	. . 3 |- ((G e. Abel /\ prod_k e. (M...N)GA e. X /\ prod_k e. (M...N)GB e. X) -> (prod_k e. (M...N)GADprod_k e. (M...N)GB) = (prod_k e. (M...N)GAG((inv` G)` prod_k e. (M...N)GB)))
111	96, 105, 108, 110	syl111anc 1100	. 2 |- ((N e. (ZZ>=` M) /\ A.k e. (M...N)(A e. X /\ B e. X) /\ G e. Abel) -> (prod_k e. (M...N)GADprod_k e. (M...N)GB) = (prod_k e. (M...N)GAG((inv` G)` prod_k e. (M...N)GB)))
112	95, 111	eqtr4d 1928	1 |- ((N e. (ZZ>=` M) /\ A.k e. (M...N)(A e. X /\ B e. X) /\ G e. Abel) -> prod_k e. (M...N)G(ADB) = (prod_k e. (M...N)GADprod_k e. (M...N)GB))

Syntax hints:   -> wi 3   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  _Vcvv 2292   i^i cin 2592  dom cdm 3986  ran crn 3987  ` cfv 3998  (class class class)co 4884  ZZ>=cuz 7586  ...cfz 7637  Grpcgr 9311  invcgn 9313   /g cgs 9314  Abelcabl 9407   ExId cexid 10361  Magmacmagm 10365  SemiGrpcsem 10377  Mndcmnd 10384  prod_cprd2 14654  Com1ccm1 14687

This theorem is referenced by:  svli2 14826

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1302  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-inf2 5731

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-nel 2020  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-mpt 5006  df-1st 5020  df-2nd 5021  df-iota 5089  df-rdg 5140  df-1o 5177  df-oadd 5179  df-omul 5180  df-er 5318  df-ec 5320  df-qs 5323  df-en 5427  df-dom 5428  df-sdom 5429  df-undef 5556  df-riota 5560  df-ni 6152  df-pli 6153  df-mi 6154  df-lti 6155  df-plpq 6187  df-mpq 6188  df-enq 6189  df-nq 6190  df-plq 6191  df-mq 6192  df-rq 6193  df-ltq 6194  df-1q 6195  df-np 6238  df-1p 6239  df-plp 6240  df-mp 6241  df-ltp 6242  df-plpr 6316  df-mpr 6317  df-enr 6318  df-nr 6319  df-plr 6320  df-mr 6321  df-ltr 6322  df-0r 6323  df-1r 6324  df-m1r 6325  df-c 6392  df-0 6393  df-1 6394  df-i 6395  df-r 6396  df-plus 6397  df-mul 6398  df-lt 6399  df-sub 6511  df-neg 6513  df-pnf 6654  df-mnf 6655  df-xr 6656  df-ltxr 6657  df-le 6658  df-n 7108  df-n0 7309  df-z 7345  df-uz 7587  df-fz 7638  df-seq1 7721  df-shft 7754  df-seqz 7776  df-grp 9316  df-gid 9317  df-ginv 9318  df-gdiv 9319  df-abl 9408  df-ass 10360  df-exid 10362  df-mgm 10366  df-sgr 10378  df-mnd 10385  df-prod 14653  df-prod2 14655  df-com1 14688

Copyright terms: Public domain