Theorem lidlval 20542

Description: Value of the set of ring ideals. (Contributed by Stefan O'Rear, 31-Mar-2015.)

Assertion

Ref	Expression
lidlval	⊢ (LIdeal‘𝑊) = (LSubSp‘(ringLMod‘𝑊))

Proof of Theorem lidlval

Step	Hyp	Ref	Expression
1		df-lidl 20516	. . 3 ⊢ LIdeal = (LSubSp ∘ ringLMod)
2	1	fveq1i 6812	. 2 ⊢ (LIdeal‘𝑊) = ((LSubSp ∘ ringLMod)‘𝑊)
3		00lss 20283	. . 3 ⊢ ∅ = (LSubSp‘∅)
4		rlmfn 20540	. . . 4 ⊢ ringLMod Fn V
5		fnfun 6571	. . . 4 ⊢ (ringLMod Fn V → Fun ringLMod)
6	4, 5	ax-mp 5	. . 3 ⊢ Fun ringLMod
7	3, 6	fvco4i 6908	. 2 ⊢ ((LSubSp ∘ ringLMod)‘𝑊) = (LSubSp‘(ringLMod‘𝑊))
8	2, 7	eqtri 2764	1 ⊢ (LIdeal‘𝑊) = (LSubSp‘(ringLMod‘𝑊))

Syntax hints:   = wceq 1540  Vcvv 3440   ∘ ccom 5611  Fun wfun 6459   Fn wfn 6460  ‘cfv 6465  LSubSpclss 20273  ringLModcrglmod 20511  LIdealclidl 20512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5237  ax-nul 5244  ax-pow 5302  ax-pr 5366  ax-un 7629  ax-cnex 11006  ax-1cn 11008  ax-addcl 11010

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3350  df-rab 3404  df-v 3442  df-sbc 3726  df-csb 3842  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-pss 3915  df-nul 4267  df-if 4471  df-pw 4546  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4850  df-iun 4938  df-br 5087  df-opab 5149  df-mpt 5170  df-tr 5204  df-id 5506  df-eprel 5512  df-po 5520  df-so 5521  df-fr 5562  df-we 5564  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-pred 6224  df-ord 6291  df-on 6292  df-lim 6293  df-suc 6294  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-ov 7319  df-om 7759  df-2nd 7878  df-frecs 8145  df-wrecs 8176  df-recs 8250  df-rdg 8289  df-nn 12053  df-slot 16957  df-ndx 16969  df-base 16987  df-lss 20274  df-rgmod 20515  df-lidl 20516

This theorem is referenced by:  lidlss  20561  islidl  20562  lidl0cl  20563  lidlacl  20564  lidlnegcl  20565  lidlmcl  20568  lidl0  20570  lidl1  20571  lidlacs  20572  rspcl  20573  rspssp  20577  mrcrsp  20578  lidlrsppropd  20581  lsmidllsp  31723  lsmidl  31724  islnr2  41161