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	ringmgp	$⊢ R \in Ring \to {mulGrp}_{R} \in Mnd$
42	39 41	syl	$⊢ φ \to {mulGrp}_{R} \in Mnd$
43	42	adantr	$⊢ (φ \land i \in (0 \dots P - 1 + 1)) \to {mulGrp}_{R} \in Mnd$
44		simpr	$⊢ (φ \land i \in (0 \dots P - 1 + 1)) \to i \in (0 \dots P - 1 + 1)$
45	20	adantr	$⊢ (φ \land i \in (0 \dots P - 1 + 1)) \to (0 \dots P - 1 + 1) = (0 \dots P)$
46	44 45	eleqtrd	$⊢ (φ \land i \in (0 \dots P - 1 + 1)) \to i \in (0 \dots P)$
47		fznn0sub	$⊢ i \in (0 \dots P) \to P - i \in ℕ_{0}$
48	46 47	syl	$⊢ (φ \land i \in (0 \dots P - 1 + 1)) \to P - i \in ℕ_{0}$
49	7	adantr	$⊢ (φ \land i \in (0 \dots P - 1 + 1)) \to X \in B$
50	14 1	mgpbas	$⊢ B = {Base}_{{mulGrp}_{R}}$
51	50 3	mulgnn0cl	$⊢ ({mulGrp}_{R} \in Mnd \land P - i \in ℕ_{0} \land X \in B) \to (P - i) \underset{˙}{\times} X \in B$
52	43 48 49 51	syl3anc	$⊢ (φ \land i \in (0 \dots P - 1 + 1)) \to (P - i) \underset{˙}{\times} X \in B$
53		elfznn0	$⊢ i \in (0 \dots P - 1 + 1) \to i \in ℕ_{0}$
54	53	adantl	$⊢ (φ \land i \in (0 \dots P - 1 + 1)) \to i \in ℕ_{0}$
55	8	adantr	$⊢ (φ \land i \in (0 \dots P - 1 + 1)) \to Y \in B$
56	50 3	mulgnn0cl	$⊢ ({mulGrp}_{R} \in Mnd \land i \in ℕ_{0} \land Y \in B) \to i \underset{˙}{\times} Y \in B$
57	43 54 55 56	syl3anc	$⊢ (φ \land i \in (0 \dots P - 1 + 1)) \to i \underset{˙}{\times} Y \in B$
58	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$
59	40 52 57 58	syl3anc	$⊢ (φ \land i \in (0 \dots P - 1 + 1)) \to ((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y) \in B$
60	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$
61	31 38 59 60	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$
62	1 2 25 28 61	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))))$
63	30	adantr	$⊢ (φ \land i \in (0 \dots P - 1)) \to R \in Grp$
64		elfzelz	$⊢ i \in (0 \dots P - 1) \to i \in ℤ$
65	11 64 36	syl2an	$⊢ (φ \land i \in (0 \dots P - 1)) \to (\binom{P}{i}) \in ℕ_{0}$
66	65	nn0zd	$⊢ (φ \land i \in (0 \dots P - 1)) \to (\binom{P}{i}) \in ℤ$
67	39	adantr	$⊢ (φ \land i \in (0 \dots P - 1)) \to R \in Ring$
68	67 41	syl	$⊢ (φ \land i \in (0 \dots P - 1)) \to {mulGrp}_{R} \in Mnd$
69		fzssp1	$⊢ (0 \dots P - 1) \subseteq (0 \dots P - 1 + 1)$
70	69 20	sseqtrid	$⊢ φ \to (0 \dots P - 1) \subseteq (0 \dots P)$
71	70	sselda	$⊢ (φ \land i \in (0 \dots P - 1)) \to i \in (0 \dots P)$
72	71 47	syl	$⊢ (φ \land i \in (0 \dots P - 1)) \to P - i \in ℕ_{0}$
73	7	adantr	$⊢ (φ \land i \in (0 \dots P - 1)) \to X \in B$
74	68 72 73 51	syl3anc	$⊢ (φ \land i \in (0 \dots P - 1)) \to (P - i) \underset{˙}{\times} X \in B$
75		elfznn0	$⊢ i \in (0 \dots P - 1) \to i \in ℕ_{0}$
76	75	adantl	$⊢ (φ \land i \in (0 \dots P - 1)) \to i \in ℕ_{0}$
77	8	adantr	$⊢ (φ \land i \in (0 \dots P - 1)) \to Y \in B$
78	68 76 77 56	syl3anc	$⊢ (φ \land i \in (0 \dots P - 1)) \to i \underset{˙}{\times} Y \in B$
79	67 74 78 58	syl3anc	$⊢ (φ \land i \in (0 \dots P - 1)) \to ((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y) \in B$
80	63 66 79 60	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$
81	1 2 25 28 80	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))))$
82	39	adantr	$⊢ (φ \land i \in (1 \dots P - 1)) \to R \in Ring$
83		prmdvdsbc	$⊢ (P \in ℙ \land i \in (1 \dots P - 1)) \to P ∥ (\binom{P}{i})$
84	6 83	sylan	$⊢ (φ \land i \in (1 \dots P - 1)) \to P ∥ (\binom{P}{i})$
85	82 41	syl	$⊢ (φ \land i \in (1 \dots P - 1)) \to {mulGrp}_{R} \in Mnd$
86	11	nn0zd	$⊢ φ \to P \in ℤ$
87		1nn0	$⊢ 1 \in ℕ_{0}$
88		eluzmn	$⊢ (P \in ℤ \land 1 \in ℕ_{0}) \to P \in ℤ_{\geq (P - 1)}$
89	86 87 88	sylancl	$⊢ φ \to P \in ℤ_{\geq (P - 1)}$
90		fzss2	$⊢ P \in ℤ_{\geq (P - 1)} \to (1 \dots P - 1) \subseteq (1 \dots P)$
91	89 90	syl	$⊢ φ \to (1 \dots P - 1) \subseteq (1 \dots P)$
92	91	sselda	$⊢ (φ \land i \in (1 \dots P - 1)) \to i \in (1 \dots P)$
93		fznn0sub	$⊢ i \in (1 \dots P) \to P - i \in ℕ_{0}$
94	92 93	syl	$⊢ (φ \land i \in (1 \dots P - 1)) \to P - i \in ℕ_{0}$
95	7	adantr	$⊢ (φ \land i \in (1 \dots P - 1)) \to X \in B$
96	85 94 95 51	syl3anc	$⊢ (φ \land i \in (1 \dots P - 1)) \to (P - i) \underset{˙}{\times} X \in B$
97		elfznn	$⊢ i \in (1 \dots P - 1) \to i \in ℕ$
98	97	nnnn0d	$⊢ i \in (1 \dots P - 1) \to i \in ℕ_{0}$
99	98	adantl	$⊢ (φ \land i \in (1 \dots P - 1)) \to i \in ℕ_{0}$
100	8	adantr	$⊢ (φ \land i \in (1 \dots P - 1)) \to Y \in B$
101	85 99 100 56	syl3anc	$⊢ (φ \land i \in (1 \dots P - 1)) \to i \underset{˙}{\times} Y \in B$
102	82 96 101 58	syl3anc	$⊢ (φ \land i \in (1 \dots P - 1)) \to ((P - i) \underset{˙}{\times} X) \cdot_{R} (i \underset{˙}{\times} Y) \in B$
103		eqid	$⊢ 0_{R} = 0_{R}$
104	4 1 13 103	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}$
105	82 84 102 104	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}$
106	105	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})$
107	106	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}$
108		ringmnd	$⊢ R \in Ring \to R \in Mnd$
109	39 108	syl	$⊢ φ \to R \in Mnd$
110		ovex	$⊢ (1 \dots P - 1) \in V$
111	103	gsumz	$⊢ (R \in Mnd \land (1 \dots P - 1) \in V) \to {\sum_{R}}_{i = 1}^{P - 1} 0_{R} = 0_{R}$
112	109 110 111	sylancl	$⊢ φ \to {\sum_{R}}_{i = 1}^{P - 1} 0_{R} = 0_{R}$
113	107 112	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}$
114		0nn0	$⊢ 0 \in ℕ_{0}$
115	114	a1i	$⊢ φ \to 0 \in ℕ_{0}$
116	50 3	mulgnn0cl	$⊢ ({mulGrp}_{R} \in Mnd \land P \in ℕ_{0} \land X \in B) \to P \underset{˙}{\times} X \in B$
117	42 11 7 116	syl3anc	$⊢ φ \to P \underset{˙}{\times} X \in B$
118		simpr	$⊢ (φ \land i = 0) \to i = 0$
119	118	oveq2d	$⊢ (φ \land i = 0) \to (\binom{P}{i}) = (\binom{P}{0})$
120	118	oveq2d	$⊢ (φ \land i = 0) \to P - i = P - 0$
121	120	oveq1d	$⊢ (φ \land i = 0) \to (P - i) \underset{˙}{\times} X = (P - 0) \underset{˙}{\times} X$
122	118	oveq1d	$⊢ (φ \land i = 0) \to i \underset{˙}{\times} Y = 0 \underset{˙}{\times} Y$
123	121 122	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)$
124	119 123	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))$
125		bcn0	$⊢ P \in ℕ_{0} \to (\binom{P}{0}) = 1$
126	11 125	syl	$⊢ φ \to (\binom{P}{0}) = 1$
127	17	subid1d	$⊢ φ \to P - 0 = P$
128	127	oveq1d	$⊢ φ \to (P - 0) \underset{˙}{\times} X = P \underset{˙}{\times} X$
129		eqid	$⊢ 1_{R} = 1_{R}$
130	14 129	ringidval	$⊢ 1_{R} = 0_{{mulGrp}_{R}}$
131	50 130 3	mulg0	$⊢ Y \in B \to 0 \underset{˙}{\times} Y = 1_{R}$
132	8 131	syl	$⊢ φ \to 0 \underset{˙}{\times} Y = 1_{R}$
133	128 132	oveq12d	$⊢ φ \to ((P - 0) \underset{˙}{\times} X) \cdot_{R} (0 \underset{˙}{\times} Y) = (P \underset{˙}{\times} X) \cdot_{R} 1_{R}$
134	1 12 129	ringridm	$⊢ (R \in Ring \land P \underset{˙}{\times} X \in B) \to (P \underset{˙}{\times} X) \cdot_{R} 1_{R} = P \underset{˙}{\times} X$
135	39 117 134	syl2anc	$⊢ φ \to (P \underset{˙}{\times} X) \cdot_{R} 1_{R} = P \underset{˙}{\times} X$
136	133 135	eqtrd	$⊢ φ \to ((P - 0) \underset{˙}{\times} X) \cdot_{R} (0 \underset{˙}{\times} Y) = P \underset{˙}{\times} X$
137	126 136	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)$
138	1 13	mulg1	$⊢ P \underset{˙}{\times} X \in B \to 1 \cdot_{R} (P \underset{˙}{\times} X) = P \underset{˙}{\times} X$
139	117 138	syl	$⊢ φ \to 1 \cdot_{R} (P \underset{˙}{\times} X) = P \underset{˙}{\times} X$
140	137 139	eqtrd	$⊢ φ \to (\binom{P}{0}) \cdot_{R} (((P - 0) \underset{˙}{\times} X) \cdot_{R} (0 \underset{˙}{\times} Y)) = P \underset{˙}{\times} X$
141	140	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$
142	124 141	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$
143	1 109 115 117 142	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$
144	113 143	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)$
145	1 2 103	grplid	$⊢ (R \in Grp \land P \underset{˙}{\times} X \in B) \to 0_{R} \underset{˙}{+} (P \underset{˙}{\times} X) = P \underset{˙}{\times} X$
146	30 117 145	syl2anc	$⊢ φ \to 0_{R} \underset{˙}{+} (P \underset{˙}{\times} X) = P \underset{˙}{\times} X$
147	81 144 146	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$
148	19 11	eqeltrd	$⊢ φ \to P - 1 + 1 \in ℕ_{0}$
149	50 3	mulgnn0cl	$⊢ ({mulGrp}_{R} \in Mnd \land P \in ℕ_{0} \land Y \in B) \to P \underset{˙}{\times} Y \in B$
150	42 11 8 149	syl3anc	$⊢ φ \to P \underset{˙}{\times} Y \in B$
151		simpr	$⊢ (φ \land i = P - 1 + 1) \to i = P - 1 + 1$
152	19	adantr	$⊢ (φ \land i = P - 1 + 1) \to P - 1 + 1 = P$
153	151 152	eqtrd	$⊢ (φ \land i = P - 1 + 1) \to i = P$
154	153	oveq2d	$⊢ (φ \land i = P - 1 + 1) \to (\binom{P}{i}) = (\binom{P}{P})$
155	153	oveq2d	$⊢ (φ \land i = P - 1 + 1) \to P - i = P - P$
156	155	oveq1d	$⊢ (φ \land i = P - 1 + 1) \to (P - i) \underset{˙}{\times} X = (P - P) \underset{˙}{\times} X$
157	153	oveq1d	$⊢ (φ \land i = P - 1 + 1) \to i \underset{˙}{\times} Y = P \underset{˙}{\times} Y$
158	156 157	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)$
159	154 158	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))$
160		bcnn	$⊢ P \in ℕ_{0} \to (\binom{P}{P}) = 1$
161	11 160	syl	$⊢ φ \to (\binom{P}{P}) = 1$
162	17	subidd	$⊢ φ \to P - P = 0$
163	162	oveq1d	$⊢ φ \to (P - P) \underset{˙}{\times} X = 0 \underset{˙}{\times} X$
164	50 130 3	mulg0	$⊢ X \in B \to 0 \underset{˙}{\times} X = 1_{R}$
165	7 164	syl	$⊢ φ \to 0 \underset{˙}{\times} X = 1_{R}$
166	163 165	eqtrd	$⊢ φ \to (P - P) \underset{˙}{\times} X = 1_{R}$
167	166	oveq1d	$⊢ φ \to ((P - P) \underset{˙}{\times} X) \cdot_{R} (P \underset{˙}{\times} Y) = 1_{R} \cdot_{R} (P \underset{˙}{\times} Y)$
168	1 12 129	ringlidm	$⊢ (R \in Ring \land P \underset{˙}{\times} Y \in B) \to 1_{R} \cdot_{R} (P \underset{˙}{\times} Y) = P \underset{˙}{\times} Y$
169	39 150 168	syl2anc	$⊢ φ \to 1_{R} \cdot_{R} (P \underset{˙}{\times} Y) = P \underset{˙}{\times} Y$
170	167 169	eqtrd	$⊢ φ \to ((P - P) \underset{˙}{\times} X) \cdot_{R} (P \underset{˙}{\times} Y) = P \underset{˙}{\times} Y$
171	161 170	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)$
172	1 13	mulg1	$⊢ P \underset{˙}{\times} Y \in B \to 1 \cdot_{R} (P \underset{˙}{\times} Y) = P \underset{˙}{\times} Y$
173	150 172	syl	$⊢ φ \to 1 \cdot_{R} (P \underset{˙}{\times} Y) = P \underset{˙}{\times} Y$
174	171 173	eqtrd	$⊢ φ \to (\binom{P}{P}) \cdot_{R} (((P - P) \underset{˙}{\times} X) \cdot_{R} (P \underset{˙}{\times} Y)) = P \underset{˙}{\times} Y$
175	174	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$
176	159 175	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$
177	1 109 148 150 176	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$
178	147 177	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)$
179	62 178	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)$
180	16 23 179	3eqtrd	$⊢ φ \to P \underset{˙}{\times} (X \underset{˙}{+} Y) = (P \underset{˙}{\times} X) \underset{˙}{+} (P \underset{˙}{\times} Y)$

Metamath Proof Explorer

Theorem freshmansdream

Proof