Theorem zarclsun

Description: The union of two closed sets of the Zariski topology is closed. (Contributed by Thierry Arnoux, 16-Jun-2024)

	Ref	Expression
Hypothesis	zarclsx.1	No typesetting found for |- V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) with typecode |-
Assertion	zarclsun	$$⊢\left(R\in \mathrm{CRing}\wedge X\in \mathrm{ran}V\wedge Y\in \mathrm{ran}V\right)\to X\cup Y\in \mathrm{ran}V$$

Proof

Step	Hyp	Ref	Expression
1		zarclsx.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 |-
2		simpllr	Could not format ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ X = { j e. ( PrmIdeal ` R ) | l C_ j } ) /\ k e. ( LIdeal ` R ) ) /\ Y = { j e. ( PrmIdeal ` R ) | k C_ j } ) -> X = { j e. ( PrmIdeal ` R ) | l C_ j } ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ X = { j e. ( PrmIdeal ` R ) | l C_ j } ) /\ k e. ( LIdeal ` R ) ) /\ Y = { j e. ( PrmIdeal ` R ) | k C_ j } ) -> X = { j e. ( PrmIdeal ` R ) | l C_ j } ) with typecode |-
3		simpr	Could not format ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ X = { j e. ( PrmIdeal ` R ) | l C_ j } ) /\ k e. ( LIdeal ` R ) ) /\ Y = { j e. ( PrmIdeal ` R ) | k C_ j } ) -> Y = { j e. ( PrmIdeal ` R ) | k C_ j } ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ X = { j e. ( PrmIdeal ` R ) | l C_ j } ) /\ k e. ( LIdeal ` R ) ) /\ Y = { j e. ( PrmIdeal ` R ) | k C_ j } ) -> Y = { j e. ( PrmIdeal ` R ) | k C_ j } ) with typecode |-
4	2 3	uneq12d	Could not format ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ X = { j e. ( PrmIdeal ` R ) | l C_ j } ) /\ k e. ( LIdeal ` R ) ) /\ Y = { j e. ( PrmIdeal ` R ) | k C_ j } ) -> ( X u. Y ) = ( { j e. ( PrmIdeal ` R ) | l C_ j } u. { j e. ( PrmIdeal ` R ) | k C_ j } ) ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ X = { j e. ( PrmIdeal ` R ) | l C_ j } ) /\ k e. ( LIdeal ` R ) ) /\ Y = { j e. ( PrmIdeal ` R ) | k C_ j } ) -> ( X u. Y ) = ( { j e. ( PrmIdeal ` R ) | l C_ j } u. { j e. ( PrmIdeal ` R ) | k C_ j } ) ) with typecode |-
5		unrab	Could not format ( { j e. ( PrmIdeal ` R ) | l C_ j } u. { j e. ( PrmIdeal ` R ) | k C_ j } ) = { j e. ( PrmIdeal ` R ) | ( l C_ j \/ k C_ j ) } : No typesetting found for |- ( { j e. ( PrmIdeal ` R ) | l C_ j } u. { j e. ( PrmIdeal ` R ) | k C_ j } ) = { j e. ( PrmIdeal ` R ) | ( l C_ j \/ k C_ j ) } with typecode |-
6		eqid	Could not format ( IDLsrg ` R ) = ( IDLsrg ` R ) : No typesetting found for |- ( IDLsrg ` R ) = ( IDLsrg ` R ) with typecode |-
7		eqid	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LIdeal}\left(R\right)$$
8		eqid	Could not format ( .r ` ( IDLsrg ` R ) ) = ( .r ` ( IDLsrg ` R ) ) : No typesetting found for |- ( .r ` ( IDLsrg ` R ) ) = ( .r ` ( IDLsrg ` R ) ) with typecode |-
9		simpll	$$⊢\left(\left(R\in \mathrm{CRing}\wedge l\in \mathrm{LIdeal}\left(R\right)\right)\wedge k\in \mathrm{LIdeal}\left(R\right)\right)\to R\in \mathrm{CRing}$$
10	9	crngringd	$$⊢\left(\left(R\in \mathrm{CRing}\wedge l\in \mathrm{LIdeal}\left(R\right)\right)\wedge k\in \mathrm{LIdeal}\left(R\right)\right)\to R\in \mathrm{Ring}$$
11		simplr	$$⊢\left(\left(R\in \mathrm{CRing}\wedge l\in \mathrm{LIdeal}\left(R\right)\right)\wedge k\in \mathrm{LIdeal}\left(R\right)\right)\to l\in \mathrm{LIdeal}\left(R\right)$$
12		simpr	$$⊢\left(\left(R\in \mathrm{CRing}\wedge l\in \mathrm{LIdeal}\left(R\right)\right)\wedge k\in \mathrm{LIdeal}\left(R\right)\right)\to k\in \mathrm{LIdeal}\left(R\right)$$
13	6 7 8 10 11 12	idlsrgmulrcl	Could not format ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) -> ( l ( .r ` ( IDLsrg ` R ) ) k ) e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) -> ( l ( .r ` ( IDLsrg ` R ) ) k ) e. ( LIdeal ` R ) ) with typecode |-
14		sseq1	Could not format ( i = ( l ( .r ` ( IDLsrg ` R ) ) k ) -> ( i C_ j <-> ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) ) : No typesetting found for |- ( i = ( l ( .r ` ( IDLsrg ` R ) ) k ) -> ( i C_ j <-> ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) ) with typecode |-
15	14	rabbidv	Could not format ( i = ( l ( .r ` ( IDLsrg ` R ) ) k ) -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j } ) : No typesetting found for |- ( i = ( l ( .r ` ( IDLsrg ` R ) ) k ) -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j } ) with typecode |-
16	15	eqeq2d	Could not format ( i = ( l ( .r ` ( IDLsrg ` R ) ) k ) -> ( { j e. ( PrmIdeal ` R ) | ( l C_ j \/ k C_ j ) } = { j e. ( PrmIdeal ` R ) | i C_ j } <-> { j e. ( PrmIdeal ` R ) | ( l C_ j \/ k C_ j ) } = { j e. ( PrmIdeal ` R ) | ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j } ) ) : No typesetting found for |- ( i = ( l ( .r ` ( IDLsrg ` R ) ) k ) -> ( { j e. ( PrmIdeal ` R ) | ( l C_ j \/ k C_ j ) } = { j e. ( PrmIdeal ` R ) | i C_ j } <-> { j e. ( PrmIdeal ` R ) | ( l C_ j \/ k C_ j ) } = { j e. ( PrmIdeal ` R ) | ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j } ) ) with typecode |-
17	16	adantl	Could not format ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ i = ( l ( .r ` ( IDLsrg ` R ) ) k ) ) -> ( { j e. ( PrmIdeal ` R ) | ( l C_ j \/ k C_ j ) } = { j e. ( PrmIdeal ` R ) | i C_ j } <-> { j e. ( PrmIdeal ` R ) | ( l C_ j \/ k C_ j ) } = { j e. ( PrmIdeal ` R ) | ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j } ) ) : No typesetting found for |- ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ i = ( l ( .r ` ( IDLsrg ` R ) ) k ) ) -> ( { j e. ( PrmIdeal ` R ) | ( l C_ j \/ k C_ j ) } = { j e. ( PrmIdeal ` R ) | i C_ j } <-> { j e. ( PrmIdeal ` R ) | ( l C_ j \/ k C_ j ) } = { j e. ( PrmIdeal ` R ) | ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j } ) ) with typecode |-
18		eqid	$$⊢{\cdot }_R={\cdot }_R$$
19	9	ad2antrr	Could not format ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ l C_ j ) -> R e. CRing ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ l C_ j ) -> R e. CRing ) with typecode |-
20	11	ad2antrr	Could not format ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ l C_ j ) -> l e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ l C_ j ) -> l e. ( LIdeal ` R ) ) with typecode |-
21	12	ad2antrr	Could not format ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ l C_ j ) -> k e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ l C_ j ) -> k e. ( LIdeal ` R ) ) with typecode |-
22	6 7 8 18 19 20 21	idlsrgmulrss1	Could not format ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ l C_ j ) -> ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ l ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ l C_ j ) -> ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ l ) with typecode |-
23		simpr	Could not format ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ l C_ j ) -> l C_ j ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ l C_ j ) -> l C_ j ) with typecode |-
24	22 23	sstrd	Could not format ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ l C_ j ) -> ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ l C_ j ) -> ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) with typecode |-
25	10	ad2antrr	Could not format ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ k C_ j ) -> R e. Ring ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ k C_ j ) -> R e. Ring ) with typecode |-
26	11	ad2antrr	Could not format ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ k C_ j ) -> l e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ k C_ j ) -> l e. ( LIdeal ` R ) ) with typecode |-
27	12	ad2antrr	Could not format ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ k C_ j ) -> k e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ k C_ j ) -> k e. ( LIdeal ` R ) ) with typecode |-
28	6 7 8 18 25 26 27	idlsrgmulrss2	Could not format ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ k C_ j ) -> ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ k ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ k C_ j ) -> ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ k ) with typecode |-
29		simpr	Could not format ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ k C_ j ) -> k C_ j ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ k C_ j ) -> k C_ j ) with typecode |-
30	28 29	sstrd	Could not format ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ k C_ j ) -> ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ k C_ j ) -> ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) with typecode |-
31	24 30	jaodan	Could not format ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l C_ j \/ k C_ j ) ) -> ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l C_ j \/ k C_ j ) ) -> ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) with typecode |-
32		eqid	$$⊢\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)=\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)$$
33	10	ad2antrr	Could not format ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> R e. Ring ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> R e. Ring ) with typecode |-
34		simplr	Could not format ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> j e. ( PrmIdeal ` R ) ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> j e. ( PrmIdeal ` R ) ) with typecode |-
35	11	ad2antrr	Could not format ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> l e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> l e. ( LIdeal ` R ) ) with typecode |-
36	12	ad2antrr	Could not format ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> k e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> k e. ( LIdeal ` R ) ) with typecode |-
37		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
38		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
39	37 7	lidlss	$$⊢l\in \mathrm{LIdeal}\left(R\right)\to l\subseteq {\mathrm{Base}}_R$$
40	35 39	syl	Could not format ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> l C_ ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> l C_ ( Base ` R ) ) with typecode |-
41	37 7	lidlss	$$⊢k\in \mathrm{LIdeal}\left(R\right)\to k\subseteq {\mathrm{Base}}_R$$
42	36 41	syl	Could not format ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> k C_ ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> k C_ ( Base ` R ) ) with typecode |-
43	37 38 32 33 40 42	ringlsmss	Could not format ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> ( l ( LSSum ` ( mulGrp ` R ) ) k ) C_ ( Base ` R ) ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> ( l ( LSSum ` ( mulGrp ` R ) ) k ) C_ ( Base ` R ) ) with typecode |-
44		eqid	$$⊢\mathrm{RSpan}\left(R\right)=\mathrm{RSpan}\left(R\right)$$
45	44 37	rspssid	$$⊢\left(R\in \mathrm{Ring}\wedge l\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)k\subseteq {\mathrm{Base}}_R\right)\to l\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)k\subseteq \mathrm{RSpan}\left(R\right)\left(l\mathrm{LSSum}\left({\mathrm{mulGrp}}_R\right)k\right)$$
46	33 43 45	syl2anc	Could not format ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> ( l ( LSSum ` ( mulGrp ` R ) ) k ) C_ ( ( RSpan ` R ) ` ( l ( LSSum ` ( mulGrp ` R ) ) k ) ) ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> ( l ( LSSum ` ( mulGrp ` R ) ) k ) C_ ( ( RSpan ` R ) ` ( l ( LSSum ` ( mulGrp ` R ) ) k ) ) ) with typecode |-
47	6 7 8 38 32 33 35 36	idlsrgmulrval	Could not format ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> ( l ( .r ` ( IDLsrg ` R ) ) k ) = ( ( RSpan ` R ) ` ( l ( LSSum ` ( mulGrp ` R ) ) k ) ) ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> ( l ( .r ` ( IDLsrg ` R ) ) k ) = ( ( RSpan ` R ) ` ( l ( LSSum ` ( mulGrp ` R ) ) k ) ) ) with typecode |-
48	46 47	sseqtrrd	Could not format ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> ( l ( LSSum ` ( mulGrp ` R ) ) k ) C_ ( l ( .r ` ( IDLsrg ` R ) ) k ) ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> ( l ( LSSum ` ( mulGrp ` R ) ) k ) C_ ( l ( .r ` ( IDLsrg ` R ) ) k ) ) with typecode |-
49		simpr	Could not format ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) with typecode |-
50	48 49	sstrd	Could not format ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> ( l ( LSSum ` ( mulGrp ` R ) ) k ) C_ j ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> ( l ( LSSum ` ( mulGrp ` R ) ) k ) C_ j ) with typecode |-
51	32 33 34 35 36 50	idlmulssprm	Could not format ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> ( l C_ j \/ k C_ j ) ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) /\ ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) -> ( l C_ j \/ k C_ j ) ) with typecode |-
52	31 51	impbida	Could not format ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) -> ( ( l C_ j \/ k C_ j ) <-> ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) ) : No typesetting found for |- ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) /\ j e. ( PrmIdeal ` R ) ) -> ( ( l C_ j \/ k C_ j ) <-> ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j ) ) with typecode |-
53	52	rabbidva	Could not format ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) -> { j e. ( PrmIdeal ` R ) | ( l C_ j \/ k C_ j ) } = { j e. ( PrmIdeal ` R ) | ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j } ) : No typesetting found for |- ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) -> { j e. ( PrmIdeal ` R ) | ( l C_ j \/ k C_ j ) } = { j e. ( PrmIdeal ` R ) | ( l ( .r ` ( IDLsrg ` R ) ) k ) C_ j } ) with typecode |-
54	13 17 53	rspcedvd	Could not format ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) -> E. i e. ( LIdeal ` R ) { j e. ( PrmIdeal ` R ) | ( l C_ j \/ k C_ j ) } = { j e. ( PrmIdeal ` R ) | i C_ j } ) : No typesetting found for |- ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) -> E. i e. ( LIdeal ` R ) { j e. ( PrmIdeal ` R ) | ( l C_ j \/ k C_ j ) } = { j e. ( PrmIdeal ` R ) | i C_ j } ) with typecode |-
55		fvex	Could not format ( PrmIdeal ` R ) e. _V : No typesetting found for |- ( PrmIdeal ` R ) e. _V with typecode |-
56	55	rabex	Could not format { j e. ( PrmIdeal ` R ) | ( l C_ j \/ k C_ j ) } e. _V : No typesetting found for |- { j e. ( PrmIdeal ` R ) | ( l C_ j \/ k C_ j ) } e. _V with typecode |-
57	56	a1i	Could not format ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) -> { j e. ( PrmIdeal ` R ) | ( l C_ j \/ k C_ j ) } e. _V ) : No typesetting found for |- ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) -> { j e. ( PrmIdeal ` R ) | ( l C_ j \/ k C_ j ) } e. _V ) with typecode |-
58	1 54 57	elrnmptd	Could not format ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) -> { j e. ( PrmIdeal ` R ) | ( l C_ j \/ k C_ j ) } e. ran V ) : No typesetting found for |- ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) -> { j e. ( PrmIdeal ` R ) | ( l C_ j \/ k C_ j ) } e. ran V ) with typecode |-
59	5 58	eqeltrid	Could not format ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) -> ( { j e. ( PrmIdeal ` R ) | l C_ j } u. { j e. ( PrmIdeal ` R ) | k C_ j } ) e. ran V ) : No typesetting found for |- ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ k e. ( LIdeal ` R ) ) -> ( { j e. ( PrmIdeal ` R ) | l C_ j } u. { j e. ( PrmIdeal ` R ) | k C_ j } ) e. ran V ) with typecode |-
60	59	adantlr	Could not format ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ X = { j e. ( PrmIdeal ` R ) | l C_ j } ) /\ k e. ( LIdeal ` R ) ) -> ( { j e. ( PrmIdeal ` R ) | l C_ j } u. { j e. ( PrmIdeal ` R ) | k C_ j } ) e. ran V ) : No typesetting found for |- ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ X = { j e. ( PrmIdeal ` R ) | l C_ j } ) /\ k e. ( LIdeal ` R ) ) -> ( { j e. ( PrmIdeal ` R ) | l C_ j } u. { j e. ( PrmIdeal ` R ) | k C_ j } ) e. ran V ) with typecode |-
61	60	adantr	Could not format ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ X = { j e. ( PrmIdeal ` R ) | l C_ j } ) /\ k e. ( LIdeal ` R ) ) /\ Y = { j e. ( PrmIdeal ` R ) | k C_ j } ) -> ( { j e. ( PrmIdeal ` R ) | l C_ j } u. { j e. ( PrmIdeal ` R ) | k C_ j } ) e. ran V ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ X = { j e. ( PrmIdeal ` R ) | l C_ j } ) /\ k e. ( LIdeal ` R ) ) /\ Y = { j e. ( PrmIdeal ` R ) | k C_ j } ) -> ( { j e. ( PrmIdeal ` R ) | l C_ j } u. { j e. ( PrmIdeal ` R ) | k C_ j } ) e. ran V ) with typecode |-
62	4 61	eqeltrd	Could not format ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ X = { j e. ( PrmIdeal ` R ) | l C_ j } ) /\ k e. ( LIdeal ` R ) ) /\ Y = { j e. ( PrmIdeal ` R ) | k C_ j } ) -> ( X u. Y ) e. ran V ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ l e. ( LIdeal ` R ) ) /\ X = { j e. ( PrmIdeal ` R ) | l C_ j } ) /\ k e. ( LIdeal ` R ) ) /\ Y = { j e. ( PrmIdeal ` R ) | k C_ j } ) -> ( X u. Y ) e. ran V ) with typecode |-
63	62	adantl4r	Could not format ( ( ( ( ( ( R e. CRing /\ Y e. ran V ) /\ l e. ( LIdeal ` R ) ) /\ X = { j e. ( PrmIdeal ` R ) | l C_ j } ) /\ k e. ( LIdeal ` R ) ) /\ Y = { j e. ( PrmIdeal ` R ) | k C_ j } ) -> ( X u. Y ) e. ran V ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ Y e. ran V ) /\ l e. ( LIdeal ` R ) ) /\ X = { j e. ( PrmIdeal ` R ) | l C_ j } ) /\ k e. ( LIdeal ` R ) ) /\ Y = { j e. ( PrmIdeal ` R ) | k C_ j } ) -> ( X u. Y ) e. ran V ) with typecode |-
64	55	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 |-
65	1 64	elrnmpti	Could not format ( Y e. ran V <-> E. i e. ( LIdeal ` R ) Y = { j e. ( PrmIdeal ` R ) | i C_ j } ) : No typesetting found for |- ( Y e. ran V <-> E. i e. ( LIdeal ` R ) Y = { j e. ( PrmIdeal ` R ) | i C_ j } ) with typecode |-
66		sseq1	$$⊢i=k\to \left(i\subseteq j\leftrightarrow k\subseteq j\right)$$
67	66	rabbidv	Could not format ( i = k -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | k C_ j } ) : No typesetting found for |- ( i = k -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | k C_ j } ) with typecode |-
68	67	eqeq2d	Could not format ( i = k -> ( Y = { j e. ( PrmIdeal ` R ) | i C_ j } <-> Y = { j e. ( PrmIdeal ` R ) | k C_ j } ) ) : No typesetting found for |- ( i = k -> ( Y = { j e. ( PrmIdeal ` R ) | i C_ j } <-> Y = { j e. ( PrmIdeal ` R ) | k C_ j } ) ) with typecode |-
69	68	cbvrexvw	Could not format ( E. i e. ( LIdeal ` R ) Y = { j e. ( PrmIdeal ` R ) | i C_ j } <-> E. k e. ( LIdeal ` R ) Y = { j e. ( PrmIdeal ` R ) | k C_ j } ) : No typesetting found for |- ( E. i e. ( LIdeal ` R ) Y = { j e. ( PrmIdeal ` R ) | i C_ j } <-> E. k e. ( LIdeal ` R ) Y = { j e. ( PrmIdeal ` R ) | k C_ j } ) with typecode |-
70		biid	Could not format ( E. k e. ( LIdeal ` R ) Y = { j e. ( PrmIdeal ` R ) | k C_ j } <-> E. k e. ( LIdeal ` R ) Y = { j e. ( PrmIdeal ` R ) | k C_ j } ) : No typesetting found for |- ( E. k e. ( LIdeal ` R ) Y = { j e. ( PrmIdeal ` R ) | k C_ j } <-> E. k e. ( LIdeal ` R ) Y = { j e. ( PrmIdeal ` R ) | k C_ j } ) with typecode |-
71	65 69 70	3bitri	Could not format ( Y e. ran V <-> E. k e. ( LIdeal ` R ) Y = { j e. ( PrmIdeal ` R ) | k C_ j } ) : No typesetting found for |- ( Y e. ran V <-> E. k e. ( LIdeal ` R ) Y = { j e. ( PrmIdeal ` R ) | k C_ j } ) with typecode |-
72	71	biimpi	Could not format ( Y e. ran V -> E. k e. ( LIdeal ` R ) Y = { j e. ( PrmIdeal ` R ) | k C_ j } ) : No typesetting found for |- ( Y e. ran V -> E. k e. ( LIdeal ` R ) Y = { j e. ( PrmIdeal ` R ) | k C_ j } ) with typecode |-
73	72	ad3antlr	Could not format ( ( ( ( R e. CRing /\ Y e. ran V ) /\ l e. ( LIdeal ` R ) ) /\ X = { j e. ( PrmIdeal ` R ) | l C_ j } ) -> E. k e. ( LIdeal ` R ) Y = { j e. ( PrmIdeal ` R ) | k C_ j } ) : No typesetting found for |- ( ( ( ( R e. CRing /\ Y e. ran V ) /\ l e. ( LIdeal ` R ) ) /\ X = { j e. ( PrmIdeal ` R ) | l C_ j } ) -> E. k e. ( LIdeal ` R ) Y = { j e. ( PrmIdeal ` R ) | k C_ j } ) with typecode |-
74	63 73	r19.29a	Could not format ( ( ( ( R e. CRing /\ Y e. ran V ) /\ l e. ( LIdeal ` R ) ) /\ X = { j e. ( PrmIdeal ` R ) | l C_ j } ) -> ( X u. Y ) e. ran V ) : No typesetting found for |- ( ( ( ( R e. CRing /\ Y e. ran V ) /\ l e. ( LIdeal ` R ) ) /\ X = { j e. ( PrmIdeal ` R ) | l C_ j } ) -> ( X u. Y ) e. ran V ) with typecode |-
75	74	adantl3r	Could not format ( ( ( ( ( R e. CRing /\ X e. ran V ) /\ Y e. ran V ) /\ l e. ( LIdeal ` R ) ) /\ X = { j e. ( PrmIdeal ` R ) | l C_ j } ) -> ( X u. Y ) e. ran V ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ X e. ran V ) /\ Y e. ran V ) /\ l e. ( LIdeal ` R ) ) /\ X = { j e. ( PrmIdeal ` R ) | l C_ j } ) -> ( X u. Y ) e. ran V ) with typecode |-
76	1 64	elrnmpti	Could not format ( X e. ran V <-> E. i e. ( LIdeal ` R ) X = { j e. ( PrmIdeal ` R ) | i C_ j } ) : No typesetting found for |- ( X e. ran V <-> E. i e. ( LIdeal ` R ) X = { j e. ( PrmIdeal ` R ) | i C_ j } ) with typecode |-
77		sseq1	$$⊢i=l\to \left(i\subseteq j\leftrightarrow l\subseteq j\right)$$
78	77	rabbidv	Could not format ( i = l -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | l C_ j } ) : No typesetting found for |- ( i = l -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | l C_ j } ) with typecode |-
79	78	eqeq2d	Could not format ( i = l -> ( X = { j e. ( PrmIdeal ` R ) | i C_ j } <-> X = { j e. ( PrmIdeal ` R ) | l C_ j } ) ) : No typesetting found for |- ( i = l -> ( X = { j e. ( PrmIdeal ` R ) | i C_ j } <-> X = { j e. ( PrmIdeal ` R ) | l C_ j } ) ) with typecode |-
80	79	cbvrexvw	Could not format ( E. i e. ( LIdeal ` R ) X = { j e. ( PrmIdeal ` R ) | i C_ j } <-> E. l e. ( LIdeal ` R ) X = { j e. ( PrmIdeal ` R ) | l C_ j } ) : No typesetting found for |- ( E. i e. ( LIdeal ` R ) X = { j e. ( PrmIdeal ` R ) | i C_ j } <-> E. l e. ( LIdeal ` R ) X = { j e. ( PrmIdeal ` R ) | l C_ j } ) with typecode |-
81		biid	Could not format ( E. l e. ( LIdeal ` R ) X = { j e. ( PrmIdeal ` R ) | l C_ j } <-> E. l e. ( LIdeal ` R ) X = { j e. ( PrmIdeal ` R ) | l C_ j } ) : No typesetting found for |- ( E. l e. ( LIdeal ` R ) X = { j e. ( PrmIdeal ` R ) | l C_ j } <-> E. l e. ( LIdeal ` R ) X = { j e. ( PrmIdeal ` R ) | l C_ j } ) with typecode |-
82	76 80 81	3bitri	Could not format ( X e. ran V <-> E. l e. ( LIdeal ` R ) X = { j e. ( PrmIdeal ` R ) | l C_ j } ) : No typesetting found for |- ( X e. ran V <-> E. l e. ( LIdeal ` R ) X = { j e. ( PrmIdeal ` R ) | l C_ j } ) with typecode |-
83	82	biimpi	Could not format ( X e. ran V -> E. l e. ( LIdeal ` R ) X = { j e. ( PrmIdeal ` R ) | l C_ j } ) : No typesetting found for |- ( X e. ran V -> E. l e. ( LIdeal ` R ) X = { j e. ( PrmIdeal ` R ) | l C_ j } ) with typecode |-
84	83	ad2antlr	Could not format ( ( ( R e. CRing /\ X e. ran V ) /\ Y e. ran V ) -> E. l e. ( LIdeal ` R ) X = { j e. ( PrmIdeal ` R ) | l C_ j } ) : No typesetting found for |- ( ( ( R e. CRing /\ X e. ran V ) /\ Y e. ran V ) -> E. l e. ( LIdeal ` R ) X = { j e. ( PrmIdeal ` R ) | l C_ j } ) with typecode |-
85	75 84	r19.29a	$$⊢\left(\left(R\in \mathrm{CRing}\wedge X\in \mathrm{ran}V\right)\wedge Y\in \mathrm{ran}V\right)\to X\cup Y\in \mathrm{ran}V$$
86	85	3impa	$$⊢\left(R\in \mathrm{CRing}\wedge X\in \mathrm{ran}V\wedge Y\in \mathrm{ran}V\right)\to X\cup Y\in \mathrm{ran}V$$