aks6d1c5

	Ref	Expression
Hypotheses	aks6d1p5.1	$⊢ φ \to K \in Field$
	aks6d1p5.2	$⊢ φ \to P \in ℙ$
	aks6d1c5.3	$⊢ P = chr (K)$
	aks6d1c5.4	$⊢ φ \to A \in ℕ_{0}$
	aks6d1c5.5	$⊢ φ \to A < P$
	aks6d1c5.6	$⊢ X = {var}_{1} (K)$
	aks6d1c5.7	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{{Poly}_{1} (K)}}$
	aks6d1c5.8	$⊢ G = (g \in ({ℕ_{0}}^{(0 \dots A)}) ⟼ {\sum_{{mulGrp}_{{Poly}_{1} (K)}}}_{i = 0}^{A} (g (i) \underset{˙}{\times} (X +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (i)))))$
Assertion	aks6d1c5	$⊢ φ \to G : {ℕ_{0}}^{(0 \dots A)} \underset{1-1}{⟶} {Base}_{{Poly}_{1} (K)}$

Proof

Step	Hyp	Ref	Expression
1		aks6d1p5.1	$⊢ φ \to K \in Field$
2		aks6d1p5.2	$⊢ φ \to P \in ℙ$
3		aks6d1c5.3	$⊢ P = chr (K)$
4		aks6d1c5.4	$⊢ φ \to A \in ℕ_{0}$
5		aks6d1c5.5	$⊢ φ \to A < P$
6		aks6d1c5.6	$⊢ X = {var}_{1} (K)$
7		aks6d1c5.7	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{{Poly}_{1} (K)}}$
8		aks6d1c5.8	$⊢ G = (g \in ({ℕ_{0}}^{(0 \dots A)}) ⟼ {\sum_{{mulGrp}_{{Poly}_{1} (K)}}}_{i = 0}^{A} (g (i) \underset{˙}{\times} (X +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (i)))))$
9		eqid	$⊢ {Base}_{{mulGrp}_{{Poly}_{1} (K)}} = {Base}_{{mulGrp}_{{Poly}_{1} (K)}}$
10	1	fldcrngd	$⊢ φ \to K \in CRing$
11		eqid	$⊢ {Poly}_{1} (K) = {Poly}_{1} (K)$
12	11	ply1crng	$⊢ K \in CRing \to {Poly}_{1} (K) \in CRing$
13	10 12	syl	$⊢ φ \to {Poly}_{1} (K) \in CRing$
14		eqid	$⊢ {mulGrp}_{{Poly}_{1} (K)} = {mulGrp}_{{Poly}_{1} (K)}$
15	14	crngmgp	$⊢ {Poly}_{1} (K) \in CRing \to {mulGrp}_{{Poly}_{1} (K)} \in CMnd$
16	13 15	syl	$⊢ φ \to {mulGrp}_{{Poly}_{1} (K)} \in CMnd$
17	16	adantr	$⊢ (φ \land g \in ({ℕ_{0}}^{(0 \dots A)})) \to {mulGrp}_{{Poly}_{1} (K)} \in CMnd$
18		fzfid	$⊢ (φ \land g \in ({ℕ_{0}}^{(0 \dots A)})) \to (0 \dots A) \in Fin$
19	17	cmnmndd	$⊢ (φ \land g \in ({ℕ_{0}}^{(0 \dots A)})) \to {mulGrp}_{{Poly}_{1} (K)} \in Mnd$
20	19	adantr	$⊢ ((φ \land g \in ({ℕ_{0}}^{(0 \dots A)})) \land i \in (0 \dots A)) \to {mulGrp}_{{Poly}_{1} (K)} \in Mnd$
21		nn0ex	$⊢ ℕ_{0} \in V$
22	21	a1i	$⊢ φ \to ℕ_{0} \in V$
23		ovexd	$⊢ φ \to (0 \dots A) \in V$
24	22 23	elmapd	$⊢ φ \to (g \in ({ℕ_{0}}^{(0 \dots A)}) \leftrightarrow g : (0 \dots A) ⟶ ℕ_{0})$
25	24	biimpd	$⊢ φ \to (g \in ({ℕ_{0}}^{(0 \dots A)}) \to g : (0 \dots A) ⟶ ℕ_{0})$
26	25	imp	$⊢ (φ \land g \in ({ℕ_{0}}^{(0 \dots A)})) \to g : (0 \dots A) ⟶ ℕ_{0}$
27	26	ffvelcdmda	$⊢ ((φ \land g \in ({ℕ_{0}}^{(0 \dots A)})) \land i \in (0 \dots A)) \to g (i) \in ℕ_{0}$
28	13	crngringd	$⊢ φ \to {Poly}_{1} (K) \in Ring$
29	28	ringcmnd	$⊢ φ \to {Poly}_{1} (K) \in CMnd$
30		cmnmnd	$⊢ {Poly}_{1} (K) \in CMnd \to {Poly}_{1} (K) \in Mnd$
31	29 30	syl	$⊢ φ \to {Poly}_{1} (K) \in Mnd$
32	31	adantr	$⊢ (φ \land g \in ({ℕ_{0}}^{(0 \dots A)})) \to {Poly}_{1} (K) \in Mnd$
33	32	adantr	$⊢ ((φ \land g \in ({ℕ_{0}}^{(0 \dots A)})) \land i \in (0 \dots A)) \to {Poly}_{1} (K) \in Mnd$
34	10	crngringd	$⊢ φ \to K \in Ring$
35	34	adantr	$⊢ (φ \land g \in ({ℕ_{0}}^{(0 \dots A)})) \to K \in Ring$
36	35	adantr	$⊢ ((φ \land g \in ({ℕ_{0}}^{(0 \dots A)})) \land i \in (0 \dots A)) \to K \in Ring$
37		eqid	$⊢ {Base}_{{Poly}_{1} (K)} = {Base}_{{Poly}_{1} (K)}$
38	6 11 37	vr1cl	$⊢ K \in Ring \to X \in {Base}_{{Poly}_{1} (K)}$
39	36 38	syl	$⊢ ((φ \land g \in ({ℕ_{0}}^{(0 \dots A)})) \land i \in (0 \dots A)) \to X \in {Base}_{{Poly}_{1} (K)}$
40		simpl	$⊢ ((φ \land g \in ({ℕ_{0}}^{(0 \dots A)})) \land i \in (0 \dots A)) \to (φ \land g \in ({ℕ_{0}}^{(0 \dots A)}))$
41		elfzelz	$⊢ i \in (0 \dots A) \to i \in ℤ$
42	41	adantl	$⊢ ((φ \land g \in ({ℕ_{0}}^{(0 \dots A)})) \land i \in (0 \dots A)) \to i \in ℤ$
43	40 42	jca	$⊢ ((φ \land g \in ({ℕ_{0}}^{(0 \dots A)})) \land i \in (0 \dots A)) \to ((φ \land g \in ({ℕ_{0}}^{(0 \dots A)})) \land i \in ℤ)$
44		eqid	$⊢ ℤRHom (K) = ℤRHom (K)$
45	44	zrhrhm	$⊢ K \in Ring \to ℤRHom (K) \in (ℤ_{ring} RingHom K)$
46		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
47		eqid	$⊢ {Base}_{K} = {Base}_{K}$
48	46 47	rhmf	$⊢ ℤRHom (K) \in (ℤ_{ring} RingHom K) \to ℤRHom (K) : ℤ ⟶ {Base}_{K}$
49	45 48	syl	$⊢ K \in Ring \to ℤRHom (K) : ℤ ⟶ {Base}_{K}$
50	35 49	syl	$⊢ (φ \land g \in ({ℕ_{0}}^{(0 \dots A)})) \to ℤRHom (K) : ℤ ⟶ {Base}_{K}$
51	50	ffvelcdmda	$⊢ ((φ \land g \in ({ℕ_{0}}^{(0 \dots A)})) \land i \in ℤ) \to ℤRHom (K) (i) \in {Base}_{K}$
52	43 51	syl	$⊢ ((φ \land g \in ({ℕ_{0}}^{(0 \dots A)})) \land i \in (0 \dots A)) \to ℤRHom (K) (i) \in {Base}_{K}$
53		eqid	$⊢ algSc ({Poly}_{1} (K)) = algSc ({Poly}_{1} (K))$
54	11 53 47 37	ply1sclcl	$⊢ (K \in Ring \land ℤRHom (K) (i) \in {Base}_{K}) \to algSc ({Poly}_{1} (K)) (ℤRHom (K) (i)) \in {Base}_{{Poly}_{1} (K)}$
55	36 52 54	syl2anc	$⊢ ((φ \land g \in ({ℕ_{0}}^{(0 \dots A)})) \land i \in (0 \dots A)) \to algSc ({Poly}_{1} (K)) (ℤRHom (K) (i)) \in {Base}_{{Poly}_{1} (K)}$
56		eqid	$⊢ +_{{Poly}_{1} (K)} = +_{{Poly}_{1} (K)}$
57	37 56	mndcl	$⊢ ({Poly}_{1} (K) \in Mnd \land X \in {Base}_{{Poly}_{1} (K)} \land algSc ({Poly}_{1} (K)) (ℤRHom (K) (i)) \in {Base}_{{Poly}_{1} (K)}) \to X +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (i)) \in {Base}_{{Poly}_{1} (K)}$
58	33 39 55 57	syl3anc	$⊢ ((φ \land g \in ({ℕ_{0}}^{(0 \dots A)})) \land i \in (0 \dots A)) \to X +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (i)) \in {Base}_{{Poly}_{1} (K)}$
59	14 37	mgpbas	$⊢ {Base}_{{Poly}_{1} (K)} = {Base}_{{mulGrp}_{{Poly}_{1} (K)}}$
60	59	a1i	$⊢ ((φ \land g \in ({ℕ_{0}}^{(0 \dots A)})) \land i \in (0 \dots A)) \to {Base}_{{Poly}_{1} (K)} = {Base}_{{mulGrp}_{{Poly}_{1} (K)}}$
61	58 60	eleqtrd	$⊢ ((φ \land g \in ({ℕ_{0}}^{(0 \dots A)})) \land i \in (0 \dots A)) \to X +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (i)) \in {Base}_{{mulGrp}_{{Poly}_{1} (K)}}$
62	9 7 20 27 61	mulgnn0cld	$⊢ ((φ \land g \in ({ℕ_{0}}^{(0 \dots A)})) \land i \in (0 \dots A)) \to g (i) \underset{˙}{\times} (X +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (i))) \in {Base}_{{mulGrp}_{{Poly}_{1} (K)}}$
63	62	ralrimiva	$⊢ (φ \land g \in ({ℕ_{0}}^{(0 \dots A)})) \to \forall i \in (0 \dots A) g (i) \underset{˙}{\times} (X +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (i))) \in {Base}_{{mulGrp}_{{Poly}_{1} (K)}}$
64	9 17 18 63	gsummptcl	$⊢ (φ \land g \in ({ℕ_{0}}^{(0 \dots A)})) \to {\sum_{{mulGrp}_{{Poly}_{1} (K)}}}_{i = 0}^{A} (g (i) \underset{˙}{\times} (X +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (i)))) \in {Base}_{{mulGrp}_{{Poly}_{1} (K)}}$
65	59	eqcomi	$⊢ {Base}_{{mulGrp}_{{Poly}_{1} (K)}} = {Base}_{{Poly}_{1} (K)}$
66	65	a1i	$⊢ (φ \land g \in ({ℕ_{0}}^{(0 \dots A)})) \to {Base}_{{mulGrp}_{{Poly}_{1} (K)}} = {Base}_{{Poly}_{1} (K)}$
67	64 66	eleqtrd	$⊢ (φ \land g \in ({ℕ_{0}}^{(0 \dots A)})) \to {\sum_{{mulGrp}_{{Poly}_{1} (K)}}}_{i = 0}^{A} (g (i) \underset{˙}{\times} (X +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (i)))) \in {Base}_{{Poly}_{1} (K)}$
68	67 8	fmptd	$⊢ φ \to G : {ℕ_{0}}^{(0 \dots A)} ⟶ {Base}_{{Poly}_{1} (K)}$
69		eqidd	$⊢ ((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \to 0_{K} = 0_{K}$
70		simpr	$⊢ ((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \to x \neq y$
71	70	neneqd	$⊢ ((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \to \neg x = y$
72		simp-4r	$⊢ ((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \to x \in ({ℕ_{0}}^{(0 \dots A)})$
73	21	a1i	$⊢ ((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \to ℕ_{0} \in V$
74		ovexd	$⊢ ((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \to (0 \dots A) \in V$
75	73 74	elmapd	$⊢ ((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \to (x \in ({ℕ_{0}}^{(0 \dots A)}) \leftrightarrow x : (0 \dots A) ⟶ ℕ_{0})$
76	72 75	mpbid	$⊢ ((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \to x : (0 \dots A) ⟶ ℕ_{0}$
77		ffn	$⊢ x : (0 \dots A) ⟶ ℕ_{0} \to x Fn (0 \dots A)$
78	76 77	syl	$⊢ ((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \to x Fn (0 \dots A)$
79		simpllr	$⊢ ((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \to y \in ({ℕ_{0}}^{(0 \dots A)})$
80	73 74	elmapd	$⊢ ((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \to (y \in ({ℕ_{0}}^{(0 \dots A)}) \leftrightarrow y : (0 \dots A) ⟶ ℕ_{0})$
81	79 80	mpbid	$⊢ ((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \to y : (0 \dots A) ⟶ ℕ_{0}$
82		ffn	$⊢ y : (0 \dots A) ⟶ ℕ_{0} \to y Fn (0 \dots A)$
83	81 82	syl	$⊢ ((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \to y Fn (0 \dots A)$
84		eqfnfv2	$⊢ (x Fn (0 \dots A) \land y Fn (0 \dots A)) \to (x = y \leftrightarrow ((0 \dots A) = (0 \dots A) \land \forall z \in (0 \dots A) x (z) = y (z)))$
85	78 83 84	syl2anc	$⊢ ((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \to (x = y \leftrightarrow ((0 \dots A) = (0 \dots A) \land \forall z \in (0 \dots A) x (z) = y (z)))$
86	85	notbid	$⊢ ((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \to (\neg x = y \leftrightarrow \neg ((0 \dots A) = (0 \dots A) \land \forall z \in (0 \dots A) x (z) = y (z)))$
87	86	biimpd	$⊢ ((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \to (\neg x = y \to \neg ((0 \dots A) = (0 \dots A) \land \forall z \in (0 \dots A) x (z) = y (z)))$
88	71 87	mpd	$⊢ ((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \to \neg ((0 \dots A) = (0 \dots A) \land \forall z \in (0 \dots A) x (z) = y (z))$
89		ianor	$⊢ \neg ((0 \dots A) = (0 \dots A) \land \forall z \in (0 \dots A) x (z) = y (z)) \leftrightarrow (\neg (0 \dots A) = (0 \dots A) \lor \neg \forall z \in (0 \dots A) x (z) = y (z))$
90	88 89	sylib	$⊢ ((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \to (\neg (0 \dots A) = (0 \dots A) \lor \neg \forall z \in (0 \dots A) x (z) = y (z))$
91		eqidd	$⊢ ((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \to (0 \dots A) = (0 \dots A)$
92	91	notnotd	$⊢ ((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \to \neg \neg (0 \dots A) = (0 \dots A)$
93	90 92	orcnd	$⊢ ((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \to \neg \forall z \in (0 \dots A) x (z) = y (z)$
94		rexnal	$⊢ \exists z \in (0 \dots A) \neg x (z) = y (z) \leftrightarrow \neg \forall z \in (0 \dots A) x (z) = y (z)$
95	93 94	sylibr	$⊢ ((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \to \exists z \in (0 \dots A) \neg x (z) = y (z)$
96		df-ne	$⊢ x (z) \neq y (z) \leftrightarrow \neg x (z) = y (z)$
97	96	rexbii	$⊢ \exists z \in (0 \dots A) x (z) \neq y (z) \leftrightarrow \exists z \in (0 \dots A) \neg x (z) = y (z)$
98	95 97	sylibr	$⊢ ((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \to \exists z \in (0 \dots A) x (z) \neq y (z)$
99		simpl	$⊢ (((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land (z \in (0 \dots A) \land x (z) \neq y (z))) \to ((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y)$
100		simprl	$⊢ (((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land (z \in (0 \dots A) \land x (z) \neq y (z))) \to z \in (0 \dots A)$
101		simprr	$⊢ (((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land (z \in (0 \dots A) \land x (z) \neq y (z))) \to x (z) \neq y (z)$
102	99 100 101	jca31	$⊢ (((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land (z \in (0 \dots A) \land x (z) \neq y (z))) \to ((((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land z \in (0 \dots A)) \land x (z) \neq y (z))$
103	75	biimpd	$⊢ ((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \to (x \in ({ℕ_{0}}^{(0 \dots A)}) \to x : (0 \dots A) ⟶ ℕ_{0})$
104	72 103	mpd	$⊢ ((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \to x : (0 \dots A) ⟶ ℕ_{0}$
105	104	ffvelcdmda	$⊢ (((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land z \in (0 \dots A)) \to x (z) \in ℕ_{0}$
106	105	nn0red	$⊢ (((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land z \in (0 \dots A)) \to x (z) \in ℝ$
107	80	biimpd	$⊢ ((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \to (y \in ({ℕ_{0}}^{(0 \dots A)}) \to y : (0 \dots A) ⟶ ℕ_{0})$
108	79 107	mpd	$⊢ ((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \to y : (0 \dots A) ⟶ ℕ_{0}$
109	108	ffvelcdmda	$⊢ (((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land z \in (0 \dots A)) \to y (z) \in ℕ_{0}$
110	109	nn0red	$⊢ (((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land z \in (0 \dots A)) \to y (z) \in ℝ$
111	106 110	lttri2d	$⊢ (((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land z \in (0 \dots A)) \to (x (z) \neq y (z) \leftrightarrow (x (z) < y (z) \lor y (z) < x (z)))$
112	1	ad6antr	$⊢ ((((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land z \in (0 \dots A)) \land x (z) < y (z)) \to K \in Field$
113	2	ad6antr	$⊢ ((((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land z \in (0 \dots A)) \land x (z) < y (z)) \to P \in ℙ$
114	4	ad6antr	$⊢ ((((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land z \in (0 \dots A)) \land x (z) < y (z)) \to A \in ℕ_{0}$
115	5	ad6antr	$⊢ ((((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land z \in (0 \dots A)) \land x (z) < y (z)) \to A < P$
116	72	ad2antrr	$⊢ ((((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land z \in (0 \dots A)) \land x (z) < y (z)) \to x \in ({ℕ_{0}}^{(0 \dots A)})$
117	79	ad2antrr	$⊢ ((((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land z \in (0 \dots A)) \land x (z) < y (z)) \to y \in ({ℕ_{0}}^{(0 \dots A)})$
118		simp-4r	$⊢ ((((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land z \in (0 \dots A)) \land x (z) < y (z)) \to G (x) = G (y)$
119		simplr	$⊢ ((((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land z \in (0 \dots A)) \land x (z) < y (z)) \to z \in (0 \dots A)$
120		simpr	$⊢ ((((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land z \in (0 \dots A)) \land x (z) < y (z)) \to x (z) < y (z)$
121	112 113 3 114 115 6 7 8 116 117 118 119 120	aks6d1c5lem2	$⊢ ((((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land z \in (0 \dots A)) \land x (z) < y (z)) \to 0_{K} \neq 0_{K}$
122	1	ad6antr	$⊢ ((((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land z \in (0 \dots A)) \land y (z) < x (z)) \to K \in Field$
123	2	ad6antr	$⊢ ((((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land z \in (0 \dots A)) \land y (z) < x (z)) \to P \in ℙ$
124	4	ad6antr	$⊢ ((((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land z \in (0 \dots A)) \land y (z) < x (z)) \to A \in ℕ_{0}$
125	5	ad6antr	$⊢ ((((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land z \in (0 \dots A)) \land y (z) < x (z)) \to A < P$
126	79	ad2antrr	$⊢ ((((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land z \in (0 \dots A)) \land y (z) < x (z)) \to y \in ({ℕ_{0}}^{(0 \dots A)})$
127	72	ad2antrr	$⊢ ((((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land z \in (0 \dots A)) \land y (z) < x (z)) \to x \in ({ℕ_{0}}^{(0 \dots A)})$
128		simp-4r	$⊢ ((((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land z \in (0 \dots A)) \land y (z) < x (z)) \to G (x) = G (y)$
129	128	eqcomd	$⊢ ((((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land z \in (0 \dots A)) \land y (z) < x (z)) \to G (y) = G (x)$
130		simplr	$⊢ ((((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land z \in (0 \dots A)) \land y (z) < x (z)) \to z \in (0 \dots A)$
131		simpr	$⊢ ((((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land z \in (0 \dots A)) \land y (z) < x (z)) \to y (z) < x (z)$
132	122 123 3 124 125 6 7 8 126 127 129 130 131	aks6d1c5lem2	$⊢ ((((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land z \in (0 \dots A)) \land y (z) < x (z)) \to 0_{K} \neq 0_{K}$
133	121 132	jaodan	$⊢ ((((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land z \in (0 \dots A)) \land (x (z) < y (z) \lor y (z) < x (z))) \to 0_{K} \neq 0_{K}$
134	133	ex	$⊢ (((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land z \in (0 \dots A)) \to ((x (z) < y (z) \lor y (z) < x (z)) \to 0_{K} \neq 0_{K})$
135	111 134	sylbid	$⊢ (((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land z \in (0 \dots A)) \to (x (z) \neq y (z) \to 0_{K} \neq 0_{K})$
136	135	imp	$⊢ ((((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land z \in (0 \dots A)) \land x (z) \neq y (z)) \to 0_{K} \neq 0_{K}$
137	102 136	syl	$⊢ (((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \land (z \in (0 \dots A) \land x (z) \neq y (z))) \to 0_{K} \neq 0_{K}$
138	98 137	rexlimddv	$⊢ ((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \to 0_{K} \neq 0_{K}$
139	138	neneqd	$⊢ ((((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \land x \neq y) \to \neg 0_{K} = 0_{K}$
140	69 139	pm2.65da	$⊢ (((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \to \neg x \neq y$
141		df-ne	$⊢ x \neq y \leftrightarrow \neg x = y$
142	141	notbii	$⊢ \neg x \neq y \leftrightarrow \neg \neg x = y$
143	140 142	sylib	$⊢ (((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \to \neg \neg x = y$
144		notnotb	$⊢ x = y \leftrightarrow \neg \neg x = y$
145	143 144	sylibr	$⊢ (((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \land G (x) = G (y)) \to x = y$
146	145	ex	$⊢ ((φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \land y \in ({ℕ_{0}}^{(0 \dots A)})) \to (G (x) = G (y) \to x = y)$
147	146	ralrimiva	$⊢ (φ \land x \in ({ℕ_{0}}^{(0 \dots A)})) \to \forall y \in ({ℕ_{0}}^{(0 \dots A)}) (G (x) = G (y) \to x = y)$
148	147	ralrimiva	$⊢ φ \to \forall x \in ({ℕ_{0}}^{(0 \dots A)}) \forall y \in ({ℕ_{0}}^{(0 \dots A)}) (G (x) = G (y) \to x = y)$
149	68 148	jca	$⊢ φ \to (G : {ℕ_{0}}^{(0 \dots A)} ⟶ {Base}_{{Poly}_{1} (K)} \land \forall x \in ({ℕ_{0}}^{(0 \dots A)}) \forall y \in ({ℕ_{0}}^{(0 \dots A)}) (G (x) = G (y) \to x = y))$
150		dff13	$⊢ G : {ℕ_{0}}^{(0 \dots A)} \underset{1-1}{⟶} {Base}_{{Poly}_{1} (K)} \leftrightarrow (G : {ℕ_{0}}^{(0 \dots A)} ⟶ {Base}_{{Poly}_{1} (K)} \land \forall x \in ({ℕ_{0}}^{(0 \dots A)}) \forall y \in ({ℕ_{0}}^{(0 \dots A)}) (G (x) = G (y) \to x = y))$
151	149 150	sylibr	$⊢ φ \to G : {ℕ_{0}}^{(0 \dots A)} \underset{1-1}{⟶} {Base}_{{Poly}_{1} (K)}$

Metamath Proof Explorer

Theorem aks6d1c5

Proof