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

Theorem srgbinom 20125
Description: The binomial theorem for commuting elements of a semiring: (๐ด + ๐ต)โ†‘๐‘ is the sum from ๐‘˜ = 0 to ๐‘ of (๐‘C๐‘˜) ยท ((๐ดโ†‘๐‘˜) ยท (๐ตโ†‘(๐‘ โˆ’ ๐‘˜)) (generalization of binom 15772). (Contributed by AV, 24-Aug-2019.)
Hypotheses
Ref Expression
srgbinom.s ๐‘† = (Baseโ€˜๐‘…)
srgbinom.m ร— = (.rโ€˜๐‘…)
srgbinom.t ยท = (.gโ€˜๐‘…)
srgbinom.a + = (+gโ€˜๐‘…)
srgbinom.g ๐บ = (mulGrpโ€˜๐‘…)
srgbinom.e โ†‘ = (.gโ€˜๐บ)
Assertion
Ref Expression
srgbinom (((๐‘… โˆˆ SRing โˆง ๐‘ โˆˆ โ„•0) โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ (๐‘ โ†‘ (๐ด + ๐ต)) = (๐‘… ฮฃg (๐‘˜ โˆˆ (0...๐‘) โ†ฆ ((๐‘C๐‘˜) ยท (((๐‘ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))))
Distinct variable groups:   ๐ด,๐‘˜   ๐ต,๐‘˜   ๐‘˜,๐‘   ๐‘…,๐‘˜   ๐‘†,๐‘˜   ยท ,๐‘˜   โ†‘ ,๐‘˜   ร— ,๐‘˜   + ,๐‘˜
Allowed substitution hint:   ๐บ(๐‘˜)

Proof of Theorem srgbinom
Dummy variables ๐‘› ๐‘ฅ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq1 7408 . . . . . . 7 (๐‘ฅ = 0 โ†’ (๐‘ฅ โ†‘ (๐ด + ๐ต)) = (0 โ†‘ (๐ด + ๐ต)))
2 oveq2 7409 . . . . . . . . 9 (๐‘ฅ = 0 โ†’ (0...๐‘ฅ) = (0...0))
3 oveq1 7408 . . . . . . . . . 10 (๐‘ฅ = 0 โ†’ (๐‘ฅC๐‘˜) = (0C๐‘˜))
4 oveq1 7408 . . . . . . . . . . . 12 (๐‘ฅ = 0 โ†’ (๐‘ฅ โˆ’ ๐‘˜) = (0 โˆ’ ๐‘˜))
54oveq1d 7416 . . . . . . . . . . 11 (๐‘ฅ = 0 โ†’ ((๐‘ฅ โˆ’ ๐‘˜) โ†‘ ๐ด) = ((0 โˆ’ ๐‘˜) โ†‘ ๐ด))
65oveq1d 7416 . . . . . . . . . 10 (๐‘ฅ = 0 โ†’ (((๐‘ฅ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต)) = (((0 โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต)))
73, 6oveq12d 7419 . . . . . . . . 9 (๐‘ฅ = 0 โ†’ ((๐‘ฅC๐‘˜) ยท (((๐‘ฅ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))) = ((0C๐‘˜) ยท (((0 โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))
82, 7mpteq12dv 5229 . . . . . . . 8 (๐‘ฅ = 0 โ†’ (๐‘˜ โˆˆ (0...๐‘ฅ) โ†ฆ ((๐‘ฅC๐‘˜) ยท (((๐‘ฅ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต)))) = (๐‘˜ โˆˆ (0...0) โ†ฆ ((0C๐‘˜) ยท (((0 โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต)))))
98oveq2d 7417 . . . . . . 7 (๐‘ฅ = 0 โ†’ (๐‘… ฮฃg (๐‘˜ โˆˆ (0...๐‘ฅ) โ†ฆ ((๐‘ฅC๐‘˜) ยท (((๐‘ฅ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))) = (๐‘… ฮฃg (๐‘˜ โˆˆ (0...0) โ†ฆ ((0C๐‘˜) ยท (((0 โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))))
101, 9eqeq12d 2740 . . . . . 6 (๐‘ฅ = 0 โ†’ ((๐‘ฅ โ†‘ (๐ด + ๐ต)) = (๐‘… ฮฃg (๐‘˜ โˆˆ (0...๐‘ฅ) โ†ฆ ((๐‘ฅC๐‘˜) ยท (((๐‘ฅ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))) โ†” (0 โ†‘ (๐ด + ๐ต)) = (๐‘… ฮฃg (๐‘˜ โˆˆ (0...0) โ†ฆ ((0C๐‘˜) ยท (((0 โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต)))))))
1110imbi2d 340 . . . . 5 (๐‘ฅ = 0 โ†’ (((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ (๐‘ฅ โ†‘ (๐ด + ๐ต)) = (๐‘… ฮฃg (๐‘˜ โˆˆ (0...๐‘ฅ) โ†ฆ ((๐‘ฅC๐‘˜) ยท (((๐‘ฅ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต)))))) โ†” ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ (0 โ†‘ (๐ด + ๐ต)) = (๐‘… ฮฃg (๐‘˜ โˆˆ (0...0) โ†ฆ ((0C๐‘˜) ยท (((0 โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))))))
12 oveq1 7408 . . . . . . 7 (๐‘ฅ = ๐‘› โ†’ (๐‘ฅ โ†‘ (๐ด + ๐ต)) = (๐‘› โ†‘ (๐ด + ๐ต)))
13 oveq2 7409 . . . . . . . . 9 (๐‘ฅ = ๐‘› โ†’ (0...๐‘ฅ) = (0...๐‘›))
14 oveq1 7408 . . . . . . . . . 10 (๐‘ฅ = ๐‘› โ†’ (๐‘ฅC๐‘˜) = (๐‘›C๐‘˜))
15 oveq1 7408 . . . . . . . . . . . 12 (๐‘ฅ = ๐‘› โ†’ (๐‘ฅ โˆ’ ๐‘˜) = (๐‘› โˆ’ ๐‘˜))
1615oveq1d 7416 . . . . . . . . . . 11 (๐‘ฅ = ๐‘› โ†’ ((๐‘ฅ โˆ’ ๐‘˜) โ†‘ ๐ด) = ((๐‘› โˆ’ ๐‘˜) โ†‘ ๐ด))
1716oveq1d 7416 . . . . . . . . . 10 (๐‘ฅ = ๐‘› โ†’ (((๐‘ฅ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต)) = (((๐‘› โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต)))
1814, 17oveq12d 7419 . . . . . . . . 9 (๐‘ฅ = ๐‘› โ†’ ((๐‘ฅC๐‘˜) ยท (((๐‘ฅ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))) = ((๐‘›C๐‘˜) ยท (((๐‘› โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))
1913, 18mpteq12dv 5229 . . . . . . . 8 (๐‘ฅ = ๐‘› โ†’ (๐‘˜ โˆˆ (0...๐‘ฅ) โ†ฆ ((๐‘ฅC๐‘˜) ยท (((๐‘ฅ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต)))) = (๐‘˜ โˆˆ (0...๐‘›) โ†ฆ ((๐‘›C๐‘˜) ยท (((๐‘› โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต)))))
2019oveq2d 7417 . . . . . . 7 (๐‘ฅ = ๐‘› โ†’ (๐‘… ฮฃg (๐‘˜ โˆˆ (0...๐‘ฅ) โ†ฆ ((๐‘ฅC๐‘˜) ยท (((๐‘ฅ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))) = (๐‘… ฮฃg (๐‘˜ โˆˆ (0...๐‘›) โ†ฆ ((๐‘›C๐‘˜) ยท (((๐‘› โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))))
2112, 20eqeq12d 2740 . . . . . 6 (๐‘ฅ = ๐‘› โ†’ ((๐‘ฅ โ†‘ (๐ด + ๐ต)) = (๐‘… ฮฃg (๐‘˜ โˆˆ (0...๐‘ฅ) โ†ฆ ((๐‘ฅC๐‘˜) ยท (((๐‘ฅ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))) โ†” (๐‘› โ†‘ (๐ด + ๐ต)) = (๐‘… ฮฃg (๐‘˜ โˆˆ (0...๐‘›) โ†ฆ ((๐‘›C๐‘˜) ยท (((๐‘› โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต)))))))
2221imbi2d 340 . . . . 5 (๐‘ฅ = ๐‘› โ†’ (((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ (๐‘ฅ โ†‘ (๐ด + ๐ต)) = (๐‘… ฮฃg (๐‘˜ โˆˆ (0...๐‘ฅ) โ†ฆ ((๐‘ฅC๐‘˜) ยท (((๐‘ฅ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต)))))) โ†” ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ (๐‘› โ†‘ (๐ด + ๐ต)) = (๐‘… ฮฃg (๐‘˜ โˆˆ (0...๐‘›) โ†ฆ ((๐‘›C๐‘˜) ยท (((๐‘› โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))))))
23 oveq1 7408 . . . . . . 7 (๐‘ฅ = (๐‘› + 1) โ†’ (๐‘ฅ โ†‘ (๐ด + ๐ต)) = ((๐‘› + 1) โ†‘ (๐ด + ๐ต)))
24 oveq2 7409 . . . . . . . . 9 (๐‘ฅ = (๐‘› + 1) โ†’ (0...๐‘ฅ) = (0...(๐‘› + 1)))
25 oveq1 7408 . . . . . . . . . 10 (๐‘ฅ = (๐‘› + 1) โ†’ (๐‘ฅC๐‘˜) = ((๐‘› + 1)C๐‘˜))
26 oveq1 7408 . . . . . . . . . . . 12 (๐‘ฅ = (๐‘› + 1) โ†’ (๐‘ฅ โˆ’ ๐‘˜) = ((๐‘› + 1) โˆ’ ๐‘˜))
2726oveq1d 7416 . . . . . . . . . . 11 (๐‘ฅ = (๐‘› + 1) โ†’ ((๐‘ฅ โˆ’ ๐‘˜) โ†‘ ๐ด) = (((๐‘› + 1) โˆ’ ๐‘˜) โ†‘ ๐ด))
2827oveq1d 7416 . . . . . . . . . 10 (๐‘ฅ = (๐‘› + 1) โ†’ (((๐‘ฅ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต)) = ((((๐‘› + 1) โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต)))
2925, 28oveq12d 7419 . . . . . . . . 9 (๐‘ฅ = (๐‘› + 1) โ†’ ((๐‘ฅC๐‘˜) ยท (((๐‘ฅ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))) = (((๐‘› + 1)C๐‘˜) ยท ((((๐‘› + 1) โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))
3024, 29mpteq12dv 5229 . . . . . . . 8 (๐‘ฅ = (๐‘› + 1) โ†’ (๐‘˜ โˆˆ (0...๐‘ฅ) โ†ฆ ((๐‘ฅC๐‘˜) ยท (((๐‘ฅ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต)))) = (๐‘˜ โˆˆ (0...(๐‘› + 1)) โ†ฆ (((๐‘› + 1)C๐‘˜) ยท ((((๐‘› + 1) โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต)))))
3130oveq2d 7417 . . . . . . 7 (๐‘ฅ = (๐‘› + 1) โ†’ (๐‘… ฮฃg (๐‘˜ โˆˆ (0...๐‘ฅ) โ†ฆ ((๐‘ฅC๐‘˜) ยท (((๐‘ฅ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))) = (๐‘… ฮฃg (๐‘˜ โˆˆ (0...(๐‘› + 1)) โ†ฆ (((๐‘› + 1)C๐‘˜) ยท ((((๐‘› + 1) โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))))
3223, 31eqeq12d 2740 . . . . . 6 (๐‘ฅ = (๐‘› + 1) โ†’ ((๐‘ฅ โ†‘ (๐ด + ๐ต)) = (๐‘… ฮฃg (๐‘˜ โˆˆ (0...๐‘ฅ) โ†ฆ ((๐‘ฅC๐‘˜) ยท (((๐‘ฅ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))) โ†” ((๐‘› + 1) โ†‘ (๐ด + ๐ต)) = (๐‘… ฮฃg (๐‘˜ โˆˆ (0...(๐‘› + 1)) โ†ฆ (((๐‘› + 1)C๐‘˜) ยท ((((๐‘› + 1) โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต)))))))
3332imbi2d 340 . . . . 5 (๐‘ฅ = (๐‘› + 1) โ†’ (((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ (๐‘ฅ โ†‘ (๐ด + ๐ต)) = (๐‘… ฮฃg (๐‘˜ โˆˆ (0...๐‘ฅ) โ†ฆ ((๐‘ฅC๐‘˜) ยท (((๐‘ฅ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต)))))) โ†” ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ ((๐‘› + 1) โ†‘ (๐ด + ๐ต)) = (๐‘… ฮฃg (๐‘˜ โˆˆ (0...(๐‘› + 1)) โ†ฆ (((๐‘› + 1)C๐‘˜) ยท ((((๐‘› + 1) โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))))))
34 oveq1 7408 . . . . . . 7 (๐‘ฅ = ๐‘ โ†’ (๐‘ฅ โ†‘ (๐ด + ๐ต)) = (๐‘ โ†‘ (๐ด + ๐ต)))
35 oveq2 7409 . . . . . . . . 9 (๐‘ฅ = ๐‘ โ†’ (0...๐‘ฅ) = (0...๐‘))
36 oveq1 7408 . . . . . . . . . 10 (๐‘ฅ = ๐‘ โ†’ (๐‘ฅC๐‘˜) = (๐‘C๐‘˜))
37 oveq1 7408 . . . . . . . . . . . 12 (๐‘ฅ = ๐‘ โ†’ (๐‘ฅ โˆ’ ๐‘˜) = (๐‘ โˆ’ ๐‘˜))
3837oveq1d 7416 . . . . . . . . . . 11 (๐‘ฅ = ๐‘ โ†’ ((๐‘ฅ โˆ’ ๐‘˜) โ†‘ ๐ด) = ((๐‘ โˆ’ ๐‘˜) โ†‘ ๐ด))
3938oveq1d 7416 . . . . . . . . . 10 (๐‘ฅ = ๐‘ โ†’ (((๐‘ฅ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต)) = (((๐‘ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต)))
4036, 39oveq12d 7419 . . . . . . . . 9 (๐‘ฅ = ๐‘ โ†’ ((๐‘ฅC๐‘˜) ยท (((๐‘ฅ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))) = ((๐‘C๐‘˜) ยท (((๐‘ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))
4135, 40mpteq12dv 5229 . . . . . . . 8 (๐‘ฅ = ๐‘ โ†’ (๐‘˜ โˆˆ (0...๐‘ฅ) โ†ฆ ((๐‘ฅC๐‘˜) ยท (((๐‘ฅ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต)))) = (๐‘˜ โˆˆ (0...๐‘) โ†ฆ ((๐‘C๐‘˜) ยท (((๐‘ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต)))))
4241oveq2d 7417 . . . . . . 7 (๐‘ฅ = ๐‘ โ†’ (๐‘… ฮฃg (๐‘˜ โˆˆ (0...๐‘ฅ) โ†ฆ ((๐‘ฅC๐‘˜) ยท (((๐‘ฅ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))) = (๐‘… ฮฃg (๐‘˜ โˆˆ (0...๐‘) โ†ฆ ((๐‘C๐‘˜) ยท (((๐‘ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))))
4334, 42eqeq12d 2740 . . . . . 6 (๐‘ฅ = ๐‘ โ†’ ((๐‘ฅ โ†‘ (๐ด + ๐ต)) = (๐‘… ฮฃg (๐‘˜ โˆˆ (0...๐‘ฅ) โ†ฆ ((๐‘ฅC๐‘˜) ยท (((๐‘ฅ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))) โ†” (๐‘ โ†‘ (๐ด + ๐ต)) = (๐‘… ฮฃg (๐‘˜ โˆˆ (0...๐‘) โ†ฆ ((๐‘C๐‘˜) ยท (((๐‘ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต)))))))
4443imbi2d 340 . . . . 5 (๐‘ฅ = ๐‘ โ†’ (((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ (๐‘ฅ โ†‘ (๐ด + ๐ต)) = (๐‘… ฮฃg (๐‘˜ โˆˆ (0...๐‘ฅ) โ†ฆ ((๐‘ฅC๐‘˜) ยท (((๐‘ฅ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต)))))) โ†” ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ (๐‘ โ†‘ (๐ด + ๐ต)) = (๐‘… ฮฃg (๐‘˜ โˆˆ (0...๐‘) โ†ฆ ((๐‘C๐‘˜) ยท (((๐‘ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))))))
45 simpr1 1191 . . . . . . . . . . 11 ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ ๐ด โˆˆ ๐‘†)
46 srgbinom.g . . . . . . . . . . . 12 ๐บ = (mulGrpโ€˜๐‘…)
47 srgbinom.s . . . . . . . . . . . 12 ๐‘† = (Baseโ€˜๐‘…)
4846, 47mgpbas 20034 . . . . . . . . . . 11 ๐‘† = (Baseโ€˜๐บ)
4945, 48eleqtrdi 2835 . . . . . . . . . 10 ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ ๐ด โˆˆ (Baseโ€˜๐บ))
50 eqid 2724 . . . . . . . . . . 11 (Baseโ€˜๐บ) = (Baseโ€˜๐บ)
51 eqid 2724 . . . . . . . . . . 11 (0gโ€˜๐บ) = (0gโ€˜๐บ)
52 srgbinom.e . . . . . . . . . . 11 โ†‘ = (.gโ€˜๐บ)
5350, 51, 52mulg0 18991 . . . . . . . . . 10 (๐ด โˆˆ (Baseโ€˜๐บ) โ†’ (0 โ†‘ ๐ด) = (0gโ€˜๐บ))
5449, 53syl 17 . . . . . . . . 9 ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ (0 โ†‘ ๐ด) = (0gโ€˜๐บ))
55 simpr2 1192 . . . . . . . . . . 11 ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ ๐ต โˆˆ ๐‘†)
5655, 48eleqtrdi 2835 . . . . . . . . . 10 ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ ๐ต โˆˆ (Baseโ€˜๐บ))
5750, 51, 52mulg0 18991 . . . . . . . . . 10 (๐ต โˆˆ (Baseโ€˜๐บ) โ†’ (0 โ†‘ ๐ต) = (0gโ€˜๐บ))
5856, 57syl 17 . . . . . . . . 9 ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ (0 โ†‘ ๐ต) = (0gโ€˜๐บ))
5954, 58oveq12d 7419 . . . . . . . 8 ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ ((0 โ†‘ ๐ด) ร— (0 โ†‘ ๐ต)) = ((0gโ€˜๐บ) ร— (0gโ€˜๐บ)))
6059oveq2d 7417 . . . . . . 7 ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ (1 ยท ((0 โ†‘ ๐ด) ร— (0 โ†‘ ๐ต))) = (1 ยท ((0gโ€˜๐บ) ร— (0gโ€˜๐บ))))
61 eqid 2724 . . . . . . . . . . . . . 14 (1rโ€˜๐‘…) = (1rโ€˜๐‘…)
6247, 61srgidcl 20093 . . . . . . . . . . . . 13 (๐‘… โˆˆ SRing โ†’ (1rโ€˜๐‘…) โˆˆ ๐‘†)
6362ancli 548 . . . . . . . . . . . 12 (๐‘… โˆˆ SRing โ†’ (๐‘… โˆˆ SRing โˆง (1rโ€˜๐‘…) โˆˆ ๐‘†))
6463adantr 480 . . . . . . . . . . 11 ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ (๐‘… โˆˆ SRing โˆง (1rโ€˜๐‘…) โˆˆ ๐‘†))
65 srgbinom.m . . . . . . . . . . . 12 ร— = (.rโ€˜๐‘…)
6647, 65, 61srglidm 20096 . . . . . . . . . . 11 ((๐‘… โˆˆ SRing โˆง (1rโ€˜๐‘…) โˆˆ ๐‘†) โ†’ ((1rโ€˜๐‘…) ร— (1rโ€˜๐‘…)) = (1rโ€˜๐‘…))
6764, 66syl 17 . . . . . . . . . 10 ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ ((1rโ€˜๐‘…) ร— (1rโ€˜๐‘…)) = (1rโ€˜๐‘…))
6867oveq2d 7417 . . . . . . . . 9 ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ (1 ยท ((1rโ€˜๐‘…) ร— (1rโ€˜๐‘…))) = (1 ยท (1rโ€˜๐‘…)))
69 eqid 2724 . . . . . . . . . . . 12 (Baseโ€˜๐‘…) = (Baseโ€˜๐‘…)
7069, 61srgidcl 20093 . . . . . . . . . . 11 (๐‘… โˆˆ SRing โ†’ (1rโ€˜๐‘…) โˆˆ (Baseโ€˜๐‘…))
71 srgbinom.t . . . . . . . . . . . 12 ยท = (.gโ€˜๐‘…)
7269, 71mulg1 18997 . . . . . . . . . . 11 ((1rโ€˜๐‘…) โˆˆ (Baseโ€˜๐‘…) โ†’ (1 ยท (1rโ€˜๐‘…)) = (1rโ€˜๐‘…))
7370, 72syl 17 . . . . . . . . . 10 (๐‘… โˆˆ SRing โ†’ (1 ยท (1rโ€˜๐‘…)) = (1rโ€˜๐‘…))
7473adantr 480 . . . . . . . . 9 ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ (1 ยท (1rโ€˜๐‘…)) = (1rโ€˜๐‘…))
7568, 74eqtrd 2764 . . . . . . . 8 ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ (1 ยท ((1rโ€˜๐‘…) ร— (1rโ€˜๐‘…))) = (1rโ€˜๐‘…))
7646, 61ringidval 20077 . . . . . . . . 9 (1rโ€˜๐‘…) = (0gโ€˜๐บ)
77 id 22 . . . . . . . . . . . 12 ((1rโ€˜๐‘…) = (0gโ€˜๐บ) โ†’ (1rโ€˜๐‘…) = (0gโ€˜๐บ))
7877, 77oveq12d 7419 . . . . . . . . . . 11 ((1rโ€˜๐‘…) = (0gโ€˜๐บ) โ†’ ((1rโ€˜๐‘…) ร— (1rโ€˜๐‘…)) = ((0gโ€˜๐บ) ร— (0gโ€˜๐บ)))
7978oveq2d 7417 . . . . . . . . . 10 ((1rโ€˜๐‘…) = (0gโ€˜๐บ) โ†’ (1 ยท ((1rโ€˜๐‘…) ร— (1rโ€˜๐‘…))) = (1 ยท ((0gโ€˜๐บ) ร— (0gโ€˜๐บ))))
8079, 77eqeq12d 2740 . . . . . . . . 9 ((1rโ€˜๐‘…) = (0gโ€˜๐บ) โ†’ ((1 ยท ((1rโ€˜๐‘…) ร— (1rโ€˜๐‘…))) = (1rโ€˜๐‘…) โ†” (1 ยท ((0gโ€˜๐บ) ร— (0gโ€˜๐บ))) = (0gโ€˜๐บ)))
8176, 80ax-mp 5 . . . . . . . 8 ((1 ยท ((1rโ€˜๐‘…) ร— (1rโ€˜๐‘…))) = (1rโ€˜๐‘…) โ†” (1 ยท ((0gโ€˜๐บ) ร— (0gโ€˜๐บ))) = (0gโ€˜๐บ))
8275, 81sylib 217 . . . . . . 7 ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ (1 ยท ((0gโ€˜๐บ) ร— (0gโ€˜๐บ))) = (0gโ€˜๐บ))
8360, 82eqtrd 2764 . . . . . 6 ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ (1 ยท ((0 โ†‘ ๐ด) ร— (0 โ†‘ ๐ต))) = (0gโ€˜๐บ))
84 fz0sn 13597 . . . . . . . . . 10 (0...0) = {0}
8584a1i 11 . . . . . . . . 9 ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ (0...0) = {0})
8685mpteq1d 5233 . . . . . . . 8 ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ (๐‘˜ โˆˆ (0...0) โ†ฆ ((0C๐‘˜) ยท (((0 โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต)))) = (๐‘˜ โˆˆ {0} โ†ฆ ((0C๐‘˜) ยท (((0 โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต)))))
8786oveq2d 7417 . . . . . . 7 ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ (๐‘… ฮฃg (๐‘˜ โˆˆ (0...0) โ†ฆ ((0C๐‘˜) ยท (((0 โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))) = (๐‘… ฮฃg (๐‘˜ โˆˆ {0} โ†ฆ ((0C๐‘˜) ยท (((0 โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))))
88 srgmnd 20084 . . . . . . . . 9 (๐‘… โˆˆ SRing โ†’ ๐‘… โˆˆ Mnd)
8988adantr 480 . . . . . . . 8 ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ ๐‘… โˆˆ Mnd)
90 c0ex 11204 . . . . . . . . 9 0 โˆˆ V
9190a1i 11 . . . . . . . 8 ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ 0 โˆˆ V)
9276, 62eqeltrrid 2830 . . . . . . . . . 10 (๐‘… โˆˆ SRing โ†’ (0gโ€˜๐บ) โˆˆ ๐‘†)
9392adantr 480 . . . . . . . . 9 ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ (0gโ€˜๐บ) โˆˆ ๐‘†)
9483, 93eqeltrd 2825 . . . . . . . 8 ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ (1 ยท ((0 โ†‘ ๐ด) ร— (0 โ†‘ ๐ต))) โˆˆ ๐‘†)
95 oveq2 7409 . . . . . . . . . . 11 (๐‘˜ = 0 โ†’ (0C๐‘˜) = (0C0))
96 0nn0 12483 . . . . . . . . . . . 12 0 โˆˆ โ„•0
97 bcn0 14266 . . . . . . . . . . . 12 (0 โˆˆ โ„•0 โ†’ (0C0) = 1)
9896, 97ax-mp 5 . . . . . . . . . . 11 (0C0) = 1
9995, 98eqtrdi 2780 . . . . . . . . . 10 (๐‘˜ = 0 โ†’ (0C๐‘˜) = 1)
100 oveq2 7409 . . . . . . . . . . . . 13 (๐‘˜ = 0 โ†’ (0 โˆ’ ๐‘˜) = (0 โˆ’ 0))
101 0m0e0 12328 . . . . . . . . . . . . 13 (0 โˆ’ 0) = 0
102100, 101eqtrdi 2780 . . . . . . . . . . . 12 (๐‘˜ = 0 โ†’ (0 โˆ’ ๐‘˜) = 0)
103102oveq1d 7416 . . . . . . . . . . 11 (๐‘˜ = 0 โ†’ ((0 โˆ’ ๐‘˜) โ†‘ ๐ด) = (0 โ†‘ ๐ด))
104 oveq1 7408 . . . . . . . . . . 11 (๐‘˜ = 0 โ†’ (๐‘˜ โ†‘ ๐ต) = (0 โ†‘ ๐ต))
105103, 104oveq12d 7419 . . . . . . . . . 10 (๐‘˜ = 0 โ†’ (((0 โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต)) = ((0 โ†‘ ๐ด) ร— (0 โ†‘ ๐ต)))
10699, 105oveq12d 7419 . . . . . . . . 9 (๐‘˜ = 0 โ†’ ((0C๐‘˜) ยท (((0 โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))) = (1 ยท ((0 โ†‘ ๐ด) ร— (0 โ†‘ ๐ต))))
10747, 106gsumsn 19863 . . . . . . . 8 ((๐‘… โˆˆ Mnd โˆง 0 โˆˆ V โˆง (1 ยท ((0 โ†‘ ๐ด) ร— (0 โ†‘ ๐ต))) โˆˆ ๐‘†) โ†’ (๐‘… ฮฃg (๐‘˜ โˆˆ {0} โ†ฆ ((0C๐‘˜) ยท (((0 โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))) = (1 ยท ((0 โ†‘ ๐ด) ร— (0 โ†‘ ๐ต))))
10889, 91, 94, 107syl3anc 1368 . . . . . . 7 ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ (๐‘… ฮฃg (๐‘˜ โˆˆ {0} โ†ฆ ((0C๐‘˜) ยท (((0 โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))) = (1 ยท ((0 โ†‘ ๐ด) ร— (0 โ†‘ ๐ต))))
10987, 108eqtrd 2764 . . . . . 6 ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ (๐‘… ฮฃg (๐‘˜ โˆˆ (0...0) โ†ฆ ((0C๐‘˜) ยท (((0 โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))) = (1 ยท ((0 โ†‘ ๐ด) ร— (0 โ†‘ ๐ต))))
110 srgbinom.a . . . . . . . . . 10 + = (+gโ€˜๐‘…)
11147, 110mndcl 18664 . . . . . . . . 9 ((๐‘… โˆˆ Mnd โˆง ๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘†) โ†’ (๐ด + ๐ต) โˆˆ ๐‘†)
11289, 45, 55, 111syl3anc 1368 . . . . . . . 8 ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ (๐ด + ๐ต) โˆˆ ๐‘†)
113112, 48eleqtrdi 2835 . . . . . . 7 ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ (๐ด + ๐ต) โˆˆ (Baseโ€˜๐บ))
11450, 51, 52mulg0 18991 . . . . . . 7 ((๐ด + ๐ต) โˆˆ (Baseโ€˜๐บ) โ†’ (0 โ†‘ (๐ด + ๐ต)) = (0gโ€˜๐บ))
115113, 114syl 17 . . . . . 6 ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ (0 โ†‘ (๐ด + ๐ต)) = (0gโ€˜๐บ))
11683, 109, 1153eqtr4rd 2775 . . . . 5 ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ (0 โ†‘ (๐ด + ๐ต)) = (๐‘… ฮฃg (๐‘˜ โˆˆ (0...0) โ†ฆ ((0C๐‘˜) ยท (((0 โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))))
117 simprl 768 . . . . . . . 8 ((๐‘› โˆˆ โ„•0 โˆง (๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด)))) โ†’ ๐‘… โˆˆ SRing)
11845adantl 481 . . . . . . . 8 ((๐‘› โˆˆ โ„•0 โˆง (๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด)))) โ†’ ๐ด โˆˆ ๐‘†)
11955adantl 481 . . . . . . . 8 ((๐‘› โˆˆ โ„•0 โˆง (๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด)))) โ†’ ๐ต โˆˆ ๐‘†)
120 simprr3 1220 . . . . . . . 8 ((๐‘› โˆˆ โ„•0 โˆง (๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด)))) โ†’ (๐ด ร— ๐ต) = (๐ต ร— ๐ด))
121 simpl 482 . . . . . . . 8 ((๐‘› โˆˆ โ„•0 โˆง (๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด)))) โ†’ ๐‘› โˆˆ โ„•0)
122 id 22 . . . . . . . 8 ((๐‘› โ†‘ (๐ด + ๐ต)) = (๐‘… ฮฃg (๐‘˜ โˆˆ (0...๐‘›) โ†ฆ ((๐‘›C๐‘˜) ยท (((๐‘› โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))) โ†’ (๐‘› โ†‘ (๐ด + ๐ต)) = (๐‘… ฮฃg (๐‘˜ โˆˆ (0...๐‘›) โ†ฆ ((๐‘›C๐‘˜) ยท (((๐‘› โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))))
12347, 65, 71, 110, 46, 52, 117, 118, 119, 120, 121, 122srgbinomlem 20124 . . . . . . 7 (((๐‘› โˆˆ โ„•0 โˆง (๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด)))) โˆง (๐‘› โ†‘ (๐ด + ๐ต)) = (๐‘… ฮฃg (๐‘˜ โˆˆ (0...๐‘›) โ†ฆ ((๐‘›C๐‘˜) ยท (((๐‘› โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต)))))) โ†’ ((๐‘› + 1) โ†‘ (๐ด + ๐ต)) = (๐‘… ฮฃg (๐‘˜ โˆˆ (0...(๐‘› + 1)) โ†ฆ (((๐‘› + 1)C๐‘˜) ยท ((((๐‘› + 1) โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))))
124123exp31 419 . . . . . 6 (๐‘› โˆˆ โ„•0 โ†’ ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ ((๐‘› โ†‘ (๐ด + ๐ต)) = (๐‘… ฮฃg (๐‘˜ โˆˆ (0...๐‘›) โ†ฆ ((๐‘›C๐‘˜) ยท (((๐‘› โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))) โ†’ ((๐‘› + 1) โ†‘ (๐ด + ๐ต)) = (๐‘… ฮฃg (๐‘˜ โˆˆ (0...(๐‘› + 1)) โ†ฆ (((๐‘› + 1)C๐‘˜) ยท ((((๐‘› + 1) โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))))))
125124a2d 29 . . . . 5 (๐‘› โˆˆ โ„•0 โ†’ (((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ (๐‘› โ†‘ (๐ด + ๐ต)) = (๐‘… ฮฃg (๐‘˜ โˆˆ (0...๐‘›) โ†ฆ ((๐‘›C๐‘˜) ยท (((๐‘› โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต)))))) โ†’ ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ ((๐‘› + 1) โ†‘ (๐ด + ๐ต)) = (๐‘… ฮฃg (๐‘˜ โˆˆ (0...(๐‘› + 1)) โ†ฆ (((๐‘› + 1)C๐‘˜) ยท ((((๐‘› + 1) โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))))))
12611, 22, 33, 44, 116, 125nn0ind 12653 . . . 4 (๐‘ โˆˆ โ„•0 โ†’ ((๐‘… โˆˆ SRing โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ (๐‘ โ†‘ (๐ด + ๐ต)) = (๐‘… ฮฃg (๐‘˜ โˆˆ (0...๐‘) โ†ฆ ((๐‘C๐‘˜) ยท (((๐‘ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต)))))))
127126expd 415 . . 3 (๐‘ โˆˆ โ„•0 โ†’ (๐‘… โˆˆ SRing โ†’ ((๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด)) โ†’ (๐‘ โ†‘ (๐ด + ๐ต)) = (๐‘… ฮฃg (๐‘˜ โˆˆ (0...๐‘) โ†ฆ ((๐‘C๐‘˜) ยท (((๐‘ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))))))
128127impcom 407 . 2 ((๐‘… โˆˆ SRing โˆง ๐‘ โˆˆ โ„•0) โ†’ ((๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด)) โ†’ (๐‘ โ†‘ (๐ด + ๐ต)) = (๐‘… ฮฃg (๐‘˜ โˆˆ (0...๐‘) โ†ฆ ((๐‘C๐‘˜) ยท (((๐‘ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต)))))))
129128imp 406 1 (((๐‘… โˆˆ SRing โˆง ๐‘ โˆˆ โ„•0) โˆง (๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† โˆง (๐ด ร— ๐ต) = (๐ต ร— ๐ด))) โ†’ (๐‘ โ†‘ (๐ด + ๐ต)) = (๐‘… ฮฃg (๐‘˜ โˆˆ (0...๐‘) โ†ฆ ((๐‘C๐‘˜) ยท (((๐‘ โˆ’ ๐‘˜) โ†‘ ๐ด) ร— (๐‘˜ โ†‘ ๐ต))))))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 395   โˆง w3a 1084   = wceq 1533   โˆˆ wcel 2098  Vcvv 3466  {csn 4620   โ†ฆ cmpt 5221  โ€˜cfv 6533  (class class class)co 7401  0cc0 11105  1c1 11106   + caddc 11108   โˆ’ cmin 11440  โ„•0cn0 12468  ...cfz 13480  Ccbc 14258  Basecbs 17142  +gcplusg 17195  .rcmulr 17196  0gc0g 17383   ฮฃg cgsu 17384  Mndcmnd 18656  .gcmg 18984  mulGrpcmgp 20028  1rcur 20075  SRingcsrg 20080
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-map 8817  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-div 11868  df-nn 12209  df-2 12271  df-n0 12469  df-z 12555  df-uz 12819  df-rp 12971  df-fz 13481  df-fzo 13624  df-seq 13963  df-fac 14230  df-bc 14259  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-mhm 18702  df-submnd 18703  df-mulg 18985  df-cntz 19222  df-cmn 19691  df-mgp 20029  df-ur 20076  df-srg 20081
This theorem is referenced by:  csrgbinom  20126
  Copyright terms: Public domain W3C validator