Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  gsumvsca2 Structured version   Visualization version   GIF version
Theorem gsumvsca2 32360
Description: Scalar product of a finite group sum for a left module over a semiring. (Contributed by Thierry Arnoux, 16-Mar-2018.) (Proof shortened by AV, 12-Dec-2019.)
Hypotheses
Ref Expression
gsumvsca.b 𝐡 = (Baseβ€˜π‘Š)
gsumvsca.g 𝐺 = (Scalarβ€˜π‘Š)
gsumvsca.z 0 = (0gβ€˜π‘Š)
gsumvsca.t Β· = ( ·𝑠 β€˜π‘Š)
gsumvsca.p + = (+gβ€˜π‘Š)
gsumvsca.k (πœ‘ β†’ 𝐾 βŠ† (Baseβ€˜πΊ))
gsumvsca.a (πœ‘ β†’ 𝐴 ∈ Fin)
gsumvsca.w (πœ‘ β†’ π‘Š ∈ SLMod)
gsumvsca2.n (πœ‘ β†’ 𝑄 ∈ 𝐡)
gsumvsca2.c ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ 𝑃 ∈ 𝐾)
Assertion
Ref Expression
gsumvsca2 (πœ‘ β†’ (π‘Š Ξ£g (π‘˜ ∈ 𝐴 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝐴 ↦ 𝑃)) Β· 𝑄))
Distinct variable groups:   Β· ,π‘˜   𝐴,π‘˜   π‘˜,π‘Š   πœ‘,π‘˜   𝐡,π‘˜   π‘˜,𝐺   π‘˜,𝐾   𝑄,π‘˜
Allowed substitution hints:   𝑃(π‘˜)   + (π‘˜)   0 (π‘˜)
Proof of Theorem gsumvsca2
Dummy variables 𝑒 π‘Ž 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 gsumvsca.a . 2 (πœ‘ β†’ 𝐴 ∈ Fin)
2 ssid 4004 . . 3 𝐴 βŠ† 𝐴
3 sseq1 4007 . . . . . . 7 (π‘Ž = βˆ… β†’ (π‘Ž βŠ† 𝐴 ↔ βˆ… βŠ† 𝐴))
43anbi2d 630 . . . . . 6 (π‘Ž = βˆ… β†’ ((πœ‘ ∧ π‘Ž βŠ† 𝐴) ↔ (πœ‘ ∧ βˆ… βŠ† 𝐴)))
5 mpteq1 5241 . . . . . . . 8 (π‘Ž = βˆ… β†’ (π‘˜ ∈ π‘Ž ↦ (𝑃 Β· 𝑄)) = (π‘˜ ∈ βˆ… ↦ (𝑃 Β· 𝑄)))
65oveq2d 7422 . . . . . . 7 (π‘Ž = βˆ… β†’ (π‘Š Ξ£g (π‘˜ ∈ π‘Ž ↦ (𝑃 Β· 𝑄))) = (π‘Š Ξ£g (π‘˜ ∈ βˆ… ↦ (𝑃 Β· 𝑄))))
7 mpteq1 5241 . . . . . . . . 9 (π‘Ž = βˆ… β†’ (π‘˜ ∈ π‘Ž ↦ 𝑃) = (π‘˜ ∈ βˆ… ↦ 𝑃))
87oveq2d 7422 . . . . . . . 8 (π‘Ž = βˆ… β†’ (𝐺 Ξ£g (π‘˜ ∈ π‘Ž ↦ 𝑃)) = (𝐺 Ξ£g (π‘˜ ∈ βˆ… ↦ 𝑃)))
98oveq1d 7421 . . . . . . 7 (π‘Ž = βˆ… β†’ ((𝐺 Ξ£g (π‘˜ ∈ π‘Ž ↦ 𝑃)) Β· 𝑄) = ((𝐺 Ξ£g (π‘˜ ∈ βˆ… ↦ 𝑃)) Β· 𝑄))
106, 9eqeq12d 2749 . . . . . 6 (π‘Ž = βˆ… β†’ ((π‘Š Ξ£g (π‘˜ ∈ π‘Ž ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ π‘Ž ↦ 𝑃)) Β· 𝑄) ↔ (π‘Š Ξ£g (π‘˜ ∈ βˆ… ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ βˆ… ↦ 𝑃)) Β· 𝑄)))
114, 10imbi12d 345 . . . . 5 (π‘Ž = βˆ… β†’ (((πœ‘ ∧ π‘Ž βŠ† 𝐴) β†’ (π‘Š Ξ£g (π‘˜ ∈ π‘Ž ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ π‘Ž ↦ 𝑃)) Β· 𝑄)) ↔ ((πœ‘ ∧ βˆ… βŠ† 𝐴) β†’ (π‘Š Ξ£g (π‘˜ ∈ βˆ… ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ βˆ… ↦ 𝑃)) Β· 𝑄))))
12 sseq1 4007 . . . . . . 7 (π‘Ž = 𝑒 β†’ (π‘Ž βŠ† 𝐴 ↔ 𝑒 βŠ† 𝐴))
1312anbi2d 630 . . . . . 6 (π‘Ž = 𝑒 β†’ ((πœ‘ ∧ π‘Ž βŠ† 𝐴) ↔ (πœ‘ ∧ 𝑒 βŠ† 𝐴)))
14 mpteq1 5241 . . . . . . . 8 (π‘Ž = 𝑒 β†’ (π‘˜ ∈ π‘Ž ↦ (𝑃 Β· 𝑄)) = (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄)))
1514oveq2d 7422 . . . . . . 7 (π‘Ž = 𝑒 β†’ (π‘Š Ξ£g (π‘˜ ∈ π‘Ž ↦ (𝑃 Β· 𝑄))) = (π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))))
16 mpteq1 5241 . . . . . . . . 9 (π‘Ž = 𝑒 β†’ (π‘˜ ∈ π‘Ž ↦ 𝑃) = (π‘˜ ∈ 𝑒 ↦ 𝑃))
1716oveq2d 7422 . . . . . . . 8 (π‘Ž = 𝑒 β†’ (𝐺 Ξ£g (π‘˜ ∈ π‘Ž ↦ 𝑃)) = (𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)))
1817oveq1d 7421 . . . . . . 7 (π‘Ž = 𝑒 β†’ ((𝐺 Ξ£g (π‘˜ ∈ π‘Ž ↦ 𝑃)) Β· 𝑄) = ((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄))
1915, 18eqeq12d 2749 . . . . . 6 (π‘Ž = 𝑒 β†’ ((π‘Š Ξ£g (π‘˜ ∈ π‘Ž ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ π‘Ž ↦ 𝑃)) Β· 𝑄) ↔ (π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄)))
2013, 19imbi12d 345 . . . . 5 (π‘Ž = 𝑒 β†’ (((πœ‘ ∧ π‘Ž βŠ† 𝐴) β†’ (π‘Š Ξ£g (π‘˜ ∈ π‘Ž ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ π‘Ž ↦ 𝑃)) Β· 𝑄)) ↔ ((πœ‘ ∧ 𝑒 βŠ† 𝐴) β†’ (π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄))))
21 sseq1 4007 . . . . . . 7 (π‘Ž = (𝑒 βˆͺ {𝑧}) β†’ (π‘Ž βŠ† 𝐴 ↔ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴))
2221anbi2d 630 . . . . . 6 (π‘Ž = (𝑒 βˆͺ {𝑧}) β†’ ((πœ‘ ∧ π‘Ž βŠ† 𝐴) ↔ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)))
23 mpteq1 5241 . . . . . . . 8 (π‘Ž = (𝑒 βˆͺ {𝑧}) β†’ (π‘˜ ∈ π‘Ž ↦ (𝑃 Β· 𝑄)) = (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ (𝑃 Β· 𝑄)))
2423oveq2d 7422 . . . . . . 7 (π‘Ž = (𝑒 βˆͺ {𝑧}) β†’ (π‘Š Ξ£g (π‘˜ ∈ π‘Ž ↦ (𝑃 Β· 𝑄))) = (π‘Š Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ (𝑃 Β· 𝑄))))
25 mpteq1 5241 . . . . . . . . 9 (π‘Ž = (𝑒 βˆͺ {𝑧}) β†’ (π‘˜ ∈ π‘Ž ↦ 𝑃) = (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ 𝑃))
2625oveq2d 7422 . . . . . . . 8 (π‘Ž = (𝑒 βˆͺ {𝑧}) β†’ (𝐺 Ξ£g (π‘˜ ∈ π‘Ž ↦ 𝑃)) = (𝐺 Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ 𝑃)))
2726oveq1d 7421 . . . . . . 7 (π‘Ž = (𝑒 βˆͺ {𝑧}) β†’ ((𝐺 Ξ£g (π‘˜ ∈ π‘Ž ↦ 𝑃)) Β· 𝑄) = ((𝐺 Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ 𝑃)) Β· 𝑄))
2824, 27eqeq12d 2749 . . . . . 6 (π‘Ž = (𝑒 βˆͺ {𝑧}) β†’ ((π‘Š Ξ£g (π‘˜ ∈ π‘Ž ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ π‘Ž ↦ 𝑃)) Β· 𝑄) ↔ (π‘Š Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ 𝑃)) Β· 𝑄)))
2922, 28imbi12d 345 . . . . 5 (π‘Ž = (𝑒 βˆͺ {𝑧}) β†’ (((πœ‘ ∧ π‘Ž βŠ† 𝐴) β†’ (π‘Š Ξ£g (π‘˜ ∈ π‘Ž ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ π‘Ž ↦ 𝑃)) Β· 𝑄)) ↔ ((πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴) β†’ (π‘Š Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ 𝑃)) Β· 𝑄))))
30 sseq1 4007 . . . . . . 7 (π‘Ž = 𝐴 β†’ (π‘Ž βŠ† 𝐴 ↔ 𝐴 βŠ† 𝐴))
3130anbi2d 630 . . . . . 6 (π‘Ž = 𝐴 β†’ ((πœ‘ ∧ π‘Ž βŠ† 𝐴) ↔ (πœ‘ ∧ 𝐴 βŠ† 𝐴)))
32 mpteq1 5241 . . . . . . . 8 (π‘Ž = 𝐴 β†’ (π‘˜ ∈ π‘Ž ↦ (𝑃 Β· 𝑄)) = (π‘˜ ∈ 𝐴 ↦ (𝑃 Β· 𝑄)))
3332oveq2d 7422 . . . . . . 7 (π‘Ž = 𝐴 β†’ (π‘Š Ξ£g (π‘˜ ∈ π‘Ž ↦ (𝑃 Β· 𝑄))) = (π‘Š Ξ£g (π‘˜ ∈ 𝐴 ↦ (𝑃 Β· 𝑄))))
34 mpteq1 5241 . . . . . . . . 9 (π‘Ž = 𝐴 β†’ (π‘˜ ∈ π‘Ž ↦ 𝑃) = (π‘˜ ∈ 𝐴 ↦ 𝑃))
3534oveq2d 7422 . . . . . . . 8 (π‘Ž = 𝐴 β†’ (𝐺 Ξ£g (π‘˜ ∈ π‘Ž ↦ 𝑃)) = (𝐺 Ξ£g (π‘˜ ∈ 𝐴 ↦ 𝑃)))
3635oveq1d 7421 . . . . . . 7 (π‘Ž = 𝐴 β†’ ((𝐺 Ξ£g (π‘˜ ∈ π‘Ž ↦ 𝑃)) Β· 𝑄) = ((𝐺 Ξ£g (π‘˜ ∈ 𝐴 ↦ 𝑃)) Β· 𝑄))
3733, 36eqeq12d 2749 . . . . . 6 (π‘Ž = 𝐴 β†’ ((π‘Š Ξ£g (π‘˜ ∈ π‘Ž ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ π‘Ž ↦ 𝑃)) Β· 𝑄) ↔ (π‘Š Ξ£g (π‘˜ ∈ 𝐴 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝐴 ↦ 𝑃)) Β· 𝑄)))
3831, 37imbi12d 345 . . . . 5 (π‘Ž = 𝐴 β†’ (((πœ‘ ∧ π‘Ž βŠ† 𝐴) β†’ (π‘Š Ξ£g (π‘˜ ∈ π‘Ž ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ π‘Ž ↦ 𝑃)) Β· 𝑄)) ↔ ((πœ‘ ∧ 𝐴 βŠ† 𝐴) β†’ (π‘Š Ξ£g (π‘˜ ∈ 𝐴 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝐴 ↦ 𝑃)) Β· 𝑄))))
39 gsumvsca.w . . . . . . . . 9 (πœ‘ β†’ π‘Š ∈ SLMod)
40 gsumvsca2.n . . . . . . . . 9 (πœ‘ β†’ 𝑄 ∈ 𝐡)
41 gsumvsca.b . . . . . . . . . 10 𝐡 = (Baseβ€˜π‘Š)
42 gsumvsca.g . . . . . . . . . 10 𝐺 = (Scalarβ€˜π‘Š)
43 gsumvsca.t . . . . . . . . . 10 Β· = ( ·𝑠 β€˜π‘Š)
44 eqid 2733 . . . . . . . . . 10 (0gβ€˜πΊ) = (0gβ€˜πΊ)
45 gsumvsca.z . . . . . . . . . 10 0 = (0gβ€˜π‘Š)
4641, 42, 43, 44, 45slmd0vs 32357 . . . . . . . . 9 ((π‘Š ∈ SLMod ∧ 𝑄 ∈ 𝐡) β†’ ((0gβ€˜πΊ) Β· 𝑄) = 0 )
4739, 40, 46syl2anc 585 . . . . . . . 8 (πœ‘ β†’ ((0gβ€˜πΊ) Β· 𝑄) = 0 )
4847eqcomd 2739 . . . . . . 7 (πœ‘ β†’ 0 = ((0gβ€˜πΊ) Β· 𝑄))
49 mpt0 6690 . . . . . . . . 9 (π‘˜ ∈ βˆ… ↦ (𝑃 Β· 𝑄)) = βˆ…
5049oveq2i 7417 . . . . . . . 8 (π‘Š Ξ£g (π‘˜ ∈ βˆ… ↦ (𝑃 Β· 𝑄))) = (π‘Š Ξ£g βˆ…)
5145gsum0 18600 . . . . . . . 8 (π‘Š Ξ£g βˆ…) = 0
5250, 51eqtri 2761 . . . . . . 7 (π‘Š Ξ£g (π‘˜ ∈ βˆ… ↦ (𝑃 Β· 𝑄))) = 0
53 mpt0 6690 . . . . . . . . . 10 (π‘˜ ∈ βˆ… ↦ 𝑃) = βˆ…
5453oveq2i 7417 . . . . . . . . 9 (𝐺 Ξ£g (π‘˜ ∈ βˆ… ↦ 𝑃)) = (𝐺 Ξ£g βˆ…)
5544gsum0 18600 . . . . . . . . 9 (𝐺 Ξ£g βˆ…) = (0gβ€˜πΊ)
5654, 55eqtri 2761 . . . . . . . 8 (𝐺 Ξ£g (π‘˜ ∈ βˆ… ↦ 𝑃)) = (0gβ€˜πΊ)
5756oveq1i 7416 . . . . . . 7 ((𝐺 Ξ£g (π‘˜ ∈ βˆ… ↦ 𝑃)) Β· 𝑄) = ((0gβ€˜πΊ) Β· 𝑄)
5848, 52, 573eqtr4g 2798 . . . . . 6 (πœ‘ β†’ (π‘Š Ξ£g (π‘˜ ∈ βˆ… ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ βˆ… ↦ 𝑃)) Β· 𝑄))
5958adantr 482 . . . . 5 ((πœ‘ ∧ βˆ… βŠ† 𝐴) β†’ (π‘Š Ξ£g (π‘˜ ∈ βˆ… ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ βˆ… ↦ 𝑃)) Β· 𝑄))
60 ssun1 4172 . . . . . . . . 9 𝑒 βŠ† (𝑒 βˆͺ {𝑧})
61 sstr2 3989 . . . . . . . . 9 (𝑒 βŠ† (𝑒 βˆͺ {𝑧}) β†’ ((𝑒 βˆͺ {𝑧}) βŠ† 𝐴 β†’ 𝑒 βŠ† 𝐴))
6260, 61ax-mp 5 . . . . . . . 8 ((𝑒 βˆͺ {𝑧}) βŠ† 𝐴 β†’ 𝑒 βŠ† 𝐴)
6362anim2i 618 . . . . . . 7 ((πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴) β†’ (πœ‘ ∧ 𝑒 βŠ† 𝐴))
6463imim1i 63 . . . . . 6 (((πœ‘ ∧ 𝑒 βŠ† 𝐴) β†’ (π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄)) β†’ ((πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴) β†’ (π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄)))
6539ad2antrl 727 . . . . . . . . . . 11 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ π‘Š ∈ SLMod)
66 eqid 2733 . . . . . . . . . . . 12 (Baseβ€˜πΊ) = (Baseβ€˜πΊ)
6742slmdsrg 32340 . . . . . . . . . . . . 13 (π‘Š ∈ SLMod β†’ 𝐺 ∈ SRing)
68 srgcmn 20006 . . . . . . . . . . . . 13 (𝐺 ∈ SRing β†’ 𝐺 ∈ CMnd)
6965, 67, 683syl 18 . . . . . . . . . . . 12 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ 𝐺 ∈ CMnd)
70 vex 3479 . . . . . . . . . . . . 13 𝑒 ∈ V
7170a1i 11 . . . . . . . . . . . 12 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ 𝑒 ∈ V)
72 simplrl 776 . . . . . . . . . . . . . 14 ((((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) ∧ π‘˜ ∈ 𝑒) β†’ πœ‘)
73 simprr 772 . . . . . . . . . . . . . . . 16 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)
7473unssad 4187 . . . . . . . . . . . . . . 15 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ 𝑒 βŠ† 𝐴)
7574sselda 3982 . . . . . . . . . . . . . 14 ((((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) ∧ π‘˜ ∈ 𝑒) β†’ π‘˜ ∈ 𝐴)
76 gsumvsca.k . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐾 βŠ† (Baseβ€˜πΊ))
7776adantr 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ 𝐾 βŠ† (Baseβ€˜πΊ))
78 gsumvsca2.c . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ 𝑃 ∈ 𝐾)
7977, 78sseldd 3983 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ 𝑃 ∈ (Baseβ€˜πΊ))
8072, 75, 79syl2anc 585 . . . . . . . . . . . . 13 ((((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) ∧ π‘˜ ∈ 𝑒) β†’ 𝑃 ∈ (Baseβ€˜πΊ))
8180fmpttd 7112 . . . . . . . . . . . 12 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ (π‘˜ ∈ 𝑒 ↦ 𝑃):π‘’βŸΆ(Baseβ€˜πΊ))
82 eqid 2733 . . . . . . . . . . . . 13 (π‘˜ ∈ 𝑒 ↦ 𝑃) = (π‘˜ ∈ 𝑒 ↦ 𝑃)
83 simpll 766 . . . . . . . . . . . . 13 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ 𝑒 ∈ Fin)
8472, 75, 78syl2anc 585 . . . . . . . . . . . . 13 ((((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) ∧ π‘˜ ∈ 𝑒) β†’ 𝑃 ∈ 𝐾)
85 fvexd 6904 . . . . . . . . . . . . 13 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ (0gβ€˜πΊ) ∈ V)
8682, 83, 84, 85fsuppmptdm 9371 . . . . . . . . . . . 12 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ (π‘˜ ∈ 𝑒 ↦ 𝑃) finSupp (0gβ€˜πΊ))
8766, 44, 69, 71, 81, 86gsumcl 19778 . . . . . . . . . . 11 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ (𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) ∈ (Baseβ€˜πΊ))
8873unssbd 4188 . . . . . . . . . . . . 13 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ {𝑧} βŠ† 𝐴)
89 vex 3479 . . . . . . . . . . . . . 14 𝑧 ∈ V
9089snss 4789 . . . . . . . . . . . . 13 (𝑧 ∈ 𝐴 ↔ {𝑧} βŠ† 𝐴)
9188, 90sylibr 233 . . . . . . . . . . . 12 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ 𝑧 ∈ 𝐴)
9279ralrimiva 3147 . . . . . . . . . . . . 13 (πœ‘ β†’ βˆ€π‘˜ ∈ 𝐴 𝑃 ∈ (Baseβ€˜πΊ))
9392ad2antrl 727 . . . . . . . . . . . 12 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ βˆ€π‘˜ ∈ 𝐴 𝑃 ∈ (Baseβ€˜πΊ))
94 rspcsbela 4435 . . . . . . . . . . . 12 ((𝑧 ∈ 𝐴 ∧ βˆ€π‘˜ ∈ 𝐴 𝑃 ∈ (Baseβ€˜πΊ)) β†’ ⦋𝑧 / π‘˜β¦Œπ‘ƒ ∈ (Baseβ€˜πΊ))
9591, 93, 94syl2anc 585 . . . . . . . . . . 11 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ ⦋𝑧 / π‘˜β¦Œπ‘ƒ ∈ (Baseβ€˜πΊ))
9640ad2antrl 727 . . . . . . . . . . 11 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ 𝑄 ∈ 𝐡)
97 gsumvsca.p . . . . . . . . . . . 12 + = (+gβ€˜π‘Š)
98 eqid 2733 . . . . . . . . . . . 12 (+gβ€˜πΊ) = (+gβ€˜πΊ)
9941, 97, 42, 43, 66, 98slmdvsdir 32349 . . . . . . . . . . 11 ((π‘Š ∈ SLMod ∧ ((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) ∈ (Baseβ€˜πΊ) ∧ ⦋𝑧 / π‘˜β¦Œπ‘ƒ ∈ (Baseβ€˜πΊ) ∧ 𝑄 ∈ 𝐡)) β†’ (((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃))(+gβ€˜πΊ)⦋𝑧 / π‘˜β¦Œπ‘ƒ) Β· 𝑄) = (((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄) + (⦋𝑧 / π‘˜β¦Œπ‘ƒ Β· 𝑄)))
10065, 87, 95, 96, 99syl13anc 1373 . . . . . . . . . 10 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ (((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃))(+gβ€˜πΊ)⦋𝑧 / π‘˜β¦Œπ‘ƒ) Β· 𝑄) = (((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄) + (⦋𝑧 / π‘˜β¦Œπ‘ƒ Β· 𝑄)))
101100adantr 482 . . . . . . . . 9 ((((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) ∧ (π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄)) β†’ (((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃))(+gβ€˜πΊ)⦋𝑧 / π‘˜β¦Œπ‘ƒ) Β· 𝑄) = (((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄) + (⦋𝑧 / π‘˜β¦Œπ‘ƒ Β· 𝑄)))
102 nfcsb1v 3918 . . . . . . . . . . . 12 β„²π‘˜β¦‹π‘§ / π‘˜β¦Œπ‘ƒ
10389a1i 11 . . . . . . . . . . . 12 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ 𝑧 ∈ V)
104 simplr 768 . . . . . . . . . . . 12 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ Β¬ 𝑧 ∈ 𝑒)
105 csbeq1a 3907 . . . . . . . . . . . 12 (π‘˜ = 𝑧 β†’ 𝑃 = ⦋𝑧 / π‘˜β¦Œπ‘ƒ)
106102, 66, 98, 69, 83, 80, 103, 104, 95, 105gsumunsnf 19822 . . . . . . . . . . 11 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ (𝐺 Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ 𝑃)) = ((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃))(+gβ€˜πΊ)⦋𝑧 / π‘˜β¦Œπ‘ƒ))
107106oveq1d 7421 . . . . . . . . . 10 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ ((𝐺 Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ 𝑃)) Β· 𝑄) = (((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃))(+gβ€˜πΊ)⦋𝑧 / π‘˜β¦Œπ‘ƒ) Β· 𝑄))
108107adantr 482 . . . . . . . . 9 ((((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) ∧ (π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄)) β†’ ((𝐺 Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ 𝑃)) Β· 𝑄) = (((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃))(+gβ€˜πΊ)⦋𝑧 / π‘˜β¦Œπ‘ƒ) Β· 𝑄))
109 nfcv 2904 . . . . . . . . . . . . 13 β„²π‘˜ Β·
110 nfcv 2904 . . . . . . . . . . . . 13 β„²π‘˜π‘„
111102, 109, 110nfov 7436 . . . . . . . . . . . 12 β„²π‘˜(⦋𝑧 / π‘˜β¦Œπ‘ƒ Β· 𝑄)
112 slmdcmn 32338 . . . . . . . . . . . . 13 (π‘Š ∈ SLMod β†’ π‘Š ∈ CMnd)
11365, 112syl 17 . . . . . . . . . . . 12 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ π‘Š ∈ CMnd)
11472, 39syl 17 . . . . . . . . . . . . 13 ((((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) ∧ π‘˜ ∈ 𝑒) β†’ π‘Š ∈ SLMod)
11572, 40syl 17 . . . . . . . . . . . . 13 ((((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) ∧ π‘˜ ∈ 𝑒) β†’ 𝑄 ∈ 𝐡)
11641, 42, 43, 66slmdvscl 32347 . . . . . . . . . . . . 13 ((π‘Š ∈ SLMod ∧ 𝑃 ∈ (Baseβ€˜πΊ) ∧ 𝑄 ∈ 𝐡) β†’ (𝑃 Β· 𝑄) ∈ 𝐡)
117114, 80, 115, 116syl3anc 1372 . . . . . . . . . . . 12 ((((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) ∧ π‘˜ ∈ 𝑒) β†’ (𝑃 Β· 𝑄) ∈ 𝐡)
11841, 42, 43, 66slmdvscl 32347 . . . . . . . . . . . . 13 ((π‘Š ∈ SLMod ∧ ⦋𝑧 / π‘˜β¦Œπ‘ƒ ∈ (Baseβ€˜πΊ) ∧ 𝑄 ∈ 𝐡) β†’ (⦋𝑧 / π‘˜β¦Œπ‘ƒ Β· 𝑄) ∈ 𝐡)
11965, 95, 96, 118syl3anc 1372 . . . . . . . . . . . 12 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ (⦋𝑧 / π‘˜β¦Œπ‘ƒ Β· 𝑄) ∈ 𝐡)
120105oveq1d 7421 . . . . . . . . . . . 12 (π‘˜ = 𝑧 β†’ (𝑃 Β· 𝑄) = (⦋𝑧 / π‘˜β¦Œπ‘ƒ Β· 𝑄))
121111, 41, 97, 113, 83, 117, 103, 104, 119, 120gsumunsnf 19822 . . . . . . . . . . 11 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ (π‘Š Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ (𝑃 Β· 𝑄))) = ((π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))) + (⦋𝑧 / π‘˜β¦Œπ‘ƒ Β· 𝑄)))
122121adantr 482 . . . . . . . . . 10 ((((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) ∧ (π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄)) β†’ (π‘Š Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ (𝑃 Β· 𝑄))) = ((π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))) + (⦋𝑧 / π‘˜β¦Œπ‘ƒ Β· 𝑄)))
123 simpr 486 . . . . . . . . . . 11 ((((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) ∧ (π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄)) β†’ (π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄))
124123oveq1d 7421 . . . . . . . . . 10 ((((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) ∧ (π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄)) β†’ ((π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))) + (⦋𝑧 / π‘˜β¦Œπ‘ƒ Β· 𝑄)) = (((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄) + (⦋𝑧 / π‘˜β¦Œπ‘ƒ Β· 𝑄)))
125122, 124eqtrd 2773 . . . . . . . . 9 ((((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) ∧ (π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄)) β†’ (π‘Š Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ (𝑃 Β· 𝑄))) = (((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄) + (⦋𝑧 / π‘˜β¦Œπ‘ƒ Β· 𝑄)))
126101, 108, 1253eqtr4rd 2784 . . . . . . . 8 ((((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) ∧ (π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄)) β†’ (π‘Š Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ 𝑃)) Β· 𝑄))
127126exp31 421 . . . . . . 7 ((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) β†’ ((πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴) β†’ ((π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄) β†’ (π‘Š Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ 𝑃)) Β· 𝑄))))
128127a2d 29 . . . . . 6 ((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) β†’ (((πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴) β†’ (π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄)) β†’ ((πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴) β†’ (π‘Š Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ 𝑃)) Β· 𝑄))))
12964, 128syl5 34 . . . . 5 ((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) β†’ (((πœ‘ ∧ 𝑒 βŠ† 𝐴) β†’ (π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄)) β†’ ((πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴) β†’ (π‘Š Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ 𝑃)) Β· 𝑄))))
13011, 20, 29, 38, 59, 129findcard2s 9162 . . . 4 (𝐴 ∈ Fin β†’ ((πœ‘ ∧ 𝐴 βŠ† 𝐴) β†’ (π‘Š Ξ£g (π‘˜ ∈ 𝐴 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝐴 ↦ 𝑃)) Β· 𝑄)))
131130imp 408 . . 3 ((𝐴 ∈ Fin ∧ (πœ‘ ∧ 𝐴 βŠ† 𝐴)) β†’ (π‘Š Ξ£g (π‘˜ ∈ 𝐴 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝐴 ↦ 𝑃)) Β· 𝑄))
1322, 131mpanr2 703 . 2 ((𝐴 ∈ Fin ∧ πœ‘) β†’ (π‘Š Ξ£g (π‘˜ ∈ 𝐴 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝐴 ↦ 𝑃)) Β· 𝑄))
1331, 132mpancom 687 1 (πœ‘ β†’ (π‘Š Ξ£g (π‘˜ ∈ 𝐴 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝐴 ↦ 𝑃)) Β· 𝑄))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  βˆ€wral 3062  Vcvv 3475  β¦‹csb 3893   βˆͺ cun 3946   βŠ† wss 3948  βˆ…c0 4322  {csn 4628   ↦ cmpt 5231  β€˜cfv 6541  (class class class)co 7406  Fincfn 8936  Basecbs 17141  +gcplusg 17194  Scalarcsca 17197   ·𝑠 cvsca 17198  0gc0g 17382   Ξ£g cgsu 17383  CMndccmn 19643  SRingcsrg 20003  SLModcslmd 32333
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 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184
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 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-isom 6550  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-of 7667  df-om 7853  df-1st 7972  df-2nd 7973  df-supp 8144  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-1o 8463  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-fsupp 9359  df-oi 9502  df-card 9931  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-nn 12210  df-2 12272  df-n0 12470  df-z 12556  df-uz 12820  df-fz 13482  df-fzo 13625  df-seq 13964  df-hash 14288  df-sets 17094  df-slot 17112  df-ndx 17124  df-base 17142  df-ress 17171  df-plusg 17207  df-0g 17384  df-gsum 17385  df-mre 17527  df-mrc 17528  df-acs 17530  df-mgm 18558  df-sgrp 18607  df-mnd 18623  df-submnd 18669  df-mulg 18946  df-cntz 19176  df-cmn 19645  df-srg 20004  df-slmd 32334
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator