Metamath Proof Explorer


Theorem zarcmplem

Description: Lemma for zarcmp . (Contributed by Thierry Arnoux, 2-Jul-2024)

Ref Expression
Hypotheses zartop.1 No typesetting found for |- S = ( Spec ` R ) with typecode |-
zartop.2 J = TopOpen S
zarcmplem.1 No typesetting found for |- V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) with typecode |-
Assertion zarcmplem R CRing J Comp

Proof

Step Hyp Ref Expression
1 zartop.1 Could not format S = ( Spec ` R ) : No typesetting found for |- S = ( Spec ` R ) with typecode |-
2 zartop.2 J = TopOpen S
3 zarcmplem.1 Could not format V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) : No typesetting found for |- V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) with typecode |-
4 crngring R CRing R Ring
5 eqid Base R = Base R
6 1 2 5 zar0ring R Ring Base R = 1 J =
7 4 6 sylan R CRing Base R = 1 J =
8 0cmp Comp
9 7 8 eqeltrdi R CRing Base R = 1 J Comp
10 1 2 zartop R CRing J Top
11 fvex LIdeal R V
12 11 mptex Could not format ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) e. _V : No typesetting found for |- ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) e. _V with typecode |-
13 3 12 eqeltri V V
14 imaexg V V V a supp 0 R V
15 13 14 mp1i R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l V a supp 0 R V
16 suppssdm a supp 0 R dom a
17 imass2 a supp 0 R dom a V a supp 0 R V dom a
18 16 17 mp1i R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l V a supp 0 R V dom a
19 3 funmpt2 Fun V
20 ssidd R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l dom a dom a
21 simpllr R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a a Base R V -1 x
22 fvexd R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a Base R V
23 13 cnvex V -1 V
24 23 imaex V -1 x V
25 24 a1i R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a V -1 x V
26 22 25 elmapd R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a a Base R V -1 x a : V -1 x Base R
27 21 26 mpbid R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a a : V -1 x Base R
28 27 fdmd R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a dom a = V -1 x
29 28 adantr R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l dom a = V -1 x
30 20 29 sseqtrd R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l dom a V -1 x
31 funimass2 Fun V dom a V -1 x V dom a x
32 19 30 31 sylancr R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l V dom a x
33 18 32 sstrd R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l V a supp 0 R x
34 15 33 elpwd R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l V a supp 0 R 𝒫 x
35 simpllr R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l finSupp 0 R a
36 35 fsuppimpd R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l a supp 0 R Fin
37 imafi Fun V a supp 0 R Fin V a supp 0 R Fin
38 19 36 37 sylancr R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l V a supp 0 R Fin
39 34 38 elind R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l V a supp 0 R 𝒫 x Fin
40 inteq y = V a supp 0 R y = V a supp 0 R
41 40 eqeq2d y = V a supp 0 R = y = V a supp 0 R
42 41 adantl R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l y = V a supp 0 R = y = V a supp 0 R
43 16 29 sseqtrid R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l a supp 0 R V -1 x
44 cnvimass V -1 x dom V
45 43 44 sstrdi R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l a supp 0 R dom V
46 intimafv Fun V a supp 0 R dom V V a supp 0 R = l a supp 0 R V l
47 19 45 46 sylancr R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l V a supp 0 R = l a supp 0 R V l
48 simplll R CRing Base R 1 x 𝒫 Clsd J x = R CRing
49 48 crngringd R CRing Base R 1 x 𝒫 Clsd J x = R Ring
50 49 ad4antr R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l R Ring
51 fvex Could not format ( PrmIdeal ` R ) e. _V : No typesetting found for |- ( PrmIdeal ` R ) e. _V with typecode |-
52 51 rabex Could not format { j e. ( PrmIdeal ` R ) | i C_ j } e. _V : No typesetting found for |- { j e. ( PrmIdeal ` R ) | i C_ j } e. _V with typecode |-
53 52 3 dmmpti dom V = LIdeal R
54 45 53 sseqtrdi R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l a supp 0 R LIdeal R
55 simp-7r R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l Base R 1
56 simpllr R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l a supp 0 R = 1 R = R a
57 eqid 0 R = 0 R
58 ringcmn R Ring R CMnd
59 4 58 syl R CRing R CMnd
60 59 ad8antr R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l a supp 0 R = R CMnd
61 24 a1i R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l a supp 0 R = V -1 x V
62 27 ad2antrr R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l a supp 0 R = a : V -1 x Base R
63 simpr R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l a supp 0 R = a supp 0 R =
64 ssidd R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l a supp 0 R =
65 63 64 eqsstrd R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l a supp 0 R = a supp 0 R
66 35 adantr R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l a supp 0 R = finSupp 0 R a
67 5 57 60 61 62 65 66 gsumres R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l a supp 0 R = R a = R a
68 res0 a =
69 68 oveq2i R a = R
70 57 gsum0 R = 0 R
71 69 70 eqtri R a = 0 R
72 67 71 eqtr3di R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l a supp 0 R = R a = 0 R
73 56 72 eqtr2d R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l a supp 0 R = 0 R = 1 R
74 eqid 1 R = 1 R
75 5 57 74 01eq0ring R Ring 0 R = 1 R Base R = 0 R
76 50 73 75 syl2an2r R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l a supp 0 R = Base R = 0 R
77 76 fveq2d R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l a supp 0 R = Base R = 0 R
78 fvex 0 R V
79 hashsng 0 R V 0 R = 1
80 78 79 ax-mp 0 R = 1
81 77 80 eqtrdi R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l a supp 0 R = Base R = 1
82 55 81 mteqand R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l a supp 0 R
83 eqid RSpan R = RSpan R
84 3 83 zarclsiin R Ring a supp 0 R LIdeal R a supp 0 R l a supp 0 R V l = V RSpan R supp 0 R a
85 50 54 82 84 syl3anc R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l l a supp 0 R V l = V RSpan R supp 0 R a
86 nfv l R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a
87 nfra1 l l V -1 x a l l
88 86 87 nfan l R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l
89 54 sselda R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l l supp 0 R a l LIdeal R
90 eqid LIdeal R = LIdeal R
91 5 90 lidlss l LIdeal R l Base R
92 89 91 syl R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l l supp 0 R a l Base R
93 92 ex R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l l supp 0 R a l Base R
94 88 93 ralrimi R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l l supp 0 R a l Base R
95 unissb supp 0 R a Base R l supp 0 R a l Base R
96 94 95 sylibr R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l supp 0 R a Base R
97 83 5 90 rspcl R Ring supp 0 R a Base R RSpan R supp 0 R a LIdeal R
98 50 96 97 syl2anc R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l RSpan R supp 0 R a LIdeal R
99 5 90 lidlss RSpan R supp 0 R a LIdeal R RSpan R supp 0 R a Base R
100 98 99 syl R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l RSpan R supp 0 R a Base R
101 83 5 74 rsp1 R Ring RSpan R 1 R = Base R
102 50 101 syl R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l RSpan R 1 R = Base R
103 27 adantr R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l a : V -1 x Base R
104 103 43 fssresd R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l a supp 0 R a : a supp 0 R Base R
105 fvex Base R V
106 ovex a supp 0 R V
107 105 106 elmap a supp 0 R a Base R supp 0 R a a supp 0 R a : a supp 0 R Base R
108 104 107 sylibr R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l a supp 0 R a Base R supp 0 R a
109 breq1 b = a supp 0 R a finSupp 0 R b finSupp 0 R a supp 0 R a
110 oveq2 b = a supp 0 R a R b = R a supp 0 R a
111 110 eqeq2d b = a supp 0 R a 1 R = R b 1 R = R a supp 0 R a
112 fveq1 b = a supp 0 R a b k = a supp 0 R a k
113 112 eleq1d b = a supp 0 R a b k k a supp 0 R a k k
114 113 ralbidv b = a supp 0 R a k supp 0 R a b k k k supp 0 R a a supp 0 R a k k
115 109 111 114 3anbi123d b = a supp 0 R a finSupp 0 R b 1 R = R b k supp 0 R a b k k finSupp 0 R a supp 0 R a 1 R = R a supp 0 R a k supp 0 R a a supp 0 R a k k
116 115 adantl R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l b = a supp 0 R a finSupp 0 R b 1 R = R b k supp 0 R a b k k finSupp 0 R a supp 0 R a 1 R = R a supp 0 R a k supp 0 R a a supp 0 R a k k
117 fvexd R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l 0 R V
118 35 117 fsuppres R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l finSupp 0 R a supp 0 R a
119 simplr R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l 1 R = R a
120 50 58 syl R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l R CMnd
121 24 a1i R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l V -1 x V
122 ssidd R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l a supp 0 R a supp 0 R
123 5 57 120 121 103 122 35 gsumres R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l R a supp 0 R a = R a
124 119 123 eqtr4d R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l 1 R = R a supp 0 R a
125 simpr R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l k supp 0 R a k supp 0 R a
126 125 fvresd R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l k supp 0 R a a supp 0 R a k = a k
127 16 28 sseqtrid R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a a supp 0 R V -1 x
128 127 sselda R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a k supp 0 R a k V -1 x
129 fveq2 l = k a l = a k
130 id l = k l = k
131 129 130 eleq12d l = k a l l a k k
132 131 adantl R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a k supp 0 R a l = k a l l a k k
133 128 132 rspcdv R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a k supp 0 R a l V -1 x a l l a k k
134 133 imp R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a k supp 0 R a l V -1 x a l l a k k
135 134 an32s R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l k supp 0 R a a k k
136 126 135 eqeltrd R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l k supp 0 R a a supp 0 R a k k
137 136 ralrimiva R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l k supp 0 R a a supp 0 R a k k
138 118 124 137 3jca R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l finSupp 0 R a supp 0 R a 1 R = R a supp 0 R a k supp 0 R a a supp 0 R a k k
139 108 116 138 rspcedvd R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l b Base R supp 0 R a finSupp 0 R b 1 R = R b k supp 0 R a b k k
140 eqid R = R
141 83 5 57 140 50 54 elrspunidl R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l 1 R RSpan R supp 0 R a b Base R supp 0 R a finSupp 0 R b 1 R = R b k supp 0 R a b k k
142 139 141 mpbird R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l 1 R RSpan R supp 0 R a
143 142 snssd R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l 1 R RSpan R supp 0 R a
144 83 90 rspssp R Ring RSpan R supp 0 R a LIdeal R 1 R RSpan R supp 0 R a RSpan R 1 R RSpan R supp 0 R a
145 50 98 143 144 syl3anc R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l RSpan R 1 R RSpan R supp 0 R a
146 102 145 eqsstrrd R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l Base R RSpan R supp 0 R a
147 100 146 eqssd R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l RSpan R supp 0 R a = Base R
148 147 fveq2d R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l V RSpan R supp 0 R a = V Base R
149 90 5 lidl1 R Ring Base R LIdeal R
150 4 149 syl R CRing Base R LIdeal R
151 3 5 zarcls1 R CRing Base R LIdeal R V Base R = Base R = Base R
152 150 151 mpdan R CRing V Base R = Base R = Base R
153 5 152 mpbiri R CRing V Base R =
154 153 ad7antr R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l V Base R =
155 148 154 eqtrd R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l V RSpan R supp 0 R a =
156 47 85 155 3eqtrrd R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l = V a supp 0 R
157 39 42 156 rspcedvd R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l y 𝒫 x Fin = y
158 157 exp41 R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l y 𝒫 x Fin = y
159 158 3imp2 R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l y 𝒫 x Fin = y
160 5 74 ringidcl R Ring 1 R Base R
161 49 160 syl R CRing Base R 1 x 𝒫 Clsd J x = 1 R Base R
162 simplr R CRing Base R 1 x 𝒫 Clsd J x = x 𝒫 Clsd J
163 eqid Could not format ( PrmIdeal ` R ) = ( PrmIdeal ` R ) : No typesetting found for |- ( PrmIdeal ` R ) = ( PrmIdeal ` R ) with typecode |-
164 1 2 163 3 zartopn Could not format ( R e. CRing -> ( J e. ( TopOn ` ( PrmIdeal ` R ) ) /\ ran V = ( Clsd ` J ) ) ) : No typesetting found for |- ( R e. CRing -> ( J e. ( TopOn ` ( PrmIdeal ` R ) ) /\ ran V = ( Clsd ` J ) ) ) with typecode |-
165 164 simprd R CRing ran V = Clsd J
166 48 165 syl R CRing Base R 1 x 𝒫 Clsd J x = ran V = Clsd J
167 166 pweqd R CRing Base R 1 x 𝒫 Clsd J x = 𝒫 ran V = 𝒫 Clsd J
168 162 167 eleqtrrd R CRing Base R 1 x 𝒫 Clsd J x = x 𝒫 ran V
169 168 elpwid R CRing Base R 1 x 𝒫 Clsd J x = x ran V
170 intimafv Fun V V -1 x dom V V V -1 x = l V -1 x V l
171 19 44 170 mp2an V V -1 x = l V -1 x V l
172 funimacnv Fun V V V -1 x = x ran V
173 19 172 ax-mp V V -1 x = x ran V
174 df-ss x ran V x ran V = x
175 174 biimpi x ran V x ran V = x
176 173 175 syl5eq x ran V V V -1 x = x
177 176 inteqd x ran V V V -1 x = x
178 171 177 eqtr3id x ran V l V -1 x V l = x
179 169 178 syl R CRing Base R 1 x 𝒫 Clsd J x = l V -1 x V l = x
180 44 a1i R CRing Base R 1 x 𝒫 Clsd J x = V -1 x dom V
181 180 53 sseqtrdi R CRing Base R 1 x 𝒫 Clsd J x = V -1 x LIdeal R
182 19 a1i R CRing Base R 1 x 𝒫 Clsd J x = Fun V
183 inteq x = x =
184 int0 = V
185 183 184 eqtrdi x = x = V
186 vn0 V
187 neeq1 x = V x V
188 186 187 mpbiri x = V x
189 185 188 syl x = x
190 189 necon2i x = x
191 190 adantl R CRing Base R 1 x 𝒫 Clsd J x = x
192 preiman0 Fun V x ran V x V -1 x
193 182 169 191 192 syl3anc R CRing Base R 1 x 𝒫 Clsd J x = V -1 x
194 3 83 zarclsiin R Ring V -1 x LIdeal R V -1 x l V -1 x V l = V RSpan R V -1 x
195 49 181 193 194 syl3anc R CRing Base R 1 x 𝒫 Clsd J x = l V -1 x V l = V RSpan R V -1 x
196 simpr R CRing Base R 1 x 𝒫 Clsd J x = x =
197 179 195 196 3eqtr3d R CRing Base R 1 x 𝒫 Clsd J x = V RSpan R V -1 x =
198 181 sselda R CRing Base R 1 x 𝒫 Clsd J x = l V -1 x l LIdeal R
199 198 91 syl R CRing Base R 1 x 𝒫 Clsd J x = l V -1 x l Base R
200 199 ralrimiva R CRing Base R 1 x 𝒫 Clsd J x = l V -1 x l Base R
201 unissb V -1 x Base R l V -1 x l Base R
202 200 201 sylibr R CRing Base R 1 x 𝒫 Clsd J x = V -1 x Base R
203 83 5 90 rspcl R Ring V -1 x Base R RSpan R V -1 x LIdeal R
204 49 202 203 syl2anc R CRing Base R 1 x 𝒫 Clsd J x = RSpan R V -1 x LIdeal R
205 3 5 zarcls1 R CRing RSpan R V -1 x LIdeal R V RSpan R V -1 x = RSpan R V -1 x = Base R
206 48 204 205 syl2anc R CRing Base R 1 x 𝒫 Clsd J x = V RSpan R V -1 x = RSpan R V -1 x = Base R
207 197 206 mpbid R CRing Base R 1 x 𝒫 Clsd J x = RSpan R V -1 x = Base R
208 161 207 eleqtrrd R CRing Base R 1 x 𝒫 Clsd J x = 1 R RSpan R V -1 x
209 83 5 57 140 49 181 elrspunidl R CRing Base R 1 x 𝒫 Clsd J x = 1 R RSpan R V -1 x a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l
210 208 209 mpbid R CRing Base R 1 x 𝒫 Clsd J x = a Base R V -1 x finSupp 0 R a 1 R = R a l V -1 x a l l
211 159 210 r19.29a R CRing Base R 1 x 𝒫 Clsd J x = y 𝒫 x Fin = y
212 0ex V
213 vex x V
214 elfi V x V fi x y 𝒫 x Fin = y
215 212 213 214 mp2an fi x y 𝒫 x Fin = y
216 211 215 sylibr R CRing Base R 1 x 𝒫 Clsd J x = fi x
217 216 ex R CRing Base R 1 x 𝒫 Clsd J x = fi x
218 217 necon3bd R CRing Base R 1 x 𝒫 Clsd J ¬ fi x x
219 218 ralrimiva R CRing Base R 1 x 𝒫 Clsd J ¬ fi x x
220 cmpfi J Top J Comp x 𝒫 Clsd J ¬ fi x x
221 220 biimpar J Top x 𝒫 Clsd J ¬ fi x x J Comp
222 10 219 221 syl2an2r R CRing Base R 1 J Comp
223 9 222 pm2.61dane R CRing J Comp