freshmansdream

Description: For a prime number P , if X and Y are members of a commutative ring R of characteristic P , then ( ( X + Y ) ^ P ) = ( ( X ^ P ) + ( Y ^ P ) ) . This theorem is sometimes referred to as "the freshman's dream" . (Contributed by Thierry Arnoux, 18-Sep-2023)

	Ref	Expression
Hypotheses	freshmansdream.s	$⊢ B = {Base}_{R}$
	freshmansdream.a	$⊢ \underset{˙}{+} = +_{R}$
	freshmansdream.p	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{R}}$
	freshmansdream.c	$⊢ P = chr (R)$
	freshmansdream.r	$⊢ φ \to R \in CRing$
	freshmansdream.1	$⊢ φ \to P \in ℙ$
	freshmansdream.x	$⊢ φ \to X \in B$
	freshmansdream.y	$⊢ φ \to Y \in B$
Assertion	freshmansdream	$⊢ φ \to P \underset{˙}{\times} (X \underset{˙}{+} Y) = (P \underset{˙}{\times} X) \underset{˙}{+} (P \underset{˙}{\times} Y)$

Proof

Step	Hyp	Ref	Expression
1		freshmansdream.s	$⊢ B = {Base}_{R}$
2		freshmansdream.a	$⊢ \underset{˙}{+} = +_{R}$
3		freshmansdream.p	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{R}}$
4		freshmansdream.c	$⊢ P = chr (R)$
5		freshmansdream.r	$⊢ φ \to R \in CRing$
6		freshmansdream.1	$⊢ φ \to P \in ℙ$
7		freshmansdream.x	$⊢ φ \to X \in B$
8		freshmansdream.y	$⊢ φ \to Y \in B$
9		crngring	$⊢ R \in CRing \to R \in Ring$
10	4	chrcl	$⊢ R \in Ring \to P \in ℕ_{0}$
11	5 9 10	3syl	$⊢ φ \to P \in ℕ_{0}$
12		eqid	$⊢ \cdot_{R} = \cdot_{R}$
13		eqid	$⊢ \cdot_{R} = \cdot_{R}$
14		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
15	1 12 13 2 14 3	crngbinom	$⊢ ((R \in CRing \land P \in ℕ_{0}) \land (X \in B \land Y \in B)) \to P \underset{˙}{\times} (X \underset{˙}{+} Y) = {\sum_{R}}_{i = 0}^{P} ((\binom{P}{i}) \cdot_{R} (((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y)))$
16	5 11 7 8 15	syl22anc	$⊢ φ \to P \underset{˙}{\times} (X \underset{˙}{+} Y) = {\sum_{R}}_{i = 0}^{P} ((\binom{P}{i}) \cdot_{R} (((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y)))$
17	11	nn0cnd	$⊢ φ \to P \in ℂ$
18		1cnd	$⊢ φ \to 1 \in ℂ$
19	17 18	npcand	$⊢ φ \to P - 1 + 1 = P$
20	19	oveq2d	$⊢ φ \to (0 \dots P - 1 + 1) = (0 \dots P)$
21	20	eqcomd	$⊢ φ \to (0 \dots P) = (0 \dots P - 1 + 1)$
22	21	mpteq1d	$⊢ φ \to (i \in (0 \dots P) ⟼ (\binom{P}{i}) \cdot_{R} (((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y))) = (i \in (0 \dots P - 1 + 1) ⟼ (\binom{P}{i}) \cdot_{R} (((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y)))$
23	22	oveq2d	$⊢ φ \to {\sum_{R}}_{i = 0}^{P} ((\binom{P}{i}) \cdot_{R} (((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y))) = {\sum_{R}}_{i = 0}^{P - 1 + 1} ((\binom{P}{i}) \cdot_{R} (((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y)))$
24		ringcmn	$⊢ R \in Ring \to R \in CMnd$
25	5 9 24	3syl	$⊢ φ \to R \in CMnd$
26		prmnn	$⊢ P \in ℙ \to P \in ℕ$
27		nnm1nn0	$⊢ P \in ℕ \to P - 1 \in ℕ_{0}$
28	6 26 27	3syl	$⊢ φ \to P - 1 \in ℕ_{0}$
29		ringgrp	$⊢ R \in Ring \to R \in Grp$
30	5 9 29	3syl	$⊢ φ \to R \in Grp$
31	30	adantr	$⊢ (φ \land i \in (0 \dots P - 1 + 1)) \to R \in Grp$
32	11	adantr	$⊢ (φ \land i \in (0 \dots P - 1 + 1)) \to P \in ℕ_{0}$
33		fzssz	$⊢ (0 \dots P - 1 + 1) \subseteq ℤ$
34	33	a1i	$⊢ φ \to (0 \dots P - 1 + 1) \subseteq ℤ$
35	34	sselda	$⊢ (φ \land i \in (0 \dots P - 1 + 1)) \to i \in ℤ$
36		bccl	$⊢ (P \in ℕ_{0} \land i \in ℤ) \to (\binom{P}{i}) \in ℕ_{0}$
37	32 35 36	syl2anc	$⊢ (φ \land i \in (0 \dots P - 1 + 1)) \to (\binom{P}{i}) \in ℕ_{0}$
38	37	nn0zd	$⊢ (φ \land i \in (0 \dots P - 1 + 1)) \to (\binom{P}{i}) \in ℤ$
39	5 9	syl	$⊢ φ \to R \in Ring$
40	39	adantr	$⊢ (φ \land i \in (0 \dots P - 1 + 1)) \to R \in Ring$
41	14 1	mgpbas	$⊢ B = {Base}_{{mulGrp}_{R}}$
42	14	ringmgp	$⊢ R \in Ring \to {mulGrp}_{R} \in Mnd$
43	39 42	syl	$⊢ φ \to {mulGrp}_{R} \in Mnd$
44	43	adantr	$⊢ (φ \land i \in (0 \dots P - 1 + 1)) \to {mulGrp}_{R} \in Mnd$
45		simpr	$⊢ (φ \land i \in (0 \dots P - 1 + 1)) \to i \in (0 \dots P - 1 + 1)$
46	20	adantr	$⊢ (φ \land i \in (0 \dots P - 1 + 1)) \to (0 \dots P - 1 + 1) = (0 \dots P)$
47	45 46	eleqtrd	$⊢ (φ \land i \in (0 \dots P - 1 + 1)) \to i \in (0 \dots P)$
48		fznn0sub	$⊢ i \in (0 \dots P) \to P - i \in ℕ_{0}$
49	47 48	syl	$⊢ (φ \land i \in (0 \dots P - 1 + 1)) \to P - i \in ℕ_{0}$
50	7	adantr	$⊢ (φ \land i \in (0 \dots P - 1 + 1)) \to X \in B$
51	41 3 44 49 50	mulgnn0cld	$⊢ (φ \land i \in (0 \dots P - 1 + 1)) \to (P - i) \underset{˙}{\times} X \in B$
52		elfznn0	$⊢ i \in (0 \dots P - 1 + 1) \to i \in ℕ_{0}$
53	52	adantl	$⊢ (φ \land i \in (0 \dots P - 1 + 1)) \to i \in ℕ_{0}$
54	8	adantr	$⊢ (φ \land i \in (0 \dots P - 1 + 1)) \to Y \in B$
55	41 3 44 53 54	mulgnn0cld	$⊢ (φ \land i \in (0 \dots P - 1 + 1)) \to i \underset{˙}{\times} Y \in B$
56	1 12	ringcl	$⊢ (R \in Ring \land (P - i) \underset{˙}{\times} X \in B \land i \underset{˙}{\times} Y \in B) \to ((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y) \in B$
57	40 51 55 56	syl3anc	$⊢ (φ \land i \in (0 \dots P - 1 + 1)) \to ((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y) \in B$
58	1 13	mulgcl	$⊢ (R \in Grp \land (\binom{P}{i}) \in ℤ \land ((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y) \in B) \to (\binom{P}{i}) \cdot_{R} (((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y)) \in B$
59	31 38 57 58	syl3anc	$⊢ (φ \land i \in (0 \dots P - 1 + 1)) \to (\binom{P}{i}) \cdot_{R} (((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y)) \in B$
60	1 2 25 28 59	gsummptfzsplit	$⊢ φ \to {\sum_{R}}_{i = 0}^{P - 1 + 1} ((\binom{P}{i}) \cdot_{R} (((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y))) = ({\sum_{R}}_{i = 0}^{P - 1}, ((\binom{P}{i}) \cdot_{R} (((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y)))) \underset{˙}{+} (\underset{i \in \{P - 1 + 1\}}{\sum_{R}}, ((\binom{P}{i}) \cdot_{R} (((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y))))$
61	30	adantr	$⊢ (φ \land i \in (0 \dots P - 1)) \to R \in Grp$
62		elfzelz	$⊢ i \in (0 \dots P - 1) \to i \in ℤ$
63	11 62 36	syl2an	$⊢ (φ \land i \in (0 \dots P - 1)) \to (\binom{P}{i}) \in ℕ_{0}$
64	63	nn0zd	$⊢ (φ \land i \in (0 \dots P - 1)) \to (\binom{P}{i}) \in ℤ$
65	39	adantr	$⊢ (φ \land i \in (0 \dots P - 1)) \to R \in Ring$
66	65 42	syl	$⊢ (φ \land i \in (0 \dots P - 1)) \to {mulGrp}_{R} \in Mnd$
67		fzssp1	$⊢ (0 \dots P - 1) \subseteq (0 \dots P - 1 + 1)$
68	67 20	sseqtrid	$⊢ φ \to (0 \dots P - 1) \subseteq (0 \dots P)$
69	68	sselda	$⊢ (φ \land i \in (0 \dots P - 1)) \to i \in (0 \dots P)$
70	69 48	syl	$⊢ (φ \land i \in (0 \dots P - 1)) \to P - i \in ℕ_{0}$
71	7	adantr	$⊢ (φ \land i \in (0 \dots P - 1)) \to X \in B$
72	41 3 66 70 71	mulgnn0cld	$⊢ (φ \land i \in (0 \dots P - 1)) \to (P - i) \underset{˙}{\times} X \in B$
73		elfznn0	$⊢ i \in (0 \dots P - 1) \to i \in ℕ_{0}$
74	73	adantl	$⊢ (φ \land i \in (0 \dots P - 1)) \to i \in ℕ_{0}$
75	8	adantr	$⊢ (φ \land i \in (0 \dots P - 1)) \to Y \in B$
76	41 3 66 74 75	mulgnn0cld	$⊢ (φ \land i \in (0 \dots P - 1)) \to i \underset{˙}{\times} Y \in B$
77	65 72 76 56	syl3anc	$⊢ (φ \land i \in (0 \dots P - 1)) \to ((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y) \in B$
78	61 64 77 58	syl3anc	$⊢ (φ \land i \in (0 \dots P - 1)) \to (\binom{P}{i}) \cdot_{R} (((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y)) \in B$
79	1 2 25 28 78	gsummptfzsplitl	$⊢ φ \to {\sum_{R}}_{i = 0}^{P - 1} ((\binom{P}{i}) \cdot_{R} (((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y))) = ({\sum_{R}}_{i = 1}^{P - 1}, ((\binom{P}{i}) \cdot_{R} (((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y)))) \underset{˙}{+} (\underset{i \in \{0\}}{\sum_{R}}, ((\binom{P}{i}) \cdot_{R} (((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y))))$
80	39	adantr	$⊢ (φ \land i \in (1 \dots P - 1)) \to R \in Ring$
81		prmdvdsbc	$⊢ (P \in ℙ \land i \in (1 \dots P - 1)) \to P ∥ (\binom{P}{i})$
82	6 81	sylan	$⊢ (φ \land i \in (1 \dots P - 1)) \to P ∥ (\binom{P}{i})$
83	80 42	syl	$⊢ (φ \land i \in (1 \dots P - 1)) \to {mulGrp}_{R} \in Mnd$
84	11	nn0zd	$⊢ φ \to P \in ℤ$
85		1nn0	$⊢ 1 \in ℕ_{0}$
86		eluzmn	$⊢ (P \in ℤ \land 1 \in ℕ_{0}) \to P \in ℤ_{\geq (P - 1)}$
87	84 85 86	sylancl	$⊢ φ \to P \in ℤ_{\geq (P - 1)}$
88		fzss2	$⊢ P \in ℤ_{\geq (P - 1)} \to (1 \dots P - 1) \subseteq (1 \dots P)$
89	87 88	syl	$⊢ φ \to (1 \dots P - 1) \subseteq (1 \dots P)$
90	89	sselda	$⊢ (φ \land i \in (1 \dots P - 1)) \to i \in (1 \dots P)$
91		fznn0sub	$⊢ i \in (1 \dots P) \to P - i \in ℕ_{0}$
92	90 91	syl	$⊢ (φ \land i \in (1 \dots P - 1)) \to P - i \in ℕ_{0}$
93	7	adantr	$⊢ (φ \land i \in (1 \dots P - 1)) \to X \in B$
94	41 3 83 92 93	mulgnn0cld	$⊢ (φ \land i \in (1 \dots P - 1)) \to (P - i) \underset{˙}{\times} X \in B$
95		elfznn	$⊢ i \in (1 \dots P - 1) \to i \in ℕ$
96	95	nnnn0d	$⊢ i \in (1 \dots P - 1) \to i \in ℕ_{0}$
97	96	adantl	$⊢ (φ \land i \in (1 \dots P - 1)) \to i \in ℕ_{0}$
98	8	adantr	$⊢ (φ \land i \in (1 \dots P - 1)) \to Y \in B$
99	41 3 83 97 98	mulgnn0cld	$⊢ (φ \land i \in (1 \dots P - 1)) \to i \underset{˙}{\times} Y \in B$
100	80 94 99 56	syl3anc	$⊢ (φ \land i \in (1 \dots P - 1)) \to ((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y) \in B$
101		eqid	$⊢ 0_{R} = 0_{R}$
102	4 1 13 101	dvdschrmulg	$⊢ (R \in Ring \land P ∥ (\binom{P}{i}) \land ((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y) \in B) \to (\binom{P}{i}) \cdot_{R} (((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y)) = 0_{R}$
103	80 82 100 102	syl3anc	$⊢ (φ \land i \in (1 \dots P - 1)) \to (\binom{P}{i}) \cdot_{R} (((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y)) = 0_{R}$
104	103	mpteq2dva	$⊢ φ \to (i \in (1 \dots P - 1) ⟼ (\binom{P}{i}) \cdot_{R} (((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y))) = (i \in (1 \dots P - 1) ⟼ 0_{R})$
105	104	oveq2d	$⊢ φ \to {\sum_{R}}_{i = 1}^{P - 1} ((\binom{P}{i}) \cdot_{R} (((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y))) = {\sum_{R}}_{i = 1}^{P - 1} 0_{R}$
106		ringmnd	$⊢ R \in Ring \to R \in Mnd$
107	39 106	syl	$⊢ φ \to R \in Mnd$
108		ovex	$⊢ (1 \dots P - 1) \in V$
109	101	gsumz	$⊢ (R \in Mnd \land (1 \dots P - 1) \in V) \to {\sum_{R}}_{i = 1}^{P - 1} 0_{R} = 0_{R}$
110	107 108 109	sylancl	$⊢ φ \to {\sum_{R}}_{i = 1}^{P - 1} 0_{R} = 0_{R}$
111	105 110	eqtrd	$⊢ φ \to {\sum_{R}}_{i = 1}^{P - 1} ((\binom{P}{i}) \cdot_{R} (((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y))) = 0_{R}$
112		0nn0	$⊢ 0 \in ℕ_{0}$
113	112	a1i	$⊢ φ \to 0 \in ℕ_{0}$
114	41 3 43 11 7	mulgnn0cld	$⊢ φ \to P \underset{˙}{\times} X \in B$
115		simpr	$⊢ (φ \land i = 0) \to i = 0$
116	115	oveq2d	$⊢ (φ \land i = 0) \to (\binom{P}{i}) = (\binom{P}{0})$
117	115	oveq2d	$⊢ (φ \land i = 0) \to P - i = P - 0$
118	117	oveq1d	$⊢ (φ \land i = 0) \to (P - i) \underset{˙}{\times} X = (P - 0) \underset{˙}{\times} X$
119	115	oveq1d	$⊢ (φ \land i = 0) \to i \underset{˙}{\times} Y = 0 \underset{˙}{\times} Y$
120	118 119	oveq12d	$⊢ (φ \land i = 0) \to ((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y) = ((P - 0) \underset{˙}{\times} X) \cdot_{R} (0 \underset{˙}{\times} Y)$
121	116 120	oveq12d	$⊢ (φ \land i = 0) \to (\binom{P}{i}) \cdot_{R} (((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y)) = (\binom{P}{0}) \cdot_{R} (((P - 0) \underset{˙}{\times} X) \cdot_{R} (0 \underset{˙}{\times} Y))$
122		bcn0	$⊢ P \in ℕ_{0} \to (\binom{P}{0}) = 1$
123	11 122	syl	$⊢ φ \to (\binom{P}{0}) = 1$
124	17	subid1d	$⊢ φ \to P - 0 = P$
125	124	oveq1d	$⊢ φ \to (P - 0) \underset{˙}{\times} X = P \underset{˙}{\times} X$
126		eqid	$⊢ 1_{R} = 1_{R}$
127	14 126	ringidval	$⊢ 1_{R} = 0_{{mulGrp}_{R}}$
128	41 127 3	mulg0	$⊢ Y \in B \to 0 \underset{˙}{\times} Y = 1_{R}$
129	8 128	syl	$⊢ φ \to 0 \underset{˙}{\times} Y = 1_{R}$
130	125 129	oveq12d	$⊢ φ \to ((P - 0) \underset{˙}{\times} X) \cdot_{R} (0 \underset{˙}{\times} Y) = (P \underset{˙}{\times} X) \cdot_{R} 1_{R}$
131	1 12 126	ringridm	$⊢ (R \in Ring \land P \underset{˙}{\times} X \in B) \to (P \underset{˙}{\times} X) \cdot_{R} 1_{R} = P \underset{˙}{\times} X$
132	39 114 131	syl2anc	$⊢ φ \to (P \underset{˙}{\times} X) \cdot_{R} 1_{R} = P \underset{˙}{\times} X$
133	130 132	eqtrd	$⊢ φ \to ((P - 0) \underset{˙}{\times} X) \cdot_{R} (0 \underset{˙}{\times} Y) = P \underset{˙}{\times} X$
134	123 133	oveq12d	$⊢ φ \to (\binom{P}{0}) \cdot_{R} (((P - 0) \underset{˙}{\times} X) \cdot_{R} (0 \underset{˙}{\times} Y)) = 1 \cdot_{R} (P \underset{˙}{\times} X)$
135	1 13	mulg1	$⊢ P \underset{˙}{\times} X \in B \to 1 \cdot_{R} (P \underset{˙}{\times} X) = P \underset{˙}{\times} X$
136	114 135	syl	$⊢ φ \to 1 \cdot_{R} (P \underset{˙}{\times} X) = P \underset{˙}{\times} X$
137	134 136	eqtrd	$⊢ φ \to (\binom{P}{0}) \cdot_{R} (((P - 0) \underset{˙}{\times} X) \cdot_{R} (0 \underset{˙}{\times} Y)) = P \underset{˙}{\times} X$
138	137	adantr	$⊢ (φ \land i = 0) \to (\binom{P}{0}) \cdot_{R} (((P - 0) \underset{˙}{\times} X) \cdot_{R} (0 \underset{˙}{\times} Y)) = P \underset{˙}{\times} X$
139	121 138	eqtrd	$⊢ (φ \land i = 0) \to (\binom{P}{i}) \cdot_{R} (((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y)) = P \underset{˙}{\times} X$
140	1 107 113 114 139	gsumsnd	$⊢ φ \to \underset{i \in \{0\}}{\sum_{R}} ((\binom{P}{i}) \cdot_{R} (((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y))) = P \underset{˙}{\times} X$
141	111 140	oveq12d	$⊢ φ \to ({\sum_{R}}_{i = 1}^{P - 1}, ((\binom{P}{i}) \cdot_{R} (((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y)))) \underset{˙}{+} (\underset{i \in \{0\}}{\sum_{R}}, ((\binom{P}{i}) \cdot_{R} (((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y)))) = 0_{R} \underset{˙}{+} (P \underset{˙}{\times} X)$
142	1 2 101	grplid	$⊢ (R \in Grp \land P \underset{˙}{\times} X \in B) \to 0_{R} \underset{˙}{+} (P \underset{˙}{\times} X) = P \underset{˙}{\times} X$
143	30 114 142	syl2anc	$⊢ φ \to 0_{R} \underset{˙}{+} (P \underset{˙}{\times} X) = P \underset{˙}{\times} X$
144	79 141 143	3eqtrd	$⊢ φ \to {\sum_{R}}_{i = 0}^{P - 1} ((\binom{P}{i}) \cdot_{R} (((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y))) = P \underset{˙}{\times} X$
145	19 11	eqeltrd	$⊢ φ \to P - 1 + 1 \in ℕ_{0}$
146	41 3 43 11 8	mulgnn0cld	$⊢ φ \to P \underset{˙}{\times} Y \in B$
147		simpr	$⊢ (φ \land i = P - 1 + 1) \to i = P - 1 + 1$
148	19	adantr	$⊢ (φ \land i = P - 1 + 1) \to P - 1 + 1 = P$
149	147 148	eqtrd	$⊢ (φ \land i = P - 1 + 1) \to i = P$
150	149	oveq2d	$⊢ (φ \land i = P - 1 + 1) \to (\binom{P}{i}) = (\binom{P}{P})$
151	149	oveq2d	$⊢ (φ \land i = P - 1 + 1) \to P - i = P - P$
152	151	oveq1d	$⊢ (φ \land i = P - 1 + 1) \to (P - i) \underset{˙}{\times} X = (P - P) \underset{˙}{\times} X$
153	149	oveq1d	$⊢ (φ \land i = P - 1 + 1) \to i \underset{˙}{\times} Y = P \underset{˙}{\times} Y$
154	152 153	oveq12d	$⊢ (φ \land i = P - 1 + 1) \to ((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y) = ((P - P) \underset{˙}{\times} X) \cdot_{R} (P \underset{˙}{\times} Y)$
155	150 154	oveq12d	$⊢ (φ \land i = P - 1 + 1) \to (\binom{P}{i}) \cdot_{R} (((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y)) = (\binom{P}{P}) \cdot_{R} (((P - P) \underset{˙}{\times} X) \cdot_{R} (P \underset{˙}{\times} Y))$
156		bcnn	$⊢ P \in ℕ_{0} \to (\binom{P}{P}) = 1$
157	11 156	syl	$⊢ φ \to (\binom{P}{P}) = 1$
158	17	subidd	$⊢ φ \to P - P = 0$
159	158	oveq1d	$⊢ φ \to (P - P) \underset{˙}{\times} X = 0 \underset{˙}{\times} X$
160	41 127 3	mulg0	$⊢ X \in B \to 0 \underset{˙}{\times} X = 1_{R}$
161	7 160	syl	$⊢ φ \to 0 \underset{˙}{\times} X = 1_{R}$
162	159 161	eqtrd	$⊢ φ \to (P - P) \underset{˙}{\times} X = 1_{R}$
163	162	oveq1d	$⊢ φ \to ((P - P) \underset{˙}{\times} X) \cdot_{R} (P \underset{˙}{\times} Y) = 1_{R} \cdot_{R} (P \underset{˙}{\times} Y)$
164	1 12 126	ringlidm	$⊢ (R \in Ring \land P \underset{˙}{\times} Y \in B) \to 1_{R} \cdot_{R} (P \underset{˙}{\times} Y) = P \underset{˙}{\times} Y$
165	39 146 164	syl2anc	$⊢ φ \to 1_{R} \cdot_{R} (P \underset{˙}{\times} Y) = P \underset{˙}{\times} Y$
166	163 165	eqtrd	$⊢ φ \to ((P - P) \underset{˙}{\times} X) \cdot_{R} (P \underset{˙}{\times} Y) = P \underset{˙}{\times} Y$
167	157 166	oveq12d	$⊢ φ \to (\binom{P}{P}) \cdot_{R} (((P - P) \underset{˙}{\times} X) \cdot_{R} (P \underset{˙}{\times} Y)) = 1 \cdot_{R} (P \underset{˙}{\times} Y)$
168	1 13	mulg1	$⊢ P \underset{˙}{\times} Y \in B \to 1 \cdot_{R} (P \underset{˙}{\times} Y) = P \underset{˙}{\times} Y$
169	146 168	syl	$⊢ φ \to 1 \cdot_{R} (P \underset{˙}{\times} Y) = P \underset{˙}{\times} Y$
170	167 169	eqtrd	$⊢ φ \to (\binom{P}{P}) \cdot_{R} (((P - P) \underset{˙}{\times} X) \cdot_{R} (P \underset{˙}{\times} Y)) = P \underset{˙}{\times} Y$
171	170	adantr	$⊢ (φ \land i = P - 1 + 1) \to (\binom{P}{P}) \cdot_{R} (((P - P) \underset{˙}{\times} X) \cdot_{R} (P \underset{˙}{\times} Y)) = P \underset{˙}{\times} Y$
172	155 171	eqtrd	$⊢ (φ \land i = P - 1 + 1) \to (\binom{P}{i}) \cdot_{R} (((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y)) = P \underset{˙}{\times} Y$
173	1 107 145 146 172	gsumsnd	$⊢ φ \to \underset{i \in \{P - 1 + 1\}}{\sum_{R}} ((\binom{P}{i}) \cdot_{R} (((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y))) = P \underset{˙}{\times} Y$
174	144 173	oveq12d	$⊢ φ \to ({\sum_{R}}_{i = 0}^{P - 1}, ((\binom{P}{i}) \cdot_{R} (((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y)))) \underset{˙}{+} (\underset{i \in \{P - 1 + 1\}}{\sum_{R}}, ((\binom{P}{i}) \cdot_{R} (((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y)))) = (P \underset{˙}{\times} X) \underset{˙}{+} (P \underset{˙}{\times} Y)$
175	60 174	eqtrd	$⊢ φ \to {\sum_{R}}_{i = 0}^{P - 1 + 1} ((\binom{P}{i}) \cdot_{R} (((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y))) = (P \underset{˙}{\times} X) \underset{˙}{+} (P \underset{˙}{\times} Y)$
176	16 23 175	3eqtrd	$⊢ φ \to P \underset{˙}{\times} (X \underset{˙}{+} Y) = (P \underset{˙}{\times} X) \underset{˙}{+} (P \underset{˙}{\times} Y)$

Metamath Proof Explorer

Theorem freshmansdream

Proof