Metamath Proof Explorer

Theorem mplidomlem

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

Ref Expression
Hypotheses mplidom.p 
|- P = ( I mPoly R )
mplidom.i 
|- ( ph -> I e. Fin )
mplidom.r 
|- ( ph -> R e. IDomn )
mplidomlem.j 
|- H = ( f e. C |-> ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( ( j u. { x } ) selectVars R ) ` { x } ) ` f ) ` { <. x , ( n ` (/) ) >. } ) ) )
mplidomlem.c 
|- C = ( Base ` S )
mplidomlem.s 
|- S = ( ( j u. { x } ) mPoly R )
mplidomlem.u 
|- U = ( ( ( j u. { x } ) \ { x } ) mPoly R )
mplidomlem.q 
|- Q = ( Poly1 ` U )
Assertion mplidomlem 
|- ( ph -> P e. IDomn )

Proof

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