This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mplidomlem

Description: Lemma for mplidom . (Contributed by Thierry Arnoux, 4-May-2026)

Ref Expression
Hypotheses mplidom.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
mplidom.i ⊢ ( 𝜑 → 𝐼 ∈ Fin )
mplidom.r ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
mplidomlem.j ⊢ 𝐻 = ( 𝑓 ∈ 𝐶 ↦ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( ( 𝑗 ∪ { 𝑥 } ) selectVars 𝑅 ) ‘ { 𝑥 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑥 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
mplidomlem.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
mplidomlem.s ⊢ 𝑆 = ( ( 𝑗 ∪ { 𝑥 } ) mPoly 𝑅 )
mplidomlem.u ⊢ 𝑈 = ( ( ( 𝑗 ∪ { 𝑥 } ) ∖ { 𝑥 } ) mPoly 𝑅 )
mplidomlem.q ⊢ 𝑄 = ( Poly1 ‘ 𝑈 )
Assertion mplidomlem ( 𝜑 → 𝑃 ∈ IDomn )

Proof

Step Hyp Ref Expression
1 mplidom.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2 mplidom.i ⊢ ( 𝜑 → 𝐼 ∈ Fin )
3 mplidom.r ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
4 mplidomlem.j ⊢ 𝐻 = ( 𝑓 ∈ 𝐶 ↦ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( ( 𝑗 ∪ { 𝑥 } ) selectVars 𝑅 ) ‘ { 𝑥 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑥 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
5 mplidomlem.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
6 mplidomlem.s ⊢ 𝑆 = ( ( 𝑗 ∪ { 𝑥 } ) mPoly 𝑅 )
7 mplidomlem.u ⊢ 𝑈 = ( ( ( 𝑗 ∪ { 𝑥 } ) ∖ { 𝑥 } ) mPoly 𝑅 )
8 mplidomlem.q ⊢ 𝑄 = ( Poly1 ‘ 𝑈 )
9 oveq1 ⊢ ( 𝑖 = ∅ → ( 𝑖 mPoly 𝑅 ) = ( ∅ mPoly 𝑅 ) )
10 9 eleq1d ⊢ ( 𝑖 = ∅ → ( ( 𝑖 mPoly 𝑅 ) ∈ IDomn ↔ ( ∅ mPoly 𝑅 ) ∈ IDomn ) )
11 oveq1 ⊢ ( 𝑖 = 𝑗 → ( 𝑖 mPoly 𝑅 ) = ( 𝑗 mPoly 𝑅 ) )
12 11 eleq1d ⊢ ( 𝑖 = 𝑗 → ( ( 𝑖 mPoly 𝑅 ) ∈ IDomn ↔ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) )
13 oveq1 ⊢ ( 𝑖 = ( 𝑗 ∪ { 𝑥 } ) → ( 𝑖 mPoly 𝑅 ) = ( ( 𝑗 ∪ { 𝑥 } ) mPoly 𝑅 ) )
14 13 6 eqtr4di ⊢ ( 𝑖 = ( 𝑗 ∪ { 𝑥 } ) → ( 𝑖 mPoly 𝑅 ) = 𝑆 )
15 14 eleq1d ⊢ ( 𝑖 = ( 𝑗 ∪ { 𝑥 } ) → ( ( 𝑖 mPoly 𝑅 ) ∈ IDomn ↔ 𝑆 ∈ IDomn ) )
16 oveq1 ⊢ ( 𝑖 = 𝐼 → ( 𝑖 mPoly 𝑅 ) = ( 𝐼 mPoly 𝑅 ) )
17 16 eleq1d ⊢ ( 𝑖 = 𝐼 → ( ( 𝑖 mPoly 𝑅 ) ∈ IDomn ↔ ( 𝐼 mPoly 𝑅 ) ∈ IDomn ) )
18 eqid ⊢ ( ∅ mPoly 𝑅 ) = ( ∅ mPoly 𝑅 )
19 0ex ⊢ ∅ ∈ V
20 19 a1i ⊢ ( 𝜑 → ∅ ∈ V )
21 3 idomcringd ⊢ ( 𝜑 → 𝑅 ∈ CRing )
22 18 20 21 mplcrngd ⊢ ( 𝜑 → ( ∅ mPoly 𝑅 ) ∈ CRing )
23 eqid ⊢ ( Base ‘ ( ∅ mPoly 𝑅 ) ) = ( Base ‘ ( ∅ mPoly 𝑅 ) )
24 3 idomringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
25 23 18 24 0mplric ⊢ ( 𝜑 → ( ∅ mPoly 𝑅 ) ≃𝑟 𝑅 )
26 3 idomdomd ⊢ ( 𝜑 → 𝑅 ∈ Domn )
27 ricdomn ⊢ ( ( ∅ mPoly 𝑅 ) ≃𝑟 𝑅 → ( ( ∅ mPoly 𝑅 ) ∈ Domn ↔ 𝑅 ∈ Domn ) )
28 27 biimpar ⊢ ( ( ( ∅ mPoly 𝑅 ) ≃𝑟 𝑅 ∧ 𝑅 ∈ Domn ) → ( ∅ mPoly 𝑅 ) ∈ Domn )
29 25 26 28 syl2anc ⊢ ( 𝜑 → ( ∅ mPoly 𝑅 ) ∈ Domn )
30 isidom ⊢ ( ( ∅ mPoly 𝑅 ) ∈ IDomn ↔ ( ( ∅ mPoly 𝑅 ) ∈ CRing ∧ ( ∅ mPoly 𝑅 ) ∈ Domn ) )
31 22 29 30 sylanbrc ⊢ ( 𝜑 → ( ∅ mPoly 𝑅 ) ∈ IDomn )
32 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) → 𝐼 ∈ Fin )
33 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) → 𝑗 ⊆ 𝐼 )
34 32 33 ssfid ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) → 𝑗 ∈ Fin )
35 snfi ⊢ { 𝑥 } ∈ Fin
36 35 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) → { 𝑥 } ∈ Fin )
37 34 36 unfid ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) → ( 𝑗 ∪ { 𝑥 } ) ∈ Fin )
38 21 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) → 𝑅 ∈ CRing )
39 6 37 38 mplcrngd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) → 𝑆 ∈ CRing )
40 domnnzr ⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ NzRing )
41 26 40 syl ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
42 41 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) → 𝑅 ∈ NzRing )
43 6 37 42 mplnzr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) → 𝑆 ∈ NzRing )
44 37 ad4antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) ∧ ( 𝐻 ‘ 𝑝 ) = ( 0g ‘ 𝑄 ) ) → ( 𝑗 ∪ { 𝑥 } ) ∈ Fin )
45 vsnid ⊢ 𝑥 ∈ { 𝑥 }
46 elun2 ⊢ ( 𝑥 ∈ { 𝑥 } → 𝑥 ∈ ( 𝑗 ∪ { 𝑥 } ) )
47 45 46 ax-mp ⊢ 𝑥 ∈ ( 𝑗 ∪ { 𝑥 } )
48 47 a1i ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) ∧ ( 𝐻 ‘ 𝑝 ) = ( 0g ‘ 𝑄 ) ) → 𝑥 ∈ ( 𝑗 ∪ { 𝑥 } ) )
49 38 ad4antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) ∧ ( 𝐻 ‘ 𝑝 ) = ( 0g ‘ 𝑄 ) ) → 𝑅 ∈ CRing )
50 eqid ⊢ ( 0g ‘ 𝑄 ) = ( 0g ‘ 𝑄 )
51 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
52 simp-4r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) ∧ ( 𝐻 ‘ 𝑝 ) = ( 0g ‘ 𝑄 ) ) → 𝑝 ∈ 𝐶 )
53 simpr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) ∧ ( 𝐻 ‘ 𝑝 ) = ( 0g ‘ 𝑄 ) ) → ( 𝐻 ‘ 𝑝 ) = ( 0g ‘ 𝑄 ) )
54 5 6 7 8 4 44 48 49 50 51 52 53 selvply1rhm0 ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) ∧ ( 𝐻 ‘ 𝑝 ) = ( 0g ‘ 𝑄 ) ) → 𝑝 = ( 0g ‘ 𝑆 ) )
55 37 ad4antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) ∧ ( 𝐻 ‘ 𝑞 ) = ( 0g ‘ 𝑄 ) ) → ( 𝑗 ∪ { 𝑥 } ) ∈ Fin )
56 47 a1i ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) ∧ ( 𝐻 ‘ 𝑞 ) = ( 0g ‘ 𝑄 ) ) → 𝑥 ∈ ( 𝑗 ∪ { 𝑥 } ) )
57 38 ad4antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) ∧ ( 𝐻 ‘ 𝑞 ) = ( 0g ‘ 𝑄 ) ) → 𝑅 ∈ CRing )
58 simpllr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) ∧ ( 𝐻 ‘ 𝑞 ) = ( 0g ‘ 𝑄 ) ) → 𝑞 ∈ 𝐶 )
59 simpr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) ∧ ( 𝐻 ‘ 𝑞 ) = ( 0g ‘ 𝑄 ) ) → ( 𝐻 ‘ 𝑞 ) = ( 0g ‘ 𝑄 ) )
60 5 6 7 8 4 55 56 57 50 51 58 59 selvply1rhm0 ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) ∧ ( 𝐻 ‘ 𝑞 ) = ( 0g ‘ 𝑄 ) ) → 𝑞 = ( 0g ‘ 𝑆 ) )
61 simp-5r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) → 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) )
62 61 eldifbd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) → ¬ 𝑥 ∈ 𝑗 )
63 disjsn ⊢ ( ( 𝑗 ∩ { 𝑥 } ) = ∅ ↔ ¬ 𝑥 ∈ 𝑗 )
64 62 63 sylibr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) → ( 𝑗 ∩ { 𝑥 } ) = ∅ )
65 undif5 ⊢ ( ( 𝑗 ∩ { 𝑥 } ) = ∅ → ( ( 𝑗 ∪ { 𝑥 } ) ∖ { 𝑥 } ) = 𝑗 )
66 64 65 syl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) → ( ( 𝑗 ∪ { 𝑥 } ) ∖ { 𝑥 } ) = 𝑗 )
67 66 oveq1d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) → ( ( ( 𝑗 ∪ { 𝑥 } ) ∖ { 𝑥 } ) mPoly 𝑅 ) = ( 𝑗 mPoly 𝑅 ) )
68 7 67 eqtrid ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) → 𝑈 = ( 𝑗 mPoly 𝑅 ) )
69 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) → ( 𝑗 mPoly 𝑅 ) ∈ IDomn )
70 69 idomdomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) → ( 𝑗 mPoly 𝑅 ) ∈ Domn )
71 68 70 eqeltrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) → 𝑈 ∈ Domn )
72 8 ply1domn ⊢ ( 𝑈 ∈ Domn → 𝑄 ∈ Domn )
73 71 72 syl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) → 𝑄 ∈ Domn )
74 47 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) → 𝑥 ∈ ( 𝑗 ∪ { 𝑥 } ) )
75 5 6 7 8 4 37 74 38 selvply1rhm ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) → 𝐻 ∈ ( 𝑆 RingHom 𝑄 ) )
76 75 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) → 𝐻 ∈ ( 𝑆 RingHom 𝑄 ) )
77 eqid ⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
78 5 77 rhmf ⊢ ( 𝐻 ∈ ( 𝑆 RingHom 𝑄 ) → 𝐻 : 𝐶 ⟶ ( Base ‘ 𝑄 ) )
79 76 78 syl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) → 𝐻 : 𝐶 ⟶ ( Base ‘ 𝑄 ) )
80 simpllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) → 𝑝 ∈ 𝐶 )
81 79 80 ffvelcdmd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) → ( 𝐻 ‘ 𝑝 ) ∈ ( Base ‘ 𝑄 ) )
82 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) → 𝑞 ∈ 𝐶 )
83 79 82 ffvelcdmd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) → ( 𝐻 ‘ 𝑞 ) ∈ ( Base ‘ 𝑄 ) )
84 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) → ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) )
85 84 fveq2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) → ( 𝐻 ‘ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) ) = ( 𝐻 ‘ ( 0g ‘ 𝑆 ) ) )
86 eqid ⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
87 eqid ⊢ ( .r ‘ 𝑄 ) = ( .r ‘ 𝑄 )
88 5 86 87 rhmmul ⊢ ( ( 𝐻 ∈ ( 𝑆 RingHom 𝑄 ) ∧ 𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐶 ) → ( 𝐻 ‘ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) ) = ( ( 𝐻 ‘ 𝑝 ) ( .r ‘ 𝑄 ) ( 𝐻 ‘ 𝑞 ) ) )
89 76 80 82 88 syl3anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) → ( 𝐻 ‘ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) ) = ( ( 𝐻 ‘ 𝑝 ) ( .r ‘ 𝑄 ) ( 𝐻 ‘ 𝑞 ) ) )
90 rhmghm ⊢ ( 𝐻 ∈ ( 𝑆 RingHom 𝑄 ) → 𝐻 ∈ ( 𝑆 GrpHom 𝑄 ) )
91 51 50 ghmid ⊢ ( 𝐻 ∈ ( 𝑆 GrpHom 𝑄 ) → ( 𝐻 ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑄 ) )
92 76 90 91 3syl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) → ( 𝐻 ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑄 ) )
93 85 89 92 3eqtr3d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) → ( ( 𝐻 ‘ 𝑝 ) ( .r ‘ 𝑄 ) ( 𝐻 ‘ 𝑞 ) ) = ( 0g ‘ 𝑄 ) )
94 77 87 50 domneq0 ⊢ ( ( 𝑄 ∈ Domn ∧ ( 𝐻 ‘ 𝑝 ) ∈ ( Base ‘ 𝑄 ) ∧ ( 𝐻 ‘ 𝑞 ) ∈ ( Base ‘ 𝑄 ) ) → ( ( ( 𝐻 ‘ 𝑝 ) ( .r ‘ 𝑄 ) ( 𝐻 ‘ 𝑞 ) ) = ( 0g ‘ 𝑄 ) ↔ ( ( 𝐻 ‘ 𝑝 ) = ( 0g ‘ 𝑄 ) ∨ ( 𝐻 ‘ 𝑞 ) = ( 0g ‘ 𝑄 ) ) ) )
95 94 biimpa ⊢ ( ( ( 𝑄 ∈ Domn ∧ ( 𝐻 ‘ 𝑝 ) ∈ ( Base ‘ 𝑄 ) ∧ ( 𝐻 ‘ 𝑞 ) ∈ ( Base ‘ 𝑄 ) ) ∧ ( ( 𝐻 ‘ 𝑝 ) ( .r ‘ 𝑄 ) ( 𝐻 ‘ 𝑞 ) ) = ( 0g ‘ 𝑄 ) ) → ( ( 𝐻 ‘ 𝑝 ) = ( 0g ‘ 𝑄 ) ∨ ( 𝐻 ‘ 𝑞 ) = ( 0g ‘ 𝑄 ) ) )
96 73 81 83 93 95 syl31anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) → ( ( 𝐻 ‘ 𝑝 ) = ( 0g ‘ 𝑄 ) ∨ ( 𝐻 ‘ 𝑞 ) = ( 0g ‘ 𝑄 ) ) )
97 54 60 96 orim12da ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) ∧ ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) ) → ( 𝑝 = ( 0g ‘ 𝑆 ) ∨ 𝑞 = ( 0g ‘ 𝑆 ) ) )
98 97 ex ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑞 ∈ 𝐶 ) → ( ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) → ( 𝑝 = ( 0g ‘ 𝑆 ) ∨ 𝑞 = ( 0g ‘ 𝑆 ) ) ) )
99 98 anasss ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) ∧ ( 𝑝 ∈ 𝐶 ∧ 𝑞 ∈ 𝐶 ) ) → ( ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) → ( 𝑝 = ( 0g ‘ 𝑆 ) ∨ 𝑞 = ( 0g ‘ 𝑆 ) ) ) )
100 99 ralrimivva ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) → ∀ 𝑝 ∈ 𝐶 ∀ 𝑞 ∈ 𝐶 ( ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) → ( 𝑝 = ( 0g ‘ 𝑆 ) ∨ 𝑞 = ( 0g ‘ 𝑆 ) ) ) )
101 5 86 51 isdomn ⊢ ( 𝑆 ∈ Domn ↔ ( 𝑆 ∈ NzRing ∧ ∀ 𝑝 ∈ 𝐶 ∀ 𝑞 ∈ 𝐶 ( ( 𝑝 ( .r ‘ 𝑆 ) 𝑞 ) = ( 0g ‘ 𝑆 ) → ( 𝑝 = ( 0g ‘ 𝑆 ) ∨ 𝑞 = ( 0g ‘ 𝑆 ) ) ) ) )
102 43 100 101 sylanbrc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) → 𝑆 ∈ Domn )
103 isidom ⊢ ( 𝑆 ∈ IDomn ↔ ( 𝑆 ∈ CRing ∧ 𝑆 ∈ Domn ) )
104 39 102 103 sylanbrc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ∧ ( 𝑗 mPoly 𝑅 ) ∈ IDomn ) → 𝑆 ∈ IDomn )
105 104 ex ⊢ ( ( ( 𝜑 ∧ 𝑗 ⊆ 𝐼 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) → ( ( 𝑗 mPoly 𝑅 ) ∈ IDomn → 𝑆 ∈ IDomn ) )
106 105 anasss ⊢ ( ( 𝜑 ∧ ( 𝑗 ⊆ 𝐼 ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑗 ) ) ) → ( ( 𝑗 mPoly 𝑅 ) ∈ IDomn → 𝑆 ∈ IDomn ) )
107 10 12 15 17 31 106 2 findcard2d ⊢ ( 𝜑 → ( 𝐼 mPoly 𝑅 ) ∈ IDomn )
108 1 107 eqeltrid ⊢ ( 𝜑 → 𝑃 ∈ IDomn )