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 32806
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 3996 . . 3 𝐴 βŠ† 𝐴
3 sseq1 3999 . . . . . . 7 (π‘Ž = βˆ… β†’ (π‘Ž βŠ† 𝐴 ↔ βˆ… βŠ† 𝐴))
43anbi2d 628 . . . . . 6 (π‘Ž = βˆ… β†’ ((πœ‘ ∧ π‘Ž βŠ† 𝐴) ↔ (πœ‘ ∧ βˆ… βŠ† 𝐴)))
5 mpteq1 5231 . . . . . . . 8 (π‘Ž = βˆ… β†’ (π‘˜ ∈ π‘Ž ↦ (𝑃 Β· 𝑄)) = (π‘˜ ∈ βˆ… ↦ (𝑃 Β· 𝑄)))
65oveq2d 7417 . . . . . . 7 (π‘Ž = βˆ… β†’ (π‘Š Ξ£g (π‘˜ ∈ π‘Ž ↦ (𝑃 Β· 𝑄))) = (π‘Š Ξ£g (π‘˜ ∈ βˆ… ↦ (𝑃 Β· 𝑄))))
7 mpteq1 5231 . . . . . . . . 9 (π‘Ž = βˆ… β†’ (π‘˜ ∈ π‘Ž ↦ 𝑃) = (π‘˜ ∈ βˆ… ↦ 𝑃))
87oveq2d 7417 . . . . . . . 8 (π‘Ž = βˆ… β†’ (𝐺 Ξ£g (π‘˜ ∈ π‘Ž ↦ 𝑃)) = (𝐺 Ξ£g (π‘˜ ∈ βˆ… ↦ 𝑃)))
98oveq1d 7416 . . . . . . 7 (π‘Ž = βˆ… β†’ ((𝐺 Ξ£g (π‘˜ ∈ π‘Ž ↦ 𝑃)) Β· 𝑄) = ((𝐺 Ξ£g (π‘˜ ∈ βˆ… ↦ 𝑃)) Β· 𝑄))
106, 9eqeq12d 2740 . . . . . 6 (π‘Ž = βˆ… β†’ ((π‘Š Ξ£g (π‘˜ ∈ π‘Ž ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ π‘Ž ↦ 𝑃)) Β· 𝑄) ↔ (π‘Š Ξ£g (π‘˜ ∈ βˆ… ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ βˆ… ↦ 𝑃)) Β· 𝑄)))
114, 10imbi12d 344 . . . . 5 (π‘Ž = βˆ… β†’ (((πœ‘ ∧ π‘Ž βŠ† 𝐴) β†’ (π‘Š Ξ£g (π‘˜ ∈ π‘Ž ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ π‘Ž ↦ 𝑃)) Β· 𝑄)) ↔ ((πœ‘ ∧ βˆ… βŠ† 𝐴) β†’ (π‘Š Ξ£g (π‘˜ ∈ βˆ… ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ βˆ… ↦ 𝑃)) Β· 𝑄))))
12 sseq1 3999 . . . . . . 7 (π‘Ž = 𝑒 β†’ (π‘Ž βŠ† 𝐴 ↔ 𝑒 βŠ† 𝐴))
1312anbi2d 628 . . . . . 6 (π‘Ž = 𝑒 β†’ ((πœ‘ ∧ π‘Ž βŠ† 𝐴) ↔ (πœ‘ ∧ 𝑒 βŠ† 𝐴)))
14 mpteq1 5231 . . . . . . . 8 (π‘Ž = 𝑒 β†’ (π‘˜ ∈ π‘Ž ↦ (𝑃 Β· 𝑄)) = (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄)))
1514oveq2d 7417 . . . . . . 7 (π‘Ž = 𝑒 β†’ (π‘Š Ξ£g (π‘˜ ∈ π‘Ž ↦ (𝑃 Β· 𝑄))) = (π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))))
16 mpteq1 5231 . . . . . . . . 9 (π‘Ž = 𝑒 β†’ (π‘˜ ∈ π‘Ž ↦ 𝑃) = (π‘˜ ∈ 𝑒 ↦ 𝑃))
1716oveq2d 7417 . . . . . . . 8 (π‘Ž = 𝑒 β†’ (𝐺 Ξ£g (π‘˜ ∈ π‘Ž ↦ 𝑃)) = (𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)))
1817oveq1d 7416 . . . . . . 7 (π‘Ž = 𝑒 β†’ ((𝐺 Ξ£g (π‘˜ ∈ π‘Ž ↦ 𝑃)) Β· 𝑄) = ((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄))
1915, 18eqeq12d 2740 . . . . . 6 (π‘Ž = 𝑒 β†’ ((π‘Š Ξ£g (π‘˜ ∈ π‘Ž ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ π‘Ž ↦ 𝑃)) Β· 𝑄) ↔ (π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄)))
2013, 19imbi12d 344 . . . . 5 (π‘Ž = 𝑒 β†’ (((πœ‘ ∧ π‘Ž βŠ† 𝐴) β†’ (π‘Š Ξ£g (π‘˜ ∈ π‘Ž ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ π‘Ž ↦ 𝑃)) Β· 𝑄)) ↔ ((πœ‘ ∧ 𝑒 βŠ† 𝐴) β†’ (π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄))))
21 sseq1 3999 . . . . . . 7 (π‘Ž = (𝑒 βˆͺ {𝑧}) β†’ (π‘Ž βŠ† 𝐴 ↔ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴))
2221anbi2d 628 . . . . . 6 (π‘Ž = (𝑒 βˆͺ {𝑧}) β†’ ((πœ‘ ∧ π‘Ž βŠ† 𝐴) ↔ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)))
23 mpteq1 5231 . . . . . . . 8 (π‘Ž = (𝑒 βˆͺ {𝑧}) β†’ (π‘˜ ∈ π‘Ž ↦ (𝑃 Β· 𝑄)) = (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ (𝑃 Β· 𝑄)))
2423oveq2d 7417 . . . . . . 7 (π‘Ž = (𝑒 βˆͺ {𝑧}) β†’ (π‘Š Ξ£g (π‘˜ ∈ π‘Ž ↦ (𝑃 Β· 𝑄))) = (π‘Š Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ (𝑃 Β· 𝑄))))
25 mpteq1 5231 . . . . . . . . 9 (π‘Ž = (𝑒 βˆͺ {𝑧}) β†’ (π‘˜ ∈ π‘Ž ↦ 𝑃) = (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ 𝑃))
2625oveq2d 7417 . . . . . . . 8 (π‘Ž = (𝑒 βˆͺ {𝑧}) β†’ (𝐺 Ξ£g (π‘˜ ∈ π‘Ž ↦ 𝑃)) = (𝐺 Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ 𝑃)))
2726oveq1d 7416 . . . . . . 7 (π‘Ž = (𝑒 βˆͺ {𝑧}) β†’ ((𝐺 Ξ£g (π‘˜ ∈ π‘Ž ↦ 𝑃)) Β· 𝑄) = ((𝐺 Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ 𝑃)) Β· 𝑄))
2824, 27eqeq12d 2740 . . . . . 6 (π‘Ž = (𝑒 βˆͺ {𝑧}) β†’ ((π‘Š Ξ£g (π‘˜ ∈ π‘Ž ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ π‘Ž ↦ 𝑃)) Β· 𝑄) ↔ (π‘Š Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ 𝑃)) Β· 𝑄)))
2922, 28imbi12d 344 . . . . 5 (π‘Ž = (𝑒 βˆͺ {𝑧}) β†’ (((πœ‘ ∧ π‘Ž βŠ† 𝐴) β†’ (π‘Š Ξ£g (π‘˜ ∈ π‘Ž ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ π‘Ž ↦ 𝑃)) Β· 𝑄)) ↔ ((πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴) β†’ (π‘Š Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ 𝑃)) Β· 𝑄))))
30 sseq1 3999 . . . . . . 7 (π‘Ž = 𝐴 β†’ (π‘Ž βŠ† 𝐴 ↔ 𝐴 βŠ† 𝐴))
3130anbi2d 628 . . . . . 6 (π‘Ž = 𝐴 β†’ ((πœ‘ ∧ π‘Ž βŠ† 𝐴) ↔ (πœ‘ ∧ 𝐴 βŠ† 𝐴)))
32 mpteq1 5231 . . . . . . . 8 (π‘Ž = 𝐴 β†’ (π‘˜ ∈ π‘Ž ↦ (𝑃 Β· 𝑄)) = (π‘˜ ∈ 𝐴 ↦ (𝑃 Β· 𝑄)))
3332oveq2d 7417 . . . . . . 7 (π‘Ž = 𝐴 β†’ (π‘Š Ξ£g (π‘˜ ∈ π‘Ž ↦ (𝑃 Β· 𝑄))) = (π‘Š Ξ£g (π‘˜ ∈ 𝐴 ↦ (𝑃 Β· 𝑄))))
34 mpteq1 5231 . . . . . . . . 9 (π‘Ž = 𝐴 β†’ (π‘˜ ∈ π‘Ž ↦ 𝑃) = (π‘˜ ∈ 𝐴 ↦ 𝑃))
3534oveq2d 7417 . . . . . . . 8 (π‘Ž = 𝐴 β†’ (𝐺 Ξ£g (π‘˜ ∈ π‘Ž ↦ 𝑃)) = (𝐺 Ξ£g (π‘˜ ∈ 𝐴 ↦ 𝑃)))
3635oveq1d 7416 . . . . . . 7 (π‘Ž = 𝐴 β†’ ((𝐺 Ξ£g (π‘˜ ∈ π‘Ž ↦ 𝑃)) Β· 𝑄) = ((𝐺 Ξ£g (π‘˜ ∈ 𝐴 ↦ 𝑃)) Β· 𝑄))
3733, 36eqeq12d 2740 . . . . . 6 (π‘Ž = 𝐴 β†’ ((π‘Š Ξ£g (π‘˜ ∈ π‘Ž ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ π‘Ž ↦ 𝑃)) Β· 𝑄) ↔ (π‘Š Ξ£g (π‘˜ ∈ 𝐴 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝐴 ↦ 𝑃)) Β· 𝑄)))
3831, 37imbi12d 344 . . . . 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 2724 . . . . . . . . . 10 (0gβ€˜πΊ) = (0gβ€˜πΊ)
45 gsumvsca.z . . . . . . . . . 10 0 = (0gβ€˜π‘Š)
4641, 42, 43, 44, 45slmd0vs 32803 . . . . . . . . 9 ((π‘Š ∈ SLMod ∧ 𝑄 ∈ 𝐡) β†’ ((0gβ€˜πΊ) Β· 𝑄) = 0 )
4739, 40, 46syl2anc 583 . . . . . . . 8 (πœ‘ β†’ ((0gβ€˜πΊ) Β· 𝑄) = 0 )
4847eqcomd 2730 . . . . . . 7 (πœ‘ β†’ 0 = ((0gβ€˜πΊ) Β· 𝑄))
49 mpt0 6682 . . . . . . . . 9 (π‘˜ ∈ βˆ… ↦ (𝑃 Β· 𝑄)) = βˆ…
5049oveq2i 7412 . . . . . . . 8 (π‘Š Ξ£g (π‘˜ ∈ βˆ… ↦ (𝑃 Β· 𝑄))) = (π‘Š Ξ£g βˆ…)
5145gsum0 18606 . . . . . . . 8 (π‘Š Ξ£g βˆ…) = 0
5250, 51eqtri 2752 . . . . . . 7 (π‘Š Ξ£g (π‘˜ ∈ βˆ… ↦ (𝑃 Β· 𝑄))) = 0
53 mpt0 6682 . . . . . . . . . 10 (π‘˜ ∈ βˆ… ↦ 𝑃) = βˆ…
5453oveq2i 7412 . . . . . . . . 9 (𝐺 Ξ£g (π‘˜ ∈ βˆ… ↦ 𝑃)) = (𝐺 Ξ£g βˆ…)
5544gsum0 18606 . . . . . . . . 9 (𝐺 Ξ£g βˆ…) = (0gβ€˜πΊ)
5654, 55eqtri 2752 . . . . . . . 8 (𝐺 Ξ£g (π‘˜ ∈ βˆ… ↦ 𝑃)) = (0gβ€˜πΊ)
5756oveq1i 7411 . . . . . . 7 ((𝐺 Ξ£g (π‘˜ ∈ βˆ… ↦ 𝑃)) Β· 𝑄) = ((0gβ€˜πΊ) Β· 𝑄)
5848, 52, 573eqtr4g 2789 . . . . . 6 (πœ‘ β†’ (π‘Š Ξ£g (π‘˜ ∈ βˆ… ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ βˆ… ↦ 𝑃)) Β· 𝑄))
5958adantr 480 . . . . 5 ((πœ‘ ∧ βˆ… βŠ† 𝐴) β†’ (π‘Š Ξ£g (π‘˜ ∈ βˆ… ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ βˆ… ↦ 𝑃)) Β· 𝑄))
60 ssun1 4164 . . . . . . . . 9 𝑒 βŠ† (𝑒 βˆͺ {𝑧})
61 sstr2 3981 . . . . . . . . 9 (𝑒 βŠ† (𝑒 βˆͺ {𝑧}) β†’ ((𝑒 βˆͺ {𝑧}) βŠ† 𝐴 β†’ 𝑒 βŠ† 𝐴))
6260, 61ax-mp 5 . . . . . . . 8 ((𝑒 βˆͺ {𝑧}) βŠ† 𝐴 β†’ 𝑒 βŠ† 𝐴)
6362anim2i 616 . . . . . . 7 ((πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴) β†’ (πœ‘ ∧ 𝑒 βŠ† 𝐴))
6463imim1i 63 . . . . . 6 (((πœ‘ ∧ 𝑒 βŠ† 𝐴) β†’ (π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄)) β†’ ((πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴) β†’ (π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄)))
6539ad2antrl 725 . . . . . . . . . . 11 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ π‘Š ∈ SLMod)
66 eqid 2724 . . . . . . . . . . . 12 (Baseβ€˜πΊ) = (Baseβ€˜πΊ)
6742slmdsrg 32786 . . . . . . . . . . . . 13 (π‘Š ∈ SLMod β†’ 𝐺 ∈ SRing)
68 srgcmn 20083 . . . . . . . . . . . . 13 (𝐺 ∈ SRing β†’ 𝐺 ∈ CMnd)
6965, 67, 683syl 18 . . . . . . . . . . . 12 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ 𝐺 ∈ CMnd)
70 vex 3470 . . . . . . . . . . . . 13 𝑒 ∈ V
7170a1i 11 . . . . . . . . . . . 12 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ 𝑒 ∈ V)
72 simplrl 774 . . . . . . . . . . . . . 14 ((((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) ∧ π‘˜ ∈ 𝑒) β†’ πœ‘)
73 simprr 770 . . . . . . . . . . . . . . . 16 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)
7473unssad 4179 . . . . . . . . . . . . . . 15 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ 𝑒 βŠ† 𝐴)
7574sselda 3974 . . . . . . . . . . . . . 14 ((((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) ∧ π‘˜ ∈ 𝑒) β†’ π‘˜ ∈ 𝐴)
76 gsumvsca.k . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐾 βŠ† (Baseβ€˜πΊ))
7776adantr 480 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ 𝐾 βŠ† (Baseβ€˜πΊ))
78 gsumvsca2.c . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ 𝑃 ∈ 𝐾)
7977, 78sseldd 3975 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ 𝑃 ∈ (Baseβ€˜πΊ))
8072, 75, 79syl2anc 583 . . . . . . . . . . . . 13 ((((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) ∧ π‘˜ ∈ 𝑒) β†’ 𝑃 ∈ (Baseβ€˜πΊ))
8180fmpttd 7106 . . . . . . . . . . . 12 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ (π‘˜ ∈ 𝑒 ↦ 𝑃):π‘’βŸΆ(Baseβ€˜πΊ))
82 eqid 2724 . . . . . . . . . . . . 13 (π‘˜ ∈ 𝑒 ↦ 𝑃) = (π‘˜ ∈ 𝑒 ↦ 𝑃)
83 simpll 764 . . . . . . . . . . . . 13 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ 𝑒 ∈ Fin)
8472, 75, 78syl2anc 583 . . . . . . . . . . . . 13 ((((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) ∧ π‘˜ ∈ 𝑒) β†’ 𝑃 ∈ 𝐾)
85 fvexd 6896 . . . . . . . . . . . . 13 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ (0gβ€˜πΊ) ∈ V)
8682, 83, 84, 85fsuppmptdm 9369 . . . . . . . . . . . 12 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ (π‘˜ ∈ 𝑒 ↦ 𝑃) finSupp (0gβ€˜πΊ))
8766, 44, 69, 71, 81, 86gsumcl 19824 . . . . . . . . . . 11 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ (𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) ∈ (Baseβ€˜πΊ))
8873unssbd 4180 . . . . . . . . . . . . 13 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ {𝑧} βŠ† 𝐴)
89 vex 3470 . . . . . . . . . . . . . 14 𝑧 ∈ V
9089snss 4781 . . . . . . . . . . . . 13 (𝑧 ∈ 𝐴 ↔ {𝑧} βŠ† 𝐴)
9188, 90sylibr 233 . . . . . . . . . . . 12 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ 𝑧 ∈ 𝐴)
9279ralrimiva 3138 . . . . . . . . . . . . 13 (πœ‘ β†’ βˆ€π‘˜ ∈ 𝐴 𝑃 ∈ (Baseβ€˜πΊ))
9392ad2antrl 725 . . . . . . . . . . . 12 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ βˆ€π‘˜ ∈ 𝐴 𝑃 ∈ (Baseβ€˜πΊ))
94 rspcsbela 4427 . . . . . . . . . . . 12 ((𝑧 ∈ 𝐴 ∧ βˆ€π‘˜ ∈ 𝐴 𝑃 ∈ (Baseβ€˜πΊ)) β†’ ⦋𝑧 / π‘˜β¦Œπ‘ƒ ∈ (Baseβ€˜πΊ))
9591, 93, 94syl2anc 583 . . . . . . . . . . 11 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ ⦋𝑧 / π‘˜β¦Œπ‘ƒ ∈ (Baseβ€˜πΊ))
9640ad2antrl 725 . . . . . . . . . . 11 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ 𝑄 ∈ 𝐡)
97 gsumvsca.p . . . . . . . . . . . 12 + = (+gβ€˜π‘Š)
98 eqid 2724 . . . . . . . . . . . 12 (+gβ€˜πΊ) = (+gβ€˜πΊ)
9941, 97, 42, 43, 66, 98slmdvsdir 32795 . . . . . . . . . . 11 ((π‘Š ∈ SLMod ∧ ((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) ∈ (Baseβ€˜πΊ) ∧ ⦋𝑧 / π‘˜β¦Œπ‘ƒ ∈ (Baseβ€˜πΊ) ∧ 𝑄 ∈ 𝐡)) β†’ (((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃))(+gβ€˜πΊ)⦋𝑧 / π‘˜β¦Œπ‘ƒ) Β· 𝑄) = (((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄) + (⦋𝑧 / π‘˜β¦Œπ‘ƒ Β· 𝑄)))
10065, 87, 95, 96, 99syl13anc 1369 . . . . . . . . . 10 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ (((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃))(+gβ€˜πΊ)⦋𝑧 / π‘˜β¦Œπ‘ƒ) Β· 𝑄) = (((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄) + (⦋𝑧 / π‘˜β¦Œπ‘ƒ Β· 𝑄)))
101100adantr 480 . . . . . . . . 9 ((((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) ∧ (π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄)) β†’ (((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃))(+gβ€˜πΊ)⦋𝑧 / π‘˜β¦Œπ‘ƒ) Β· 𝑄) = (((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄) + (⦋𝑧 / π‘˜β¦Œπ‘ƒ Β· 𝑄)))
102 nfcsb1v 3910 . . . . . . . . . . . 12 β„²π‘˜β¦‹π‘§ / π‘˜β¦Œπ‘ƒ
10389a1i 11 . . . . . . . . . . . 12 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ 𝑧 ∈ V)
104 simplr 766 . . . . . . . . . . . 12 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ Β¬ 𝑧 ∈ 𝑒)
105 csbeq1a 3899 . . . . . . . . . . . 12 (π‘˜ = 𝑧 β†’ 𝑃 = ⦋𝑧 / π‘˜β¦Œπ‘ƒ)
106102, 66, 98, 69, 83, 80, 103, 104, 95, 105gsumunsnf 19868 . . . . . . . . . . 11 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ (𝐺 Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ 𝑃)) = ((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃))(+gβ€˜πΊ)⦋𝑧 / π‘˜β¦Œπ‘ƒ))
107106oveq1d 7416 . . . . . . . . . 10 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ ((𝐺 Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ 𝑃)) Β· 𝑄) = (((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃))(+gβ€˜πΊ)⦋𝑧 / π‘˜β¦Œπ‘ƒ) Β· 𝑄))
108107adantr 480 . . . . . . . . 9 ((((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) ∧ (π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄)) β†’ ((𝐺 Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ 𝑃)) Β· 𝑄) = (((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃))(+gβ€˜πΊ)⦋𝑧 / π‘˜β¦Œπ‘ƒ) Β· 𝑄))
109 nfcv 2895 . . . . . . . . . . . . 13 β„²π‘˜ Β·
110 nfcv 2895 . . . . . . . . . . . . 13 β„²π‘˜π‘„
111102, 109, 110nfov 7431 . . . . . . . . . . . 12 β„²π‘˜(⦋𝑧 / π‘˜β¦Œπ‘ƒ Β· 𝑄)
112 slmdcmn 32784 . . . . . . . . . . . . 13 (π‘Š ∈ SLMod β†’ π‘Š ∈ CMnd)
11365, 112syl 17 . . . . . . . . . . . 12 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ π‘Š ∈ CMnd)
11472, 39syl 17 . . . . . . . . . . . . 13 ((((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) ∧ π‘˜ ∈ 𝑒) β†’ π‘Š ∈ SLMod)
11572, 40syl 17 . . . . . . . . . . . . 13 ((((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) ∧ π‘˜ ∈ 𝑒) β†’ 𝑄 ∈ 𝐡)
11641, 42, 43, 66slmdvscl 32793 . . . . . . . . . . . . 13 ((π‘Š ∈ SLMod ∧ 𝑃 ∈ (Baseβ€˜πΊ) ∧ 𝑄 ∈ 𝐡) β†’ (𝑃 Β· 𝑄) ∈ 𝐡)
117114, 80, 115, 116syl3anc 1368 . . . . . . . . . . . 12 ((((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) ∧ π‘˜ ∈ 𝑒) β†’ (𝑃 Β· 𝑄) ∈ 𝐡)
11841, 42, 43, 66slmdvscl 32793 . . . . . . . . . . . . 13 ((π‘Š ∈ SLMod ∧ ⦋𝑧 / π‘˜β¦Œπ‘ƒ ∈ (Baseβ€˜πΊ) ∧ 𝑄 ∈ 𝐡) β†’ (⦋𝑧 / π‘˜β¦Œπ‘ƒ Β· 𝑄) ∈ 𝐡)
11965, 95, 96, 118syl3anc 1368 . . . . . . . . . . . 12 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ (⦋𝑧 / π‘˜β¦Œπ‘ƒ Β· 𝑄) ∈ 𝐡)
120105oveq1d 7416 . . . . . . . . . . . 12 (π‘˜ = 𝑧 β†’ (𝑃 Β· 𝑄) = (⦋𝑧 / π‘˜β¦Œπ‘ƒ Β· 𝑄))
121111, 41, 97, 113, 83, 117, 103, 104, 119, 120gsumunsnf 19868 . . . . . . . . . . 11 (((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) β†’ (π‘Š Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ (𝑃 Β· 𝑄))) = ((π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))) + (⦋𝑧 / π‘˜β¦Œπ‘ƒ Β· 𝑄)))
122121adantr 480 . . . . . . . . . 10 ((((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) ∧ (π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄)) β†’ (π‘Š Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ (𝑃 Β· 𝑄))) = ((π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))) + (⦋𝑧 / π‘˜β¦Œπ‘ƒ Β· 𝑄)))
123 simpr 484 . . . . . . . . . . 11 ((((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) ∧ (π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄)) β†’ (π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄))
124123oveq1d 7416 . . . . . . . . . 10 ((((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) ∧ (π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄)) β†’ ((π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))) + (⦋𝑧 / π‘˜β¦Œπ‘ƒ Β· 𝑄)) = (((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄) + (⦋𝑧 / π‘˜β¦Œπ‘ƒ Β· 𝑄)))
125122, 124eqtrd 2764 . . . . . . . . 9 ((((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) ∧ (π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄)) β†’ (π‘Š Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ (𝑃 Β· 𝑄))) = (((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄) + (⦋𝑧 / π‘˜β¦Œπ‘ƒ Β· 𝑄)))
126101, 108, 1253eqtr4rd 2775 . . . . . . . 8 ((((𝑒 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑒) ∧ (πœ‘ ∧ (𝑒 βˆͺ {𝑧}) βŠ† 𝐴)) ∧ (π‘Š Ξ£g (π‘˜ ∈ 𝑒 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝑒 ↦ 𝑃)) Β· 𝑄)) β†’ (π‘Š Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ (𝑒 βˆͺ {𝑧}) ↦ 𝑃)) Β· 𝑄))
127126exp31 419 . . . . . . 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 9160 . . . 4 (𝐴 ∈ Fin β†’ ((πœ‘ ∧ 𝐴 βŠ† 𝐴) β†’ (π‘Š Ξ£g (π‘˜ ∈ 𝐴 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝐴 ↦ 𝑃)) Β· 𝑄)))
131130imp 406 . . 3 ((𝐴 ∈ Fin ∧ (πœ‘ ∧ 𝐴 βŠ† 𝐴)) β†’ (π‘Š Ξ£g (π‘˜ ∈ 𝐴 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝐴 ↦ 𝑃)) Β· 𝑄))
1322, 131mpanr2 701 . 2 ((𝐴 ∈ Fin ∧ πœ‘) β†’ (π‘Š Ξ£g (π‘˜ ∈ 𝐴 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝐴 ↦ 𝑃)) Β· 𝑄))
1331, 132mpancom 685 1 (πœ‘ β†’ (π‘Š Ξ£g (π‘˜ ∈ 𝐴 ↦ (𝑃 Β· 𝑄))) = ((𝐺 Ξ£g (π‘˜ ∈ 𝐴 ↦ 𝑃)) Β· 𝑄))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 395   = wceq 1533   ∈ wcel 2098  βˆ€wral 3053  Vcvv 3466  β¦‹csb 3885   βˆͺ cun 3938   βŠ† wss 3940  βˆ…c0 4314  {csn 4620   ↦ cmpt 5221  β€˜cfv 6533  (class class class)co 7401  Fincfn 8934  Basecbs 17142  +gcplusg 17195  Scalarcsca 17198   ·𝑠 cvsca 17199  0gc0g 17383   Ξ£g cgsu 17384  CMndccmn 19689  SRingcsrg 20080  SLModcslmd 32779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-cnex 11161  ax-resscn 11162  ax-1cn 11163  ax-icn 11164  ax-addcl 11165  ax-addrcl 11166  ax-mulcl 11167  ax-mulrcl 11168  ax-mulcom 11169  ax-addass 11170  ax-mulass 11171  ax-distr 11172  ax-i2m1 11173  ax-1ne0 11174  ax-1rid 11175  ax-rnegex 11176  ax-rrecex 11177  ax-cnre 11178  ax-pre-lttri 11179  ax-pre-lttrn 11180  ax-pre-ltadd 11181  ax-pre-mulgt0 11182
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-iin 4990  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-of 7663  df-om 7849  df-1st 7968  df-2nd 7969  df-supp 8141  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-er 8698  df-en 8935  df-dom 8936  df-sdom 8937  df-fin 8938  df-fsupp 9357  df-oi 9500  df-card 9929  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-nn 12209  df-2 12271  df-n0 12469  df-z 12555  df-uz 12819  df-fz 13481  df-fzo 13624  df-seq 13963  df-hash 14287  df-sets 17095  df-slot 17113  df-ndx 17125  df-base 17143  df-ress 17172  df-plusg 17208  df-0g 17385  df-gsum 17386  df-mre 17528  df-mrc 17529  df-acs 17531  df-mgm 18562  df-sgrp 18641  df-mnd 18657  df-submnd 18703  df-mulg 18985  df-cntz 19222  df-cmn 19691  df-srg 20081  df-slmd 32780
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator