MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mplsubrglem Structured version   Visualization version   GIF version

Theorem mplsubrglem 21563
Description: Lemma for mplsubrg 21564. (Contributed by Mario Carneiro, 9-Jan-2015.) (Revised by AV, 18-Jul-2019.)
Hypotheses
Ref Expression
mplsubg.s 𝑆 = (𝐼 mPwSer 𝑅)
mplsubg.p 𝑃 = (𝐼 mPoly 𝑅)
mplsubg.u π‘ˆ = (Baseβ€˜π‘ƒ)
mplsubg.i (πœ‘ β†’ 𝐼 ∈ π‘Š)
mpllss.r (πœ‘ β†’ 𝑅 ∈ Ring)
mplsubrglem.d 𝐷 = {𝑓 ∈ (β„•0 ↑m 𝐼) ∣ (◑𝑓 β€œ β„•) ∈ Fin}
mplsubrglem.z 0 = (0gβ€˜π‘…)
mplsubrglem.p 𝐴 = ( ∘f + β€œ ((𝑋 supp 0 ) Γ— (π‘Œ supp 0 )))
mplsubrglem.t Β· = (.rβ€˜π‘…)
mplsubrglem.x (πœ‘ β†’ 𝑋 ∈ π‘ˆ)
mplsubrglem.y (πœ‘ β†’ π‘Œ ∈ π‘ˆ)
Assertion
Ref Expression
mplsubrglem (πœ‘ β†’ (𝑋(.rβ€˜π‘†)π‘Œ) ∈ π‘ˆ)
Distinct variable groups:   𝑓,𝐼   𝑅,𝑓   𝑆,𝑓   𝑓,𝑋   𝑓,π‘Œ   0 ,𝑓
Allowed substitution hints:   πœ‘(𝑓)   𝐴(𝑓)   𝐷(𝑓)   𝑃(𝑓)   Β· (𝑓)   π‘ˆ(𝑓)   π‘Š(𝑓)

Proof of Theorem mplsubrglem
Dummy variables π‘˜ 𝑛 π‘₯ 𝑔 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mplsubg.s . . 3 𝑆 = (𝐼 mPwSer 𝑅)
2 eqid 2733 . . 3 (Baseβ€˜π‘†) = (Baseβ€˜π‘†)
3 eqid 2733 . . 3 (.rβ€˜π‘†) = (.rβ€˜π‘†)
4 mpllss.r . . 3 (πœ‘ β†’ 𝑅 ∈ Ring)
5 mplsubg.p . . . . 5 𝑃 = (𝐼 mPoly 𝑅)
6 mplsubg.u . . . . 5 π‘ˆ = (Baseβ€˜π‘ƒ)
75, 1, 6, 2mplbasss 21556 . . . 4 π‘ˆ βŠ† (Baseβ€˜π‘†)
8 mplsubrglem.x . . . 4 (πœ‘ β†’ 𝑋 ∈ π‘ˆ)
97, 8sselid 3981 . . 3 (πœ‘ β†’ 𝑋 ∈ (Baseβ€˜π‘†))
10 mplsubrglem.y . . . 4 (πœ‘ β†’ π‘Œ ∈ π‘ˆ)
117, 10sselid 3981 . . 3 (πœ‘ β†’ π‘Œ ∈ (Baseβ€˜π‘†))
121, 2, 3, 4, 9, 11psrmulcl 21507 . 2 (πœ‘ β†’ (𝑋(.rβ€˜π‘†)π‘Œ) ∈ (Baseβ€˜π‘†))
13 ovexd 7444 . . 3 (πœ‘ β†’ (𝑋(.rβ€˜π‘†)π‘Œ) ∈ V)
141, 2psrelbasfun 21499 . . . 4 ((𝑋(.rβ€˜π‘†)π‘Œ) ∈ (Baseβ€˜π‘†) β†’ Fun (𝑋(.rβ€˜π‘†)π‘Œ))
1512, 14syl 17 . . 3 (πœ‘ β†’ Fun (𝑋(.rβ€˜π‘†)π‘Œ))
16 mplsubrglem.z . . . . 5 0 = (0gβ€˜π‘…)
1716fvexi 6906 . . . 4 0 ∈ V
1817a1i 11 . . 3 (πœ‘ β†’ 0 ∈ V)
19 mplsubrglem.p . . . . 5 𝐴 = ( ∘f + β€œ ((𝑋 supp 0 ) Γ— (π‘Œ supp 0 )))
20 df-ima 5690 . . . . 5 ( ∘f + β€œ ((𝑋 supp 0 ) Γ— (π‘Œ supp 0 ))) = ran ( ∘f + β†Ύ ((𝑋 supp 0 ) Γ— (π‘Œ supp 0 )))
2119, 20eqtri 2761 . . . 4 𝐴 = ran ( ∘f + β†Ύ ((𝑋 supp 0 ) Γ— (π‘Œ supp 0 )))
225, 1, 2, 16, 6mplelbas 21550 . . . . . . . 8 (𝑋 ∈ π‘ˆ ↔ (𝑋 ∈ (Baseβ€˜π‘†) ∧ 𝑋 finSupp 0 ))
2322simprbi 498 . . . . . . 7 (𝑋 ∈ π‘ˆ β†’ 𝑋 finSupp 0 )
248, 23syl 17 . . . . . 6 (πœ‘ β†’ 𝑋 finSupp 0 )
255, 1, 2, 16, 6mplelbas 21550 . . . . . . . 8 (π‘Œ ∈ π‘ˆ ↔ (π‘Œ ∈ (Baseβ€˜π‘†) ∧ π‘Œ finSupp 0 ))
2625simprbi 498 . . . . . . 7 (π‘Œ ∈ π‘ˆ β†’ π‘Œ finSupp 0 )
2710, 26syl 17 . . . . . 6 (πœ‘ β†’ π‘Œ finSupp 0 )
28 fsuppxpfi 9380 . . . . . 6 ((𝑋 finSupp 0 ∧ π‘Œ finSupp 0 ) β†’ ((𝑋 supp 0 ) Γ— (π‘Œ supp 0 )) ∈ Fin)
2924, 27, 28syl2anc 585 . . . . 5 (πœ‘ β†’ ((𝑋 supp 0 ) Γ— (π‘Œ supp 0 )) ∈ Fin)
30 ofmres 7971 . . . . . . 7 ( ∘f + β†Ύ ((𝑋 supp 0 ) Γ— (π‘Œ supp 0 ))) = (𝑓 ∈ (𝑋 supp 0 ), 𝑔 ∈ (π‘Œ supp 0 ) ↦ (𝑓 ∘f + 𝑔))
31 ovex 7442 . . . . . . 7 (𝑓 ∘f + 𝑔) ∈ V
3230, 31fnmpoi 8056 . . . . . 6 ( ∘f + β†Ύ ((𝑋 supp 0 ) Γ— (π‘Œ supp 0 ))) Fn ((𝑋 supp 0 ) Γ— (π‘Œ supp 0 ))
33 dffn4 6812 . . . . . 6 (( ∘f + β†Ύ ((𝑋 supp 0 ) Γ— (π‘Œ supp 0 ))) Fn ((𝑋 supp 0 ) Γ— (π‘Œ supp 0 )) ↔ ( ∘f + β†Ύ ((𝑋 supp 0 ) Γ— (π‘Œ supp 0 ))):((𝑋 supp 0 ) Γ— (π‘Œ supp 0 ))–ontoβ†’ran ( ∘f + β†Ύ ((𝑋 supp 0 ) Γ— (π‘Œ supp 0 ))))
3432, 33mpbi 229 . . . . 5 ( ∘f + β†Ύ ((𝑋 supp 0 ) Γ— (π‘Œ supp 0 ))):((𝑋 supp 0 ) Γ— (π‘Œ supp 0 ))–ontoβ†’ran ( ∘f + β†Ύ ((𝑋 supp 0 ) Γ— (π‘Œ supp 0 )))
35 fofi 9338 . . . . 5 ((((𝑋 supp 0 ) Γ— (π‘Œ supp 0 )) ∈ Fin ∧ ( ∘f + β†Ύ ((𝑋 supp 0 ) Γ— (π‘Œ supp 0 ))):((𝑋 supp 0 ) Γ— (π‘Œ supp 0 ))–ontoβ†’ran ( ∘f + β†Ύ ((𝑋 supp 0 ) Γ— (π‘Œ supp 0 )))) β†’ ran ( ∘f + β†Ύ ((𝑋 supp 0 ) Γ— (π‘Œ supp 0 ))) ∈ Fin)
3629, 34, 35sylancl 587 . . . 4 (πœ‘ β†’ ran ( ∘f + β†Ύ ((𝑋 supp 0 ) Γ— (π‘Œ supp 0 ))) ∈ Fin)
3721, 36eqeltrid 2838 . . 3 (πœ‘ β†’ 𝐴 ∈ Fin)
38 eqid 2733 . . . . 5 (Baseβ€˜π‘…) = (Baseβ€˜π‘…)
39 mplsubrglem.d . . . . 5 𝐷 = {𝑓 ∈ (β„•0 ↑m 𝐼) ∣ (◑𝑓 β€œ β„•) ∈ Fin}
401, 38, 39, 2, 12psrelbas 21498 . . . 4 (πœ‘ β†’ (𝑋(.rβ€˜π‘†)π‘Œ):𝐷⟢(Baseβ€˜π‘…))
41 mplsubrglem.t . . . . . 6 Β· = (.rβ€˜π‘…)
429adantr 482 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) β†’ 𝑋 ∈ (Baseβ€˜π‘†))
4311adantr 482 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) β†’ π‘Œ ∈ (Baseβ€˜π‘†))
44 eldifi 4127 . . . . . . 7 (π‘˜ ∈ (𝐷 βˆ– 𝐴) β†’ π‘˜ ∈ 𝐷)
4544adantl 483 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) β†’ π‘˜ ∈ 𝐷)
461, 2, 41, 3, 39, 42, 43, 45psrmulval 21505 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) β†’ ((𝑋(.rβ€˜π‘†)π‘Œ)β€˜π‘˜) = (𝑅 Ξ£g (π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜} ↦ ((π‘‹β€˜π‘₯) Β· (π‘Œβ€˜(π‘˜ ∘f βˆ’ π‘₯))))))
474ad2antrr 725 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ 𝑅 ∈ Ring)
485, 38, 6, 39, 10mplelf 21557 . . . . . . . . . . . 12 (πœ‘ β†’ π‘Œ:𝐷⟢(Baseβ€˜π‘…))
4948ad2antrr 725 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ π‘Œ:𝐷⟢(Baseβ€˜π‘…))
50 ssrab2 4078 . . . . . . . . . . . 12 {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜} βŠ† 𝐷
5145adantr 482 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ π‘˜ ∈ 𝐷)
52 simpr 486 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜})
53 eqid 2733 . . . . . . . . . . . . . 14 {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜} = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}
5439, 53psrbagconcl 21487 . . . . . . . . . . . . 13 ((π‘˜ ∈ 𝐷 ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ (π‘˜ ∘f βˆ’ π‘₯) ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜})
5551, 52, 54syl2anc 585 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ (π‘˜ ∘f βˆ’ π‘₯) ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜})
5650, 55sselid 3981 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ (π‘˜ ∘f βˆ’ π‘₯) ∈ 𝐷)
5749, 56ffvelcdmd 7088 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ (π‘Œβ€˜(π‘˜ ∘f βˆ’ π‘₯)) ∈ (Baseβ€˜π‘…))
5838, 41, 16ringlz 20107 . . . . . . . . . 10 ((𝑅 ∈ Ring ∧ (π‘Œβ€˜(π‘˜ ∘f βˆ’ π‘₯)) ∈ (Baseβ€˜π‘…)) β†’ ( 0 Β· (π‘Œβ€˜(π‘˜ ∘f βˆ’ π‘₯))) = 0 )
5947, 57, 58syl2anc 585 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ ( 0 Β· (π‘Œβ€˜(π‘˜ ∘f βˆ’ π‘₯))) = 0 )
60 oveq1 7416 . . . . . . . . . 10 ((π‘‹β€˜π‘₯) = 0 β†’ ((π‘‹β€˜π‘₯) Β· (π‘Œβ€˜(π‘˜ ∘f βˆ’ π‘₯))) = ( 0 Β· (π‘Œβ€˜(π‘˜ ∘f βˆ’ π‘₯))))
6160eqeq1d 2735 . . . . . . . . 9 ((π‘‹β€˜π‘₯) = 0 β†’ (((π‘‹β€˜π‘₯) Β· (π‘Œβ€˜(π‘˜ ∘f βˆ’ π‘₯))) = 0 ↔ ( 0 Β· (π‘Œβ€˜(π‘˜ ∘f βˆ’ π‘₯))) = 0 ))
6259, 61syl5ibrcom 246 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ ((π‘‹β€˜π‘₯) = 0 β†’ ((π‘‹β€˜π‘₯) Β· (π‘Œβ€˜(π‘˜ ∘f βˆ’ π‘₯))) = 0 ))
635, 38, 6, 39, 8mplelf 21557 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑋:𝐷⟢(Baseβ€˜π‘…))
6463ad2antrr 725 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ 𝑋:𝐷⟢(Baseβ€˜π‘…))
6550, 52sselid 3981 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ π‘₯ ∈ 𝐷)
6664, 65ffvelcdmd 7088 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ (π‘‹β€˜π‘₯) ∈ (Baseβ€˜π‘…))
6738, 41, 16ringrz 20108 . . . . . . . . . 10 ((𝑅 ∈ Ring ∧ (π‘‹β€˜π‘₯) ∈ (Baseβ€˜π‘…)) β†’ ((π‘‹β€˜π‘₯) Β· 0 ) = 0 )
6847, 66, 67syl2anc 585 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ ((π‘‹β€˜π‘₯) Β· 0 ) = 0 )
69 oveq2 7417 . . . . . . . . . 10 ((π‘Œβ€˜(π‘˜ ∘f βˆ’ π‘₯)) = 0 β†’ ((π‘‹β€˜π‘₯) Β· (π‘Œβ€˜(π‘˜ ∘f βˆ’ π‘₯))) = ((π‘‹β€˜π‘₯) Β· 0 ))
7069eqeq1d 2735 . . . . . . . . 9 ((π‘Œβ€˜(π‘˜ ∘f βˆ’ π‘₯)) = 0 β†’ (((π‘‹β€˜π‘₯) Β· (π‘Œβ€˜(π‘˜ ∘f βˆ’ π‘₯))) = 0 ↔ ((π‘‹β€˜π‘₯) Β· 0 ) = 0 ))
7168, 70syl5ibrcom 246 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ ((π‘Œβ€˜(π‘˜ ∘f βˆ’ π‘₯)) = 0 β†’ ((π‘‹β€˜π‘₯) Β· (π‘Œβ€˜(π‘˜ ∘f βˆ’ π‘₯))) = 0 ))
7239psrbagf 21471 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ 𝐷 β†’ π‘₯:πΌβŸΆβ„•0)
7365, 72syl 17 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ π‘₯:πΌβŸΆβ„•0)
7473ffvelcdmda 7087 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) ∧ 𝑛 ∈ 𝐼) β†’ (π‘₯β€˜π‘›) ∈ β„•0)
7539psrbagf 21471 . . . . . . . . . . . . . . . . . 18 (π‘˜ ∈ 𝐷 β†’ π‘˜:πΌβŸΆβ„•0)
7651, 75syl 17 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ π‘˜:πΌβŸΆβ„•0)
7776ffvelcdmda 7087 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) ∧ 𝑛 ∈ 𝐼) β†’ (π‘˜β€˜π‘›) ∈ β„•0)
78 nn0cn 12482 . . . . . . . . . . . . . . . . 17 ((π‘₯β€˜π‘›) ∈ β„•0 β†’ (π‘₯β€˜π‘›) ∈ β„‚)
79 nn0cn 12482 . . . . . . . . . . . . . . . . 17 ((π‘˜β€˜π‘›) ∈ β„•0 β†’ (π‘˜β€˜π‘›) ∈ β„‚)
80 pncan3 11468 . . . . . . . . . . . . . . . . 17 (((π‘₯β€˜π‘›) ∈ β„‚ ∧ (π‘˜β€˜π‘›) ∈ β„‚) β†’ ((π‘₯β€˜π‘›) + ((π‘˜β€˜π‘›) βˆ’ (π‘₯β€˜π‘›))) = (π‘˜β€˜π‘›))
8178, 79, 80syl2an 597 . . . . . . . . . . . . . . . 16 (((π‘₯β€˜π‘›) ∈ β„•0 ∧ (π‘˜β€˜π‘›) ∈ β„•0) β†’ ((π‘₯β€˜π‘›) + ((π‘˜β€˜π‘›) βˆ’ (π‘₯β€˜π‘›))) = (π‘˜β€˜π‘›))
8274, 77, 81syl2anc 585 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) ∧ 𝑛 ∈ 𝐼) β†’ ((π‘₯β€˜π‘›) + ((π‘˜β€˜π‘›) βˆ’ (π‘₯β€˜π‘›))) = (π‘˜β€˜π‘›))
8382mpteq2dva 5249 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ (𝑛 ∈ 𝐼 ↦ ((π‘₯β€˜π‘›) + ((π‘˜β€˜π‘›) βˆ’ (π‘₯β€˜π‘›)))) = (𝑛 ∈ 𝐼 ↦ (π‘˜β€˜π‘›)))
84 mplsubg.i . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐼 ∈ π‘Š)
8584ad2antrr 725 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ 𝐼 ∈ π‘Š)
86 ovexd 7444 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) ∧ 𝑛 ∈ 𝐼) β†’ ((π‘˜β€˜π‘›) βˆ’ (π‘₯β€˜π‘›)) ∈ V)
8773feqmptd 6961 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ π‘₯ = (𝑛 ∈ 𝐼 ↦ (π‘₯β€˜π‘›)))
8876feqmptd 6961 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ π‘˜ = (𝑛 ∈ 𝐼 ↦ (π‘˜β€˜π‘›)))
8985, 77, 74, 88, 87offval2 7690 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ (π‘˜ ∘f βˆ’ π‘₯) = (𝑛 ∈ 𝐼 ↦ ((π‘˜β€˜π‘›) βˆ’ (π‘₯β€˜π‘›))))
9085, 74, 86, 87, 89offval2 7690 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ (π‘₯ ∘f + (π‘˜ ∘f βˆ’ π‘₯)) = (𝑛 ∈ 𝐼 ↦ ((π‘₯β€˜π‘›) + ((π‘˜β€˜π‘›) βˆ’ (π‘₯β€˜π‘›)))))
9183, 90, 883eqtr4d 2783 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ (π‘₯ ∘f + (π‘˜ ∘f βˆ’ π‘₯)) = π‘˜)
92 simplr 768 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ π‘˜ ∈ (𝐷 βˆ– 𝐴))
9391, 92eqeltrd 2834 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ (π‘₯ ∘f + (π‘˜ ∘f βˆ’ π‘₯)) ∈ (𝐷 βˆ– 𝐴))
9493eldifbd 3962 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ Β¬ (π‘₯ ∘f + (π‘˜ ∘f βˆ’ π‘₯)) ∈ 𝐴)
95 ovres 7573 . . . . . . . . . . . 12 ((π‘₯ ∈ (𝑋 supp 0 ) ∧ (π‘˜ ∘f βˆ’ π‘₯) ∈ (π‘Œ supp 0 )) β†’ (π‘₯( ∘f + β†Ύ ((𝑋 supp 0 ) Γ— (π‘Œ supp 0 )))(π‘˜ ∘f βˆ’ π‘₯)) = (π‘₯ ∘f + (π‘˜ ∘f βˆ’ π‘₯)))
96 fnovrn 7582 . . . . . . . . . . . . . 14 ((( ∘f + β†Ύ ((𝑋 supp 0 ) Γ— (π‘Œ supp 0 ))) Fn ((𝑋 supp 0 ) Γ— (π‘Œ supp 0 )) ∧ π‘₯ ∈ (𝑋 supp 0 ) ∧ (π‘˜ ∘f βˆ’ π‘₯) ∈ (π‘Œ supp 0 )) β†’ (π‘₯( ∘f + β†Ύ ((𝑋 supp 0 ) Γ— (π‘Œ supp 0 )))(π‘˜ ∘f βˆ’ π‘₯)) ∈ ran ( ∘f + β†Ύ ((𝑋 supp 0 ) Γ— (π‘Œ supp 0 ))))
9796, 21eleqtrrdi 2845 . . . . . . . . . . . . 13 ((( ∘f + β†Ύ ((𝑋 supp 0 ) Γ— (π‘Œ supp 0 ))) Fn ((𝑋 supp 0 ) Γ— (π‘Œ supp 0 )) ∧ π‘₯ ∈ (𝑋 supp 0 ) ∧ (π‘˜ ∘f βˆ’ π‘₯) ∈ (π‘Œ supp 0 )) β†’ (π‘₯( ∘f + β†Ύ ((𝑋 supp 0 ) Γ— (π‘Œ supp 0 )))(π‘˜ ∘f βˆ’ π‘₯)) ∈ 𝐴)
9832, 97mp3an1 1449 . . . . . . . . . . . 12 ((π‘₯ ∈ (𝑋 supp 0 ) ∧ (π‘˜ ∘f βˆ’ π‘₯) ∈ (π‘Œ supp 0 )) β†’ (π‘₯( ∘f + β†Ύ ((𝑋 supp 0 ) Γ— (π‘Œ supp 0 )))(π‘˜ ∘f βˆ’ π‘₯)) ∈ 𝐴)
9995, 98eqeltrrd 2835 . . . . . . . . . . 11 ((π‘₯ ∈ (𝑋 supp 0 ) ∧ (π‘˜ ∘f βˆ’ π‘₯) ∈ (π‘Œ supp 0 )) β†’ (π‘₯ ∘f + (π‘˜ ∘f βˆ’ π‘₯)) ∈ 𝐴)
10094, 99nsyl 140 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ Β¬ (π‘₯ ∈ (𝑋 supp 0 ) ∧ (π‘˜ ∘f βˆ’ π‘₯) ∈ (π‘Œ supp 0 )))
101 ianor 981 . . . . . . . . . 10 (Β¬ (π‘₯ ∈ (𝑋 supp 0 ) ∧ (π‘˜ ∘f βˆ’ π‘₯) ∈ (π‘Œ supp 0 )) ↔ (Β¬ π‘₯ ∈ (𝑋 supp 0 ) ∨ Β¬ (π‘˜ ∘f βˆ’ π‘₯) ∈ (π‘Œ supp 0 )))
102100, 101sylib 217 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ (Β¬ π‘₯ ∈ (𝑋 supp 0 ) ∨ Β¬ (π‘˜ ∘f βˆ’ π‘₯) ∈ (π‘Œ supp 0 )))
103 eldif 3959 . . . . . . . . . . . . 13 (π‘₯ ∈ (𝐷 βˆ– (𝑋 supp 0 )) ↔ (π‘₯ ∈ 𝐷 ∧ Β¬ π‘₯ ∈ (𝑋 supp 0 )))
104103baib 537 . . . . . . . . . . . 12 (π‘₯ ∈ 𝐷 β†’ (π‘₯ ∈ (𝐷 βˆ– (𝑋 supp 0 )) ↔ Β¬ π‘₯ ∈ (𝑋 supp 0 )))
10565, 104syl 17 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ (π‘₯ ∈ (𝐷 βˆ– (𝑋 supp 0 )) ↔ Β¬ π‘₯ ∈ (𝑋 supp 0 )))
106 ssidd 4006 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ (𝑋 supp 0 ) βŠ† (𝑋 supp 0 ))
107 ovex 7442 . . . . . . . . . . . . . . 15 (β„•0 ↑m 𝐼) ∈ V
10839, 107rabex2 5335 . . . . . . . . . . . . . 14 𝐷 ∈ V
109108a1i 11 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ 𝐷 ∈ V)
11017a1i 11 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ 0 ∈ V)
11164, 106, 109, 110suppssr 8181 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) ∧ π‘₯ ∈ (𝐷 βˆ– (𝑋 supp 0 ))) β†’ (π‘‹β€˜π‘₯) = 0 )
112111ex 414 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ (π‘₯ ∈ (𝐷 βˆ– (𝑋 supp 0 )) β†’ (π‘‹β€˜π‘₯) = 0 ))
113105, 112sylbird 260 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ (Β¬ π‘₯ ∈ (𝑋 supp 0 ) β†’ (π‘‹β€˜π‘₯) = 0 ))
114 eldif 3959 . . . . . . . . . . . . 13 ((π‘˜ ∘f βˆ’ π‘₯) ∈ (𝐷 βˆ– (π‘Œ supp 0 )) ↔ ((π‘˜ ∘f βˆ’ π‘₯) ∈ 𝐷 ∧ Β¬ (π‘˜ ∘f βˆ’ π‘₯) ∈ (π‘Œ supp 0 )))
115114baib 537 . . . . . . . . . . . 12 ((π‘˜ ∘f βˆ’ π‘₯) ∈ 𝐷 β†’ ((π‘˜ ∘f βˆ’ π‘₯) ∈ (𝐷 βˆ– (π‘Œ supp 0 )) ↔ Β¬ (π‘˜ ∘f βˆ’ π‘₯) ∈ (π‘Œ supp 0 )))
11656, 115syl 17 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ ((π‘˜ ∘f βˆ’ π‘₯) ∈ (𝐷 βˆ– (π‘Œ supp 0 )) ↔ Β¬ (π‘˜ ∘f βˆ’ π‘₯) ∈ (π‘Œ supp 0 )))
117 ssidd 4006 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ (π‘Œ supp 0 ) βŠ† (π‘Œ supp 0 ))
11849, 117, 109, 110suppssr 8181 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) ∧ (π‘˜ ∘f βˆ’ π‘₯) ∈ (𝐷 βˆ– (π‘Œ supp 0 ))) β†’ (π‘Œβ€˜(π‘˜ ∘f βˆ’ π‘₯)) = 0 )
119118ex 414 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ ((π‘˜ ∘f βˆ’ π‘₯) ∈ (𝐷 βˆ– (π‘Œ supp 0 )) β†’ (π‘Œβ€˜(π‘˜ ∘f βˆ’ π‘₯)) = 0 ))
120116, 119sylbird 260 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ (Β¬ (π‘˜ ∘f βˆ’ π‘₯) ∈ (π‘Œ supp 0 ) β†’ (π‘Œβ€˜(π‘˜ ∘f βˆ’ π‘₯)) = 0 ))
121113, 120orim12d 964 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ ((Β¬ π‘₯ ∈ (𝑋 supp 0 ) ∨ Β¬ (π‘˜ ∘f βˆ’ π‘₯) ∈ (π‘Œ supp 0 )) β†’ ((π‘‹β€˜π‘₯) = 0 ∨ (π‘Œβ€˜(π‘˜ ∘f βˆ’ π‘₯)) = 0 )))
122102, 121mpd 15 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ ((π‘‹β€˜π‘₯) = 0 ∨ (π‘Œβ€˜(π‘˜ ∘f βˆ’ π‘₯)) = 0 ))
12362, 71, 122mpjaod 859 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) ∧ π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜}) β†’ ((π‘‹β€˜π‘₯) Β· (π‘Œβ€˜(π‘˜ ∘f βˆ’ π‘₯))) = 0 )
124123mpteq2dva 5249 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) β†’ (π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜} ↦ ((π‘‹β€˜π‘₯) Β· (π‘Œβ€˜(π‘˜ ∘f βˆ’ π‘₯)))) = (π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜} ↦ 0 ))
125124oveq2d 7425 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) β†’ (𝑅 Ξ£g (π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜} ↦ ((π‘‹β€˜π‘₯) Β· (π‘Œβ€˜(π‘˜ ∘f βˆ’ π‘₯))))) = (𝑅 Ξ£g (π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜} ↦ 0 )))
1264adantr 482 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) β†’ 𝑅 ∈ Ring)
127 ringmnd 20066 . . . . . . 7 (𝑅 ∈ Ring β†’ 𝑅 ∈ Mnd)
128126, 127syl 17 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) β†’ 𝑅 ∈ Mnd)
12939psrbaglefi 21485 . . . . . . 7 (π‘˜ ∈ 𝐷 β†’ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜} ∈ Fin)
13045, 129syl 17 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) β†’ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜} ∈ Fin)
13116gsumz 18717 . . . . . 6 ((𝑅 ∈ Mnd ∧ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜} ∈ Fin) β†’ (𝑅 Ξ£g (π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜} ↦ 0 )) = 0 )
132128, 130, 131syl2anc 585 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) β†’ (𝑅 Ξ£g (π‘₯ ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≀ π‘˜} ↦ 0 )) = 0 )
13346, 125, 1323eqtrd 2777 . . . 4 ((πœ‘ ∧ π‘˜ ∈ (𝐷 βˆ– 𝐴)) β†’ ((𝑋(.rβ€˜π‘†)π‘Œ)β€˜π‘˜) = 0 )
13440, 133suppss 8179 . . 3 (πœ‘ β†’ ((𝑋(.rβ€˜π‘†)π‘Œ) supp 0 ) βŠ† 𝐴)
135 suppssfifsupp 9378 . . 3 ((((𝑋(.rβ€˜π‘†)π‘Œ) ∈ V ∧ Fun (𝑋(.rβ€˜π‘†)π‘Œ) ∧ 0 ∈ V) ∧ (𝐴 ∈ Fin ∧ ((𝑋(.rβ€˜π‘†)π‘Œ) supp 0 ) βŠ† 𝐴)) β†’ (𝑋(.rβ€˜π‘†)π‘Œ) finSupp 0 )
13613, 15, 18, 37, 134, 135syl32anc 1379 . 2 (πœ‘ β†’ (𝑋(.rβ€˜π‘†)π‘Œ) finSupp 0 )
1375, 1, 2, 16, 6mplelbas 21550 . 2 ((𝑋(.rβ€˜π‘†)π‘Œ) ∈ π‘ˆ ↔ ((𝑋(.rβ€˜π‘†)π‘Œ) ∈ (Baseβ€˜π‘†) ∧ (𝑋(.rβ€˜π‘†)π‘Œ) finSupp 0 ))
13812, 136, 137sylanbrc 584 1 (πœ‘ β†’ (𝑋(.rβ€˜π‘†)π‘Œ) ∈ π‘ˆ)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  {crab 3433  Vcvv 3475   βˆ– cdif 3946   βŠ† wss 3949   class class class wbr 5149   ↦ cmpt 5232   Γ— cxp 5675  β—‘ccnv 5676  ran crn 5678   β†Ύ cres 5679   β€œ cima 5680  Fun wfun 6538   Fn wfn 6539  βŸΆwf 6540  β€“ontoβ†’wfo 6542  β€˜cfv 6544  (class class class)co 7409   ∘f cof 7668   ∘r cofr 7669   supp csupp 8146   ↑m cmap 8820  Fincfn 8939   finSupp cfsupp 9361  β„‚cc 11108   + caddc 11113   ≀ cle 11249   βˆ’ cmin 11444  β„•cn 12212  β„•0cn0 12472  Basecbs 17144  .rcmulr 17198  0gc0g 17385   Ξ£g cgsu 17386  Mndcmnd 18625  Ringcrg 20056   mPwSer cmps 21457   mPoly cmpl 21459
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-of 7670  df-ofr 7671  df-om 7856  df-1st 7975  df-2nd 7976  df-supp 8147  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-er 8703  df-map 8822  df-pm 8823  df-ixp 8892  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-fsupp 9362  df-oi 9505  df-card 9934  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-nn 12213  df-2 12275  df-3 12276  df-4 12277  df-5 12278  df-6 12279  df-7 12280  df-8 12281  df-9 12282  df-n0 12473  df-z 12559  df-uz 12823  df-fz 13485  df-fzo 13628  df-seq 13967  df-hash 14291  df-struct 17080  df-sets 17097  df-slot 17115  df-ndx 17127  df-base 17145  df-ress 17174  df-plusg 17210  df-mulr 17211  df-sca 17213  df-vsca 17214  df-tset 17216  df-0g 17387  df-gsum 17388  df-mgm 18561  df-sgrp 18610  df-mnd 18626  df-grp 18822  df-minusg 18823  df-cntz 19181  df-cmn 19650  df-abl 19651  df-mgp 19988  df-ur 20005  df-ring 20058  df-psr 21462  df-mpl 21464
This theorem is referenced by:  mplsubrg  21564
  Copyright terms: Public domain W3C validator