mplidomlem

	Ref	Expression
Hypotheses	mplidom.p	$⊢ P = I mPoly R$
	mplidom.i	$⊢ φ \to I \in Fin$
	mplidom.r	$⊢ φ \to R \in IDomn$
	mplidomlem.j	$⊢ H = (f \in C ⟼ (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ ((j \cup \{x\}) selectVars R) (\{x\}) (f) (\{⟨x, n (\emptyset)⟩\})))$
	mplidomlem.c	$⊢ C = {Base}_{S}$
	mplidomlem.s	$⊢ S = (j \cup \{x\}) mPoly R$
	mplidomlem.u	$⊢ U = ((j \cup \{x\}) ∖ \{x\}) mPoly R$
	mplidomlem.q	$⊢ Q = {Poly}_{1} (U)$
Assertion	mplidomlem	$⊢ φ \to P \in IDomn$

Proof

Step	Hyp	Ref	Expression
1		mplidom.p	$⊢ P = I mPoly R$
2		mplidom.i	$⊢ φ \to I \in Fin$
3		mplidom.r	$⊢ φ \to R \in IDomn$
4		mplidomlem.j	$⊢ H = (f \in C ⟼ (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ ((j \cup \{x\}) selectVars R) (\{x\}) (f) (\{⟨x, n (\emptyset)⟩\})))$
5		mplidomlem.c	$⊢ C = {Base}_{S}$
6		mplidomlem.s	$⊢ S = (j \cup \{x\}) mPoly R$
7		mplidomlem.u	$⊢ U = ((j \cup \{x\}) ∖ \{x\}) mPoly R$
8		mplidomlem.q	$⊢ Q = {Poly}_{1} (U)$
9		oveq1	$⊢ i = \emptyset \to i mPoly R = \emptyset mPoly R$
10	9	eleq1d	$⊢ i = \emptyset \to (i mPoly R \in IDomn \leftrightarrow \emptyset mPoly R \in IDomn)$
11		oveq1	$⊢ i = j \to i mPoly R = j mPoly R$
12	11	eleq1d	$⊢ i = j \to (i mPoly R \in IDomn \leftrightarrow j mPoly R \in IDomn)$
13		oveq1	$⊢ i = j \cup \{x\} \to i mPoly R = (j \cup \{x\}) mPoly R$
14	13 6	eqtr4di	$⊢ i = j \cup \{x\} \to i mPoly R = S$
15	14	eleq1d	$⊢ i = j \cup \{x\} \to (i mPoly R \in IDomn \leftrightarrow S \in IDomn)$
16		oveq1	$⊢ i = I \to i mPoly R = I mPoly R$
17	16	eleq1d	$⊢ i = I \to (i mPoly R \in IDomn \leftrightarrow I mPoly R \in IDomn)$
18		eqid	$⊢ \emptyset mPoly R = \emptyset mPoly R$
19		0ex	$⊢ \emptyset \in V$
20	19	a1i	$⊢ φ \to \emptyset \in V$
21	3	idomcringd	$⊢ φ \to R \in CRing$
22	18 20 21	mplcrngd	$⊢ φ \to \emptyset mPoly R \in CRing$
23		eqid	$⊢ {Base}_{(\emptyset mPoly R)} = {Base}_{(\emptyset mPoly R)}$
24	3	idomringd	$⊢ φ \to R \in Ring$
25	23 18 24	0mplric	$⊢ φ \to (\emptyset mPoly R) ≃_{𝑟} R$
26	3	idomdomd	$⊢ φ \to R \in Domn$
27		ricdomn	$⊢ (\emptyset mPoly R) ≃_{𝑟} R \to (\emptyset mPoly R \in Domn \leftrightarrow R \in Domn)$
28	27	biimpar	$⊢ ((\emptyset mPoly R) ≃_{𝑟} R \land R \in Domn) \to \emptyset mPoly R \in Domn$
29	25 26 28	syl2anc	$⊢ φ \to \emptyset mPoly R \in Domn$
30		isidom	$⊢ \emptyset mPoly R \in IDomn \leftrightarrow (\emptyset mPoly R \in CRing \land \emptyset mPoly R \in Domn)$
31	22 29 30	sylanbrc	$⊢ φ \to \emptyset mPoly R \in IDomn$
32	2	ad3antrrr	$⊢ (((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \to I \in Fin$
33		simpllr	$⊢ (((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \to j \subseteq I$
34	32 33	ssfid	$⊢ (((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \to j \in Fin$
35		snfi	$⊢ \{x\} \in Fin$
36	35	a1i	$⊢ (((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \to \{x\} \in Fin$
37	34 36	unfid	$⊢ (((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \to j \cup \{x\} \in Fin$
38	21	ad3antrrr	$⊢ (((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \to R \in CRing$
39	6 37 38	mplcrngd	$⊢ (((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \to S \in CRing$
40		domnnzr	$⊢ R \in Domn \to R \in NzRing$
41	26 40	syl	$⊢ φ \to R \in NzRing$
42	41	ad3antrrr	$⊢ (((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \to R \in NzRing$
43	6 37 42	mplnzr	$⊢ (((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \to S \in NzRing$
44	37	ad4antr	$⊢ (((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \land H (p) = 0_{Q}) \to j \cup \{x\} \in Fin$
45		vsnid	$⊢ x \in \{x\}$
46		elun2	$⊢ x \in \{x\} \to x \in (j \cup \{x\})$
47	45 46	ax-mp	$⊢ x \in (j \cup \{x\})$
48	47	a1i	$⊢ (((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \land H (p) = 0_{Q}) \to x \in (j \cup \{x\})$
49	38	ad4antr	$⊢ (((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \land H (p) = 0_{Q}) \to R \in CRing$
50		eqid	$⊢ 0_{Q} = 0_{Q}$
51		eqid	$⊢ 0_{S} = 0_{S}$
52		simp-4r	$⊢ (((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \land H (p) = 0_{Q}) \to p \in C$
53		simpr	$⊢ (((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \land H (p) = 0_{Q}) \to H (p) = 0_{Q}$
54	5 6 7 8 4 44 48 49 50 51 52 53	selvply1rhm0	$⊢ (((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \land H (p) = 0_{Q}) \to p = 0_{S}$
55	37	ad4antr	$⊢ (((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \land H (q) = 0_{Q}) \to j \cup \{x\} \in Fin$
56	47	a1i	$⊢ (((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \land H (q) = 0_{Q}) \to x \in (j \cup \{x\})$
57	38	ad4antr	$⊢ (((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \land H (q) = 0_{Q}) \to R \in CRing$
58		simpllr	$⊢ (((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \land H (q) = 0_{Q}) \to q \in C$
59		simpr	$⊢ (((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \land H (q) = 0_{Q}) \to H (q) = 0_{Q}$
60	5 6 7 8 4 55 56 57 50 51 58 59	selvply1rhm0	$⊢ (((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \land H (q) = 0_{Q}) \to q = 0_{S}$
61		simp-5r	$⊢ ((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \to x \in (I ∖ j)$
62	61	eldifbd	$⊢ ((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \to \neg x \in j$
63		disjsn	$⊢ j \cap \{x\} = \emptyset \leftrightarrow \neg x \in j$
64	62 63	sylibr	$⊢ ((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \to j \cap \{x\} = \emptyset$
65		undif5	$⊢ j \cap \{x\} = \emptyset \to (j \cup \{x\}) ∖ \{x\} = j$
66	64 65	syl	$⊢ ((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \to (j \cup \{x\}) ∖ \{x\} = j$
67	66	oveq1d	$⊢ ((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \to ((j \cup \{x\}) ∖ \{x\}) mPoly R = j mPoly R$
68	7 67	eqtrid	$⊢ ((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \to U = j mPoly R$
69		simp-4r	$⊢ ((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \to j mPoly R \in IDomn$
70	69	idomdomd	$⊢ ((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \to j mPoly R \in Domn$
71	68 70	eqeltrd	$⊢ ((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \to U \in Domn$
72	8	ply1domn	$⊢ U \in Domn \to Q \in Domn$
73	71 72	syl	$⊢ ((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \to Q \in Domn$
74	47	a1i	$⊢ (((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \to x \in (j \cup \{x\})$
75	5 6 7 8 4 37 74 38	selvply1rhm	$⊢ (((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \to H \in (S RingHom Q)$
76	75	ad3antrrr	$⊢ ((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \to H \in (S RingHom Q)$
77		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
78	5 77	rhmf	$⊢ H \in (S RingHom Q) \to H : C ⟶ {Base}_{Q}$
79	76 78	syl	$⊢ ((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \to H : C ⟶ {Base}_{Q}$
80		simpllr	$⊢ ((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \to p \in C$
81	79 80	ffvelcdmd	$⊢ ((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \to H (p) \in {Base}_{Q}$
82		simplr	$⊢ ((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \to q \in C$
83	79 82	ffvelcdmd	$⊢ ((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \to H (q) \in {Base}_{Q}$
84		simpr	$⊢ ((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \to p \cdot_{S} q = 0_{S}$
85	84	fveq2d	$⊢ ((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \to H (p \cdot_{S} q) = H (0_{S})$
86		eqid	$⊢ \cdot_{S} = \cdot_{S}$
87		eqid	$⊢ \cdot_{Q} = \cdot_{Q}$
88	5 86 87	rhmmul	$⊢ (H \in (S RingHom Q) \land p \in C \land q \in C) \to H (p \cdot_{S} q) = H (p) \cdot_{Q} H (q)$
89	76 80 82 88	syl3anc	$⊢ ((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \to H (p \cdot_{S} q) = H (p) \cdot_{Q} H (q)$
90		rhmghm	$⊢ H \in (S RingHom Q) \to H \in (S GrpHom Q)$
91	51 50	ghmid	$⊢ H \in (S GrpHom Q) \to H (0_{S}) = 0_{Q}$
92	76 90 91	3syl	$⊢ ((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \to H (0_{S}) = 0_{Q}$
93	85 89 92	3eqtr3d	$⊢ ((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \to H (p) \cdot_{Q} H (q) = 0_{Q}$
94	77 87 50	domneq0	$⊢ (Q \in Domn \land H (p) \in {Base}_{Q} \land H (q) \in {Base}_{Q}) \to (H (p) \cdot_{Q} H (q) = 0_{Q} \leftrightarrow (H (p) = 0_{Q} \lor H (q) = 0_{Q}))$
95	94	biimpa	$⊢ ((Q \in Domn \land H (p) \in {Base}_{Q} \land H (q) \in {Base}_{Q}) \land H (p) \cdot_{Q} H (q) = 0_{Q}) \to (H (p) = 0_{Q} \lor H (q) = 0_{Q})$
96	73 81 83 93 95	syl31anc	$⊢ ((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \to (H (p) = 0_{Q} \lor H (q) = 0_{Q})$
97	54 60 96	orim12da	$⊢ ((((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \land p \cdot_{S} q = 0_{S}) \to (p = 0_{S} \lor q = 0_{S})$
98	97	ex	$⊢ (((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land p \in C) \land q \in C) \to (p \cdot_{S} q = 0_{S} \to (p = 0_{S} \lor q = 0_{S}))$
99	98	anasss	$⊢ ((((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \land (p \in C \land q \in C)) \to (p \cdot_{S} q = 0_{S} \to (p = 0_{S} \lor q = 0_{S}))$
100	99	ralrimivva	$⊢ (((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \to \forall p \in C \forall q \in C (p \cdot_{S} q = 0_{S} \to (p = 0_{S} \lor q = 0_{S}))$
101	5 86 51	isdomn	$⊢ S \in Domn \leftrightarrow (S \in NzRing \land \forall p \in C \forall q \in C (p \cdot_{S} q = 0_{S} \to (p = 0_{S} \lor q = 0_{S})))$
102	43 100 101	sylanbrc	$⊢ (((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \to S \in Domn$
103		isidom	$⊢ S \in IDomn \leftrightarrow (S \in CRing \land S \in Domn)$
104	39 102 103	sylanbrc	$⊢ (((φ \land j \subseteq I) \land x \in (I ∖ j)) \land j mPoly R \in IDomn) \to S \in IDomn$
105	104	ex	$⊢ ((φ \land j \subseteq I) \land x \in (I ∖ j)) \to (j mPoly R \in IDomn \to S \in IDomn)$
106	105	anasss	$⊢ (φ \land (j \subseteq I \land x \in (I ∖ j))) \to (j mPoly R \in IDomn \to S \in IDomn)$
107	10 12 15 17 31 106 2	findcard2d	$⊢ φ \to I mPoly R \in IDomn$
108	1 107	eqeltrid	$⊢ φ \to P \in IDomn$

Metamath Proof Explorer

Theorem mplidomlem

Proof