Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lincsum Structured version   Visualization version   GIF version

Theorem lincsum 44629
Description: The sum of two linear combinations is a linear combination, see also the proof in [Lang] p. 129. (Contributed by AV, 4-Apr-2019.) (Revised by AV, 28-Jul-2019.)
Hypotheses
Ref Expression
lincsum.p + = (+g𝑀)
lincsum.x 𝑋 = (𝐴( linC ‘𝑀)𝑉)
lincsum.y 𝑌 = (𝐵( linC ‘𝑀)𝑉)
lincsum.s 𝑆 = (Scalar‘𝑀)
lincsum.r 𝑅 = (Base‘𝑆)
lincsum.b = (+g𝑆)
Assertion
Ref Expression
lincsum (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉)) ∧ (𝐴 finSupp (0g𝑆) ∧ 𝐵 finSupp (0g𝑆))) → (𝑋 + 𝑌) = ((𝐴f 𝐵)( linC ‘𝑀)𝑉))

Proof of Theorem lincsum
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2820 . . 3 (Base‘𝑀) = (Base‘𝑀)
2 eqid 2820 . . 3 (0g𝑀) = (0g𝑀)
3 lincsum.p . . 3 + = (+g𝑀)
4 lmodcmn 19658 . . . . 5 (𝑀 ∈ LMod → 𝑀 ∈ CMnd)
54adantr 483 . . . 4 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → 𝑀 ∈ CMnd)
653ad2ant1 1129 . . 3 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉)) ∧ (𝐴 finSupp (0g𝑆) ∧ 𝐵 finSupp (0g𝑆))) → 𝑀 ∈ CMnd)
7 simpr 487 . . . 4 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → 𝑉 ∈ 𝒫 (Base‘𝑀))
873ad2ant1 1129 . . 3 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉)) ∧ (𝐴 finSupp (0g𝑆) ∧ 𝐵 finSupp (0g𝑆))) → 𝑉 ∈ 𝒫 (Base‘𝑀))
9 simpl 485 . . . . . 6 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → 𝑀 ∈ LMod)
1093ad2ant1 1129 . . . . 5 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉)) ∧ (𝐴 finSupp (0g𝑆) ∧ 𝐵 finSupp (0g𝑆))) → 𝑀 ∈ LMod)
1110adantr 483 . . . 4 ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉)) ∧ (𝐴 finSupp (0g𝑆) ∧ 𝐵 finSupp (0g𝑆))) ∧ 𝑥𝑉) → 𝑀 ∈ LMod)
12 elmapi 8406 . . . . . . . 8 (𝐴 ∈ (𝑅m 𝑉) → 𝐴:𝑉𝑅)
13 ffvelrn 6825 . . . . . . . . 9 ((𝐴:𝑉𝑅𝑥𝑉) → (𝐴𝑥) ∈ 𝑅)
1413ex 415 . . . . . . . 8 (𝐴:𝑉𝑅 → (𝑥𝑉 → (𝐴𝑥) ∈ 𝑅))
1512, 14syl 17 . . . . . . 7 (𝐴 ∈ (𝑅m 𝑉) → (𝑥𝑉 → (𝐴𝑥) ∈ 𝑅))
1615adantr 483 . . . . . 6 ((𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉)) → (𝑥𝑉 → (𝐴𝑥) ∈ 𝑅))
17163ad2ant2 1130 . . . . 5 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉)) ∧ (𝐴 finSupp (0g𝑆) ∧ 𝐵 finSupp (0g𝑆))) → (𝑥𝑉 → (𝐴𝑥) ∈ 𝑅))
1817imp 409 . . . 4 ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉)) ∧ (𝐴 finSupp (0g𝑆) ∧ 𝐵 finSupp (0g𝑆))) ∧ 𝑥𝑉) → (𝐴𝑥) ∈ 𝑅)
19 elelpwi 4527 . . . . . . . 8 ((𝑥𝑉𝑉 ∈ 𝒫 (Base‘𝑀)) → 𝑥 ∈ (Base‘𝑀))
2019expcom 416 . . . . . . 7 (𝑉 ∈ 𝒫 (Base‘𝑀) → (𝑥𝑉𝑥 ∈ (Base‘𝑀)))
2120adantl 484 . . . . . 6 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝑥𝑉𝑥 ∈ (Base‘𝑀)))
22213ad2ant1 1129 . . . . 5 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉)) ∧ (𝐴 finSupp (0g𝑆) ∧ 𝐵 finSupp (0g𝑆))) → (𝑥𝑉𝑥 ∈ (Base‘𝑀)))
2322imp 409 . . . 4 ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉)) ∧ (𝐴 finSupp (0g𝑆) ∧ 𝐵 finSupp (0g𝑆))) ∧ 𝑥𝑉) → 𝑥 ∈ (Base‘𝑀))
24 lincsum.s . . . . 5 𝑆 = (Scalar‘𝑀)
25 eqid 2820 . . . . 5 ( ·𝑠𝑀) = ( ·𝑠𝑀)
26 lincsum.r . . . . 5 𝑅 = (Base‘𝑆)
271, 24, 25, 26lmodvscl 19627 . . . 4 ((𝑀 ∈ LMod ∧ (𝐴𝑥) ∈ 𝑅𝑥 ∈ (Base‘𝑀)) → ((𝐴𝑥)( ·𝑠𝑀)𝑥) ∈ (Base‘𝑀))
2811, 18, 23, 27syl3anc 1367 . . 3 ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉)) ∧ (𝐴 finSupp (0g𝑆) ∧ 𝐵 finSupp (0g𝑆))) ∧ 𝑥𝑉) → ((𝐴𝑥)( ·𝑠𝑀)𝑥) ∈ (Base‘𝑀))
29 elmapi 8406 . . . . . . . 8 (𝐵 ∈ (𝑅m 𝑉) → 𝐵:𝑉𝑅)
30 ffvelrn 6825 . . . . . . . . 9 ((𝐵:𝑉𝑅𝑥𝑉) → (𝐵𝑥) ∈ 𝑅)
3130ex 415 . . . . . . . 8 (𝐵:𝑉𝑅 → (𝑥𝑉 → (𝐵𝑥) ∈ 𝑅))
3229, 31syl 17 . . . . . . 7 (𝐵 ∈ (𝑅m 𝑉) → (𝑥𝑉 → (𝐵𝑥) ∈ 𝑅))
3332adantl 484 . . . . . 6 ((𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉)) → (𝑥𝑉 → (𝐵𝑥) ∈ 𝑅))
34333ad2ant2 1130 . . . . 5 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉)) ∧ (𝐴 finSupp (0g𝑆) ∧ 𝐵 finSupp (0g𝑆))) → (𝑥𝑉 → (𝐵𝑥) ∈ 𝑅))
3534imp 409 . . . 4 ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉)) ∧ (𝐴 finSupp (0g𝑆) ∧ 𝐵 finSupp (0g𝑆))) ∧ 𝑥𝑉) → (𝐵𝑥) ∈ 𝑅)
361, 24, 25, 26lmodvscl 19627 . . . 4 ((𝑀 ∈ LMod ∧ (𝐵𝑥) ∈ 𝑅𝑥 ∈ (Base‘𝑀)) → ((𝐵𝑥)( ·𝑠𝑀)𝑥) ∈ (Base‘𝑀))
3711, 35, 23, 36syl3anc 1367 . . 3 ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉)) ∧ (𝐴 finSupp (0g𝑆) ∧ 𝐵 finSupp (0g𝑆))) ∧ 𝑥𝑉) → ((𝐵𝑥)( ·𝑠𝑀)𝑥) ∈ (Base‘𝑀))
38 eqidd 2821 . . 3 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉)) ∧ (𝐴 finSupp (0g𝑆) ∧ 𝐵 finSupp (0g𝑆))) → (𝑥𝑉 ↦ ((𝐴𝑥)( ·𝑠𝑀)𝑥)) = (𝑥𝑉 ↦ ((𝐴𝑥)( ·𝑠𝑀)𝑥)))
39 eqidd 2821 . . 3 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉)) ∧ (𝐴 finSupp (0g𝑆) ∧ 𝐵 finSupp (0g𝑆))) → (𝑥𝑉 ↦ ((𝐵𝑥)( ·𝑠𝑀)𝑥)) = (𝑥𝑉 ↦ ((𝐵𝑥)( ·𝑠𝑀)𝑥)))
40 id 22 . . . 4 ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)))
41 simpl 485 . . . 4 ((𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉)) → 𝐴 ∈ (𝑅m 𝑉))
42 simpl 485 . . . 4 ((𝐴 finSupp (0g𝑆) ∧ 𝐵 finSupp (0g𝑆)) → 𝐴 finSupp (0g𝑆))
4324, 26scmfsupp 44571 . . . 4 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐴 ∈ (𝑅m 𝑉) ∧ 𝐴 finSupp (0g𝑆)) → (𝑥𝑉 ↦ ((𝐴𝑥)( ·𝑠𝑀)𝑥)) finSupp (0g𝑀))
4440, 41, 42, 43syl3an 1156 . . 3 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉)) ∧ (𝐴 finSupp (0g𝑆) ∧ 𝐵 finSupp (0g𝑆))) → (𝑥𝑉 ↦ ((𝐴𝑥)( ·𝑠𝑀)𝑥)) finSupp (0g𝑀))
45 simpr 487 . . . 4 ((𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉)) → 𝐵 ∈ (𝑅m 𝑉))
46 simpr 487 . . . 4 ((𝐴 finSupp (0g𝑆) ∧ 𝐵 finSupp (0g𝑆)) → 𝐵 finSupp (0g𝑆))
4724, 26scmfsupp 44571 . . . 4 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ 𝐵 ∈ (𝑅m 𝑉) ∧ 𝐵 finSupp (0g𝑆)) → (𝑥𝑉 ↦ ((𝐵𝑥)( ·𝑠𝑀)𝑥)) finSupp (0g𝑀))
4840, 45, 46, 47syl3an 1156 . . 3 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉)) ∧ (𝐴 finSupp (0g𝑆) ∧ 𝐵 finSupp (0g𝑆))) → (𝑥𝑉 ↦ ((𝐵𝑥)( ·𝑠𝑀)𝑥)) finSupp (0g𝑀))
491, 2, 3, 6, 8, 28, 37, 38, 39, 44, 48gsummptfsadd 19023 . 2 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉)) ∧ (𝐴 finSupp (0g𝑆) ∧ 𝐵 finSupp (0g𝑆))) → (𝑀 Σg (𝑥𝑉 ↦ (((𝐴𝑥)( ·𝑠𝑀)𝑥) + ((𝐵𝑥)( ·𝑠𝑀)𝑥)))) = ((𝑀 Σg (𝑥𝑉 ↦ ((𝐴𝑥)( ·𝑠𝑀)𝑥))) + (𝑀 Σg (𝑥𝑉 ↦ ((𝐵𝑥)( ·𝑠𝑀)𝑥)))))
507adantr 483 . . . . . . 7 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) → 𝑉 ∈ 𝒫 (Base‘𝑀))
51 elmapfn 8407 . . . . . . . 8 (𝐴 ∈ (𝑅m 𝑉) → 𝐴 Fn 𝑉)
5251ad2antrl 726 . . . . . . 7 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) → 𝐴 Fn 𝑉)
53 elmapfn 8407 . . . . . . . 8 (𝐵 ∈ (𝑅m 𝑉) → 𝐵 Fn 𝑉)
5453ad2antll 727 . . . . . . 7 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) → 𝐵 Fn 𝑉)
5550, 52, 54offvalfv 44536 . . . . . 6 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) → (𝐴f 𝐵) = (𝑦𝑉 ↦ ((𝐴𝑦) (𝐵𝑦))))
56553adant3 1128 . . . . 5 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉)) ∧ (𝐴 finSupp (0g𝑆) ∧ 𝐵 finSupp (0g𝑆))) → (𝐴f 𝐵) = (𝑦𝑉 ↦ ((𝐴𝑦) (𝐵𝑦))))
5724lmodfgrp 19619 . . . . . . . . . . 11 (𝑀 ∈ LMod → 𝑆 ∈ Grp)
58 grpmnd 18089 . . . . . . . . . . 11 (𝑆 ∈ Grp → 𝑆 ∈ Mnd)
5957, 58syl 17 . . . . . . . . . 10 (𝑀 ∈ LMod → 𝑆 ∈ Mnd)
6059ad3antrrr 728 . . . . . . . . 9 ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) ∧ 𝑦𝑉) → 𝑆 ∈ Mnd)
61 ffvelrn 6825 . . . . . . . . . . . . . 14 ((𝐴:𝑉𝑅𝑦𝑉) → (𝐴𝑦) ∈ 𝑅)
6261ex 415 . . . . . . . . . . . . 13 (𝐴:𝑉𝑅 → (𝑦𝑉 → (𝐴𝑦) ∈ 𝑅))
6312, 62syl 17 . . . . . . . . . . . 12 (𝐴 ∈ (𝑅m 𝑉) → (𝑦𝑉 → (𝐴𝑦) ∈ 𝑅))
6463ad2antrl 726 . . . . . . . . . . 11 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) → (𝑦𝑉 → (𝐴𝑦) ∈ 𝑅))
6564imp 409 . . . . . . . . . 10 ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) ∧ 𝑦𝑉) → (𝐴𝑦) ∈ 𝑅)
6624fveq2i 6649 . . . . . . . . . . 11 (Base‘𝑆) = (Base‘(Scalar‘𝑀))
6726, 66eqtri 2843 . . . . . . . . . 10 𝑅 = (Base‘(Scalar‘𝑀))
6865, 67eleqtrdi 2921 . . . . . . . . 9 ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) ∧ 𝑦𝑉) → (𝐴𝑦) ∈ (Base‘(Scalar‘𝑀)))
69 ffvelrn 6825 . . . . . . . . . . . . . 14 ((𝐵:𝑉𝑅𝑦𝑉) → (𝐵𝑦) ∈ 𝑅)
7069, 67eleqtrdi 2921 . . . . . . . . . . . . 13 ((𝐵:𝑉𝑅𝑦𝑉) → (𝐵𝑦) ∈ (Base‘(Scalar‘𝑀)))
7170ex 415 . . . . . . . . . . . 12 (𝐵:𝑉𝑅 → (𝑦𝑉 → (𝐵𝑦) ∈ (Base‘(Scalar‘𝑀))))
7229, 71syl 17 . . . . . . . . . . 11 (𝐵 ∈ (𝑅m 𝑉) → (𝑦𝑉 → (𝐵𝑦) ∈ (Base‘(Scalar‘𝑀))))
7372ad2antll 727 . . . . . . . . . 10 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) → (𝑦𝑉 → (𝐵𝑦) ∈ (Base‘(Scalar‘𝑀))))
7473imp 409 . . . . . . . . 9 ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) ∧ 𝑦𝑉) → (𝐵𝑦) ∈ (Base‘(Scalar‘𝑀)))
7524eqcomi 2829 . . . . . . . . . . 11 (Scalar‘𝑀) = 𝑆
7675fveq2i 6649 . . . . . . . . . 10 (Base‘(Scalar‘𝑀)) = (Base‘𝑆)
77 lincsum.b . . . . . . . . . 10 = (+g𝑆)
7876, 77mndcl 17898 . . . . . . . . 9 ((𝑆 ∈ Mnd ∧ (𝐴𝑦) ∈ (Base‘(Scalar‘𝑀)) ∧ (𝐵𝑦) ∈ (Base‘(Scalar‘𝑀))) → ((𝐴𝑦) (𝐵𝑦)) ∈ (Base‘(Scalar‘𝑀)))
7960, 68, 74, 78syl3anc 1367 . . . . . . . 8 ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) ∧ 𝑦𝑉) → ((𝐴𝑦) (𝐵𝑦)) ∈ (Base‘(Scalar‘𝑀)))
8079fmpttd 6855 . . . . . . 7 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) → (𝑦𝑉 ↦ ((𝐴𝑦) (𝐵𝑦))):𝑉⟶(Base‘(Scalar‘𝑀)))
81 fvex 6659 . . . . . . . 8 (Base‘(Scalar‘𝑀)) ∈ V
82 elmapg 8397 . . . . . . . 8 (((Base‘(Scalar‘𝑀)) ∈ V ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ((𝑦𝑉 ↦ ((𝐴𝑦) (𝐵𝑦))) ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ↔ (𝑦𝑉 ↦ ((𝐴𝑦) (𝐵𝑦))):𝑉⟶(Base‘(Scalar‘𝑀))))
8381, 50, 82sylancr 589 . . . . . . 7 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) → ((𝑦𝑉 ↦ ((𝐴𝑦) (𝐵𝑦))) ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ↔ (𝑦𝑉 ↦ ((𝐴𝑦) (𝐵𝑦))):𝑉⟶(Base‘(Scalar‘𝑀))))
8480, 83mpbird 259 . . . . . 6 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) → (𝑦𝑉 ↦ ((𝐴𝑦) (𝐵𝑦))) ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉))
85843adant3 1128 . . . . 5 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉)) ∧ (𝐴 finSupp (0g𝑆) ∧ 𝐵 finSupp (0g𝑆))) → (𝑦𝑉 ↦ ((𝐴𝑦) (𝐵𝑦))) ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉))
8656, 85eqeltrd 2911 . . . 4 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉)) ∧ (𝐴 finSupp (0g𝑆) ∧ 𝐵 finSupp (0g𝑆))) → (𝐴f 𝐵) ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉))
87 lincval 44609 . . . 4 ((𝑀 ∈ LMod ∧ (𝐴f 𝐵) ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ((𝐴f 𝐵)( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥𝑉 ↦ (((𝐴f 𝐵)‘𝑥)( ·𝑠𝑀)𝑥))))
8810, 86, 8, 87syl3anc 1367 . . 3 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉)) ∧ (𝐴 finSupp (0g𝑆) ∧ 𝐵 finSupp (0g𝑆))) → ((𝐴f 𝐵)( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥𝑉 ↦ (((𝐴f 𝐵)‘𝑥)( ·𝑠𝑀)𝑥))))
8951, 53anim12i 614 . . . . . . . . . . . 12 ((𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉)) → (𝐴 Fn 𝑉𝐵 Fn 𝑉))
9089adantl 484 . . . . . . . . . . 11 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) → (𝐴 Fn 𝑉𝐵 Fn 𝑉))
9190adantr 483 . . . . . . . . . 10 ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) ∧ 𝑥𝑉) → (𝐴 Fn 𝑉𝐵 Fn 𝑉))
9250anim1i 616 . . . . . . . . . 10 ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) ∧ 𝑥𝑉) → (𝑉 ∈ 𝒫 (Base‘𝑀) ∧ 𝑥𝑉))
93 fnfvof 7401 . . . . . . . . . 10 (((𝐴 Fn 𝑉𝐵 Fn 𝑉) ∧ (𝑉 ∈ 𝒫 (Base‘𝑀) ∧ 𝑥𝑉)) → ((𝐴f 𝐵)‘𝑥) = ((𝐴𝑥) (𝐵𝑥)))
9491, 92, 93syl2anc 586 . . . . . . . . 9 ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) ∧ 𝑥𝑉) → ((𝐴f 𝐵)‘𝑥) = ((𝐴𝑥) (𝐵𝑥)))
9577a1i 11 . . . . . . . . . 10 ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) ∧ 𝑥𝑉) → = (+g𝑆))
9695oveqd 7150 . . . . . . . . 9 ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) ∧ 𝑥𝑉) → ((𝐴𝑥) (𝐵𝑥)) = ((𝐴𝑥)(+g𝑆)(𝐵𝑥)))
9794, 96eqtrd 2855 . . . . . . . 8 ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) ∧ 𝑥𝑉) → ((𝐴f 𝐵)‘𝑥) = ((𝐴𝑥)(+g𝑆)(𝐵𝑥)))
9897oveq1d 7148 . . . . . . 7 ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) ∧ 𝑥𝑉) → (((𝐴f 𝐵)‘𝑥)( ·𝑠𝑀)𝑥) = (((𝐴𝑥)(+g𝑆)(𝐵𝑥))( ·𝑠𝑀)𝑥))
999adantr 483 . . . . . . . . 9 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) → 𝑀 ∈ LMod)
10099adantr 483 . . . . . . . 8 ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) ∧ 𝑥𝑉) → 𝑀 ∈ LMod)
10115ad2antrl 726 . . . . . . . . 9 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) → (𝑥𝑉 → (𝐴𝑥) ∈ 𝑅))
102101imp 409 . . . . . . . 8 ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) ∧ 𝑥𝑉) → (𝐴𝑥) ∈ 𝑅)
10332ad2antll 727 . . . . . . . . 9 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) → (𝑥𝑉 → (𝐵𝑥) ∈ 𝑅))
104103imp 409 . . . . . . . 8 ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) ∧ 𝑥𝑉) → (𝐵𝑥) ∈ 𝑅)
10521adantr 483 . . . . . . . . 9 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) → (𝑥𝑉𝑥 ∈ (Base‘𝑀)))
106105imp 409 . . . . . . . 8 ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) ∧ 𝑥𝑉) → 𝑥 ∈ (Base‘𝑀))
107 eqid 2820 . . . . . . . . 9 (Scalar‘𝑀) = (Scalar‘𝑀)
10824fveq2i 6649 . . . . . . . . 9 (+g𝑆) = (+g‘(Scalar‘𝑀))
1091, 3, 107, 25, 67, 108lmodvsdir 19634 . . . . . . . 8 ((𝑀 ∈ LMod ∧ ((𝐴𝑥) ∈ 𝑅 ∧ (𝐵𝑥) ∈ 𝑅𝑥 ∈ (Base‘𝑀))) → (((𝐴𝑥)(+g𝑆)(𝐵𝑥))( ·𝑠𝑀)𝑥) = (((𝐴𝑥)( ·𝑠𝑀)𝑥) + ((𝐵𝑥)( ·𝑠𝑀)𝑥)))
110100, 102, 104, 106, 109syl13anc 1368 . . . . . . 7 ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) ∧ 𝑥𝑉) → (((𝐴𝑥)(+g𝑆)(𝐵𝑥))( ·𝑠𝑀)𝑥) = (((𝐴𝑥)( ·𝑠𝑀)𝑥) + ((𝐵𝑥)( ·𝑠𝑀)𝑥)))
11198, 110eqtrd 2855 . . . . . 6 ((((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) ∧ 𝑥𝑉) → (((𝐴f 𝐵)‘𝑥)( ·𝑠𝑀)𝑥) = (((𝐴𝑥)( ·𝑠𝑀)𝑥) + ((𝐵𝑥)( ·𝑠𝑀)𝑥)))
112111mpteq2dva 5137 . . . . 5 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) → (𝑥𝑉 ↦ (((𝐴f 𝐵)‘𝑥)( ·𝑠𝑀)𝑥)) = (𝑥𝑉 ↦ (((𝐴𝑥)( ·𝑠𝑀)𝑥) + ((𝐵𝑥)( ·𝑠𝑀)𝑥))))
113112oveq2d 7149 . . . 4 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) → (𝑀 Σg (𝑥𝑉 ↦ (((𝐴f 𝐵)‘𝑥)( ·𝑠𝑀)𝑥))) = (𝑀 Σg (𝑥𝑉 ↦ (((𝐴𝑥)( ·𝑠𝑀)𝑥) + ((𝐵𝑥)( ·𝑠𝑀)𝑥)))))
1141133adant3 1128 . . 3 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉)) ∧ (𝐴 finSupp (0g𝑆) ∧ 𝐵 finSupp (0g𝑆))) → (𝑀 Σg (𝑥𝑉 ↦ (((𝐴f 𝐵)‘𝑥)( ·𝑠𝑀)𝑥))) = (𝑀 Σg (𝑥𝑉 ↦ (((𝐴𝑥)( ·𝑠𝑀)𝑥) + ((𝐵𝑥)( ·𝑠𝑀)𝑥)))))
11588, 114eqtrd 2855 . 2 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉)) ∧ (𝐴 finSupp (0g𝑆) ∧ 𝐵 finSupp (0g𝑆))) → ((𝐴f 𝐵)( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥𝑉 ↦ (((𝐴𝑥)( ·𝑠𝑀)𝑥) + ((𝐵𝑥)( ·𝑠𝑀)𝑥)))))
116 lincsum.x . . . 4 𝑋 = (𝐴( linC ‘𝑀)𝑉)
117 lincsum.y . . . 4 𝑌 = (𝐵( linC ‘𝑀)𝑉)
118116, 117oveq12i 7145 . . 3 (𝑋 + 𝑌) = ((𝐴( linC ‘𝑀)𝑉) + (𝐵( linC ‘𝑀)𝑉))
11967oveq1i 7143 . . . . . . . . 9 (𝑅m 𝑉) = ((Base‘(Scalar‘𝑀)) ↑m 𝑉)
120119eleq2i 2902 . . . . . . . 8 (𝐴 ∈ (𝑅m 𝑉) ↔ 𝐴 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉))
121120biimpi 218 . . . . . . 7 (𝐴 ∈ (𝑅m 𝑉) → 𝐴 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉))
122121ad2antrl 726 . . . . . 6 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) → 𝐴 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉))
123 lincval 44609 . . . . . 6 ((𝑀 ∈ LMod ∧ 𝐴 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝐴( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥𝑉 ↦ ((𝐴𝑥)( ·𝑠𝑀)𝑥))))
12499, 122, 50, 123syl3anc 1367 . . . . 5 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) → (𝐴( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥𝑉 ↦ ((𝐴𝑥)( ·𝑠𝑀)𝑥))))
125119eleq2i 2902 . . . . . . . 8 (𝐵 ∈ (𝑅m 𝑉) ↔ 𝐵 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉))
126125biimpi 218 . . . . . . 7 (𝐵 ∈ (𝑅m 𝑉) → 𝐵 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉))
127126ad2antll 727 . . . . . 6 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) → 𝐵 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉))
128 lincval 44609 . . . . . 6 ((𝑀 ∈ LMod ∧ 𝐵 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝐵( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥𝑉 ↦ ((𝐵𝑥)( ·𝑠𝑀)𝑥))))
12999, 127, 50, 128syl3anc 1367 . . . . 5 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) → (𝐵( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥𝑉 ↦ ((𝐵𝑥)( ·𝑠𝑀)𝑥))))
130124, 129oveq12d 7151 . . . 4 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉))) → ((𝐴( linC ‘𝑀)𝑉) + (𝐵( linC ‘𝑀)𝑉)) = ((𝑀 Σg (𝑥𝑉 ↦ ((𝐴𝑥)( ·𝑠𝑀)𝑥))) + (𝑀 Σg (𝑥𝑉 ↦ ((𝐵𝑥)( ·𝑠𝑀)𝑥)))))
1311303adant3 1128 . . 3 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉)) ∧ (𝐴 finSupp (0g𝑆) ∧ 𝐵 finSupp (0g𝑆))) → ((𝐴( linC ‘𝑀)𝑉) + (𝐵( linC ‘𝑀)𝑉)) = ((𝑀 Σg (𝑥𝑉 ↦ ((𝐴𝑥)( ·𝑠𝑀)𝑥))) + (𝑀 Σg (𝑥𝑉 ↦ ((𝐵𝑥)( ·𝑠𝑀)𝑥)))))
132118, 131syl5eq 2867 . 2 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉)) ∧ (𝐴 finSupp (0g𝑆) ∧ 𝐵 finSupp (0g𝑆))) → (𝑋 + 𝑌) = ((𝑀 Σg (𝑥𝑉 ↦ ((𝐴𝑥)( ·𝑠𝑀)𝑥))) + (𝑀 Σg (𝑥𝑉 ↦ ((𝐵𝑥)( ·𝑠𝑀)𝑥)))))
13349, 115, 1323eqtr4rd 2866 1 (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅m 𝑉) ∧ 𝐵 ∈ (𝑅m 𝑉)) ∧ (𝐴 finSupp (0g𝑆) ∧ 𝐵 finSupp (0g𝑆))) → (𝑋 + 𝑌) = ((𝐴f 𝐵)( linC ‘𝑀)𝑉))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398  w3a 1083   = wceq 1537  wcel 2114  Vcvv 3473  𝒫 cpw 4515   class class class wbr 5042  cmpt 5122   Fn wfn 6326  wf 6327  cfv 6331  (class class class)co 7133  f cof 7385  m cmap 8384   finSupp cfsupp 8811  Basecbs 16462  +gcplusg 16544  Scalarcsca 16547   ·𝑠 cvsca 16548  0gc0g 16692   Σg cgsu 16693  Mndcmnd 17890  Grpcgrp 18082  CMndccmn 18885  LModclmod 19610   linC clinc 44604
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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5242  ax-pr 5306  ax-un 7439  ax-cnex 10571  ax-resscn 10572  ax-1cn 10573  ax-icn 10574  ax-addcl 10575  ax-addrcl 10576  ax-mulcl 10577  ax-mulrcl 10578  ax-mulcom 10579  ax-addass 10580  ax-mulass 10581  ax-distr 10582  ax-i2m1 10583  ax-1ne0 10584  ax-1rid 10585  ax-rnegex 10586  ax-rrecex 10587  ax-cnre 10588  ax-pre-lttri 10589  ax-pre-lttrn 10590  ax-pre-ltadd 10591  ax-pre-mulgt0 10592
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-nel 3111  df-ral 3130  df-rex 3131  df-reu 3132  df-rmo 3133  df-rab 3134  df-v 3475  df-sbc 3753  df-csb 3861  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4270  df-if 4444  df-pw 4517  df-sn 4544  df-pr 4546  df-tp 4548  df-op 4550  df-uni 4815  df-int 4853  df-iun 4897  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5436  df-eprel 5441  df-po 5450  df-so 5451  df-fr 5490  df-se 5491  df-we 5492  df-xp 5537  df-rel 5538  df-cnv 5539  df-co 5540  df-dm 5541  df-rn 5542  df-res 5543  df-ima 5544  df-pred 6124  df-ord 6170  df-on 6171  df-lim 6172  df-suc 6173  df-iota 6290  df-fun 6333  df-fn 6334  df-f 6335  df-f1 6336  df-fo 6337  df-f1o 6338  df-fv 6339  df-isom 6340  df-riota 7091  df-ov 7136  df-oprab 7137  df-mpo 7138  df-of 7387  df-om 7559  df-1st 7667  df-2nd 7668  df-supp 7809  df-wrecs 7925  df-recs 7986  df-rdg 8024  df-1o 8080  df-oadd 8084  df-er 8267  df-map 8386  df-en 8488  df-dom 8489  df-sdom 8490  df-fin 8491  df-fsupp 8812  df-oi 8952  df-card 9346  df-pnf 10655  df-mnf 10656  df-xr 10657  df-ltxr 10658  df-le 10659  df-sub 10850  df-neg 10851  df-nn 11617  df-2 11679  df-n0 11877  df-z 11961  df-uz 12223  df-fz 12877  df-fzo 13018  df-seq 13354  df-hash 13676  df-ndx 16465  df-slot 16466  df-base 16468  df-sets 16469  df-ress 16470  df-plusg 16557  df-0g 16694  df-gsum 16695  df-mgm 17831  df-sgrp 17880  df-mnd 17891  df-submnd 17936  df-grp 18085  df-minusg 18086  df-cntz 18426  df-cmn 18887  df-abl 18888  df-mgp 19219  df-ur 19231  df-ring 19278  df-lmod 19612  df-linc 44606
This theorem is referenced by:  lincsumcl  44631
  Copyright terms: Public domain W3C validator