Theorem 1mavmul

Description: Multiplication of the identity NxN matrix with an N-dimensional vector results in the vector itself. (Contributed by AV, 9-Feb-2019) (Revised by AV, 23-Feb-2019)

	Ref	Expression
Hypotheses	1mavmul.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	1mavmul.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	1mavmul.t	⊢ · = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
	1mavmul.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	1mavmul.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
	1mavmul.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ↑m 𝑁 ) )
Assertion	1mavmul	⊢ ( 𝜑 → ( ( 1r ‘ 𝐴 ) · 𝑌 ) = 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		1mavmul.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		1mavmul.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		1mavmul.t	⊢ · = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
4		1mavmul.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
5		1mavmul.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
6		1mavmul.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ↑m 𝑁 ) )
7		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
8		eqid	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
9	1	fveq2i	⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ ( 𝑁 Mat 𝑅 ) )
10	1 8 9	mat1bas	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → ( 1r ‘ 𝐴 ) ∈ ( Base ‘ 𝐴 ) )
11	4 5 10	syl2anc	⊢ ( 𝜑 → ( 1r ‘ 𝐴 ) ∈ ( Base ‘ 𝐴 ) )
12	1 3 2 7 4 5 11 6	mavmulval	⊢ ( 𝜑 → ( ( 1r ‘ 𝐴 ) · 𝑌 ) = ( 𝑖 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 1r ‘ 𝐴 ) 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) ) )
13		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
14		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
15	1 13 14	mat1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐴 ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑦 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
16	5 4 15	syl2anc	⊢ ( 𝜑 → ( 1r ‘ 𝐴 ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑦 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
17	16	oveqdr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ( 𝑖 ( 1r ‘ 𝐴 ) 𝑗 ) = ( 𝑖 ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑦 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) 𝑗 ) )
18	17	oveq1d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ( ( 𝑖 ( 1r ‘ 𝐴 ) 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) = ( ( 𝑖 ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑦 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) )
19	18	mpteq2dv	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 1r ‘ 𝐴 ) 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) = ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑦 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) )
20	19	oveq2d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 1r ‘ 𝐴 ) 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) = ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑦 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) )
21		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑦 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑦 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
22		eqeq12	⊢ ( ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) → ( 𝑥 = 𝑦 ↔ 𝑖 = 𝑗 ) )
23	22	ifbid	⊢ ( ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) → if ( 𝑥 = 𝑦 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
24	23	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) ) → if ( 𝑥 = 𝑦 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
25		simpr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
26	25	adantr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
27		simpr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
28		fvexd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 1r ‘ 𝑅 ) ∈ V )
29		fvexd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 0g ‘ 𝑅 ) ∈ V )
30	28 29	ifcld	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ V )
31	21 24 26 27 30	ovmpod	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑦 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) 𝑗 ) = if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
32	31	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑖 ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑦 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) = ( if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) )
33		iftrue	⊢ ( 𝑖 = 𝑗 → if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
34	33	adantr	⊢ ( ( 𝑖 = 𝑗 ∧ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ) → if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
35	34	oveq1d	⊢ ( ( 𝑖 = 𝑗 ∧ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ) → ( if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) = ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) )
36	4	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → 𝑅 ∈ Ring )
37	36	adantr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑅 ∈ Ring )
38	2	fvexi	⊢ 𝐵 ∈ V
39	38	a1i	⊢ ( 𝜑 → 𝐵 ∈ V )
40	39 5	elmapd	⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝐵 ↑m 𝑁 ) ↔ 𝑌 : 𝑁 ⟶ 𝐵 ) )
41		ffvelcdm	⊢ ( ( 𝑌 : 𝑁 ⟶ 𝐵 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑌 ‘ 𝑗 ) ∈ 𝐵 )
42	41	ex	⊢ ( 𝑌 : 𝑁 ⟶ 𝐵 → ( 𝑗 ∈ 𝑁 → ( 𝑌 ‘ 𝑗 ) ∈ 𝐵 ) )
43	40 42	biimtrdi	⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝐵 ↑m 𝑁 ) → ( 𝑗 ∈ 𝑁 → ( 𝑌 ‘ 𝑗 ) ∈ 𝐵 ) ) )
44	6 43	mpd	⊢ ( 𝜑 → ( 𝑗 ∈ 𝑁 → ( 𝑌 ‘ 𝑗 ) ∈ 𝐵 ) )
45	44	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ( 𝑗 ∈ 𝑁 → ( 𝑌 ‘ 𝑗 ) ∈ 𝐵 ) )
46	45	imp	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑌 ‘ 𝑗 ) ∈ 𝐵 )
47	2 7 13	ringlidm	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑌 ‘ 𝑗 ) ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) = ( 𝑌 ‘ 𝑗 ) )
48	37 46 47	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) = ( 𝑌 ‘ 𝑗 ) )
49	48	adantl	⊢ ( ( 𝑖 = 𝑗 ∧ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) = ( 𝑌 ‘ 𝑗 ) )
50		fveq2	⊢ ( 𝑗 = 𝑖 → ( 𝑌 ‘ 𝑗 ) = ( 𝑌 ‘ 𝑖 ) )
51	50	equcoms	⊢ ( 𝑖 = 𝑗 → ( 𝑌 ‘ 𝑗 ) = ( 𝑌 ‘ 𝑖 ) )
52	51	adantr	⊢ ( ( 𝑖 = 𝑗 ∧ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑌 ‘ 𝑗 ) = ( 𝑌 ‘ 𝑖 ) )
53	35 49 52	3eqtrd	⊢ ( ( 𝑖 = 𝑗 ∧ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ) → ( if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) = ( 𝑌 ‘ 𝑖 ) )
54		iftrue	⊢ ( 𝑗 = 𝑖 → if ( 𝑗 = 𝑖 , ( 𝑌 ‘ 𝑖 ) , ( 0g ‘ 𝑅 ) ) = ( 𝑌 ‘ 𝑖 ) )
55	54	equcoms	⊢ ( 𝑖 = 𝑗 → if ( 𝑗 = 𝑖 , ( 𝑌 ‘ 𝑖 ) , ( 0g ‘ 𝑅 ) ) = ( 𝑌 ‘ 𝑖 ) )
56	55	adantr	⊢ ( ( 𝑖 = 𝑗 ∧ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ) → if ( 𝑗 = 𝑖 , ( 𝑌 ‘ 𝑖 ) , ( 0g ‘ 𝑅 ) ) = ( 𝑌 ‘ 𝑖 ) )
57	53 56	eqtr4d	⊢ ( ( 𝑖 = 𝑗 ∧ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ) → ( if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) = if ( 𝑗 = 𝑖 , ( 𝑌 ‘ 𝑖 ) , ( 0g ‘ 𝑅 ) ) )
58		iffalse	⊢ ( ¬ 𝑖 = 𝑗 → if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
59	58	oveq1d	⊢ ( ¬ 𝑖 = 𝑗 → ( if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) = ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) )
60	59	adantr	⊢ ( ( ¬ 𝑖 = 𝑗 ∧ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ) → ( if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) = ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) )
61	2 7 14	ringlz	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑌 ‘ 𝑗 ) ∈ 𝐵 ) → ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) = ( 0g ‘ 𝑅 ) )
62	37 46 61	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) = ( 0g ‘ 𝑅 ) )
63	62	adantl	⊢ ( ( ¬ 𝑖 = 𝑗 ∧ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ) → ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) = ( 0g ‘ 𝑅 ) )
64		eqcom	⊢ ( 𝑖 = 𝑗 ↔ 𝑗 = 𝑖 )
65		iffalse	⊢ ( ¬ 𝑗 = 𝑖 → if ( 𝑗 = 𝑖 , ( 𝑌 ‘ 𝑖 ) , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
66	64 65	sylnbi	⊢ ( ¬ 𝑖 = 𝑗 → if ( 𝑗 = 𝑖 , ( 𝑌 ‘ 𝑖 ) , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
67	66	eqcomd	⊢ ( ¬ 𝑖 = 𝑗 → ( 0g ‘ 𝑅 ) = if ( 𝑗 = 𝑖 , ( 𝑌 ‘ 𝑖 ) , ( 0g ‘ 𝑅 ) ) )
68	67	adantr	⊢ ( ( ¬ 𝑖 = 𝑗 ∧ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ) → ( 0g ‘ 𝑅 ) = if ( 𝑗 = 𝑖 , ( 𝑌 ‘ 𝑖 ) , ( 0g ‘ 𝑅 ) ) )
69	60 63 68	3eqtrd	⊢ ( ( ¬ 𝑖 = 𝑗 ∧ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ) → ( if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) = if ( 𝑗 = 𝑖 , ( 𝑌 ‘ 𝑖 ) , ( 0g ‘ 𝑅 ) ) )
70	57 69	pm2.61ian	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) = if ( 𝑗 = 𝑖 , ( 𝑌 ‘ 𝑖 ) , ( 0g ‘ 𝑅 ) ) )
71	32 70	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑖 ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑦 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) = if ( 𝑗 = 𝑖 , ( 𝑌 ‘ 𝑖 ) , ( 0g ‘ 𝑅 ) ) )
72	71	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑦 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) = ( 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝑖 , ( 𝑌 ‘ 𝑖 ) , ( 0g ‘ 𝑅 ) ) ) )
73	72	oveq2d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑦 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) = ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝑖 , ( 𝑌 ‘ 𝑖 ) , ( 0g ‘ 𝑅 ) ) ) ) )
74		ringmnd	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
75	4 74	syl	⊢ ( 𝜑 → 𝑅 ∈ Mnd )
76	75	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → 𝑅 ∈ Mnd )
77	5	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → 𝑁 ∈ Fin )
78		eqid	⊢ ( 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝑖 , ( 𝑌 ‘ 𝑖 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝑖 , ( 𝑌 ‘ 𝑖 ) , ( 0g ‘ 𝑅 ) ) )
79		ffvelcdm	⊢ ( ( 𝑌 : 𝑁 ⟶ 𝐵 ∧ 𝑖 ∈ 𝑁 ) → ( 𝑌 ‘ 𝑖 ) ∈ 𝐵 )
80	79 2	eleqtrdi	⊢ ( ( 𝑌 : 𝑁 ⟶ 𝐵 ∧ 𝑖 ∈ 𝑁 ) → ( 𝑌 ‘ 𝑖 ) ∈ ( Base ‘ 𝑅 ) )
81	80	ex	⊢ ( 𝑌 : 𝑁 ⟶ 𝐵 → ( 𝑖 ∈ 𝑁 → ( 𝑌 ‘ 𝑖 ) ∈ ( Base ‘ 𝑅 ) ) )
82	40 81	biimtrdi	⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝐵 ↑m 𝑁 ) → ( 𝑖 ∈ 𝑁 → ( 𝑌 ‘ 𝑖 ) ∈ ( Base ‘ 𝑅 ) ) ) )
83	6 82	mpd	⊢ ( 𝜑 → ( 𝑖 ∈ 𝑁 → ( 𝑌 ‘ 𝑖 ) ∈ ( Base ‘ 𝑅 ) ) )
84	83	imp	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ( 𝑌 ‘ 𝑖 ) ∈ ( Base ‘ 𝑅 ) )
85	14 76 77 25 78 84	gsummptif1n0	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝑖 , ( 𝑌 ‘ 𝑖 ) , ( 0g ‘ 𝑅 ) ) ) ) = ( 𝑌 ‘ 𝑖 ) )
86	20 73 85	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 1r ‘ 𝐴 ) 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) = ( 𝑌 ‘ 𝑖 ) )
87	86	mpteq2dva	⊢ ( 𝜑 → ( 𝑖 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 ( 1r ‘ 𝐴 ) 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑗 ) ) ) ) ) = ( 𝑖 ∈ 𝑁 ↦ ( 𝑌 ‘ 𝑖 ) ) )
88		ffn	⊢ ( 𝑌 : 𝑁 ⟶ 𝐵 → 𝑌 Fn 𝑁 )
89	40 88	biimtrdi	⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝐵 ↑m 𝑁 ) → 𝑌 Fn 𝑁 ) )
90	6 89	mpd	⊢ ( 𝜑 → 𝑌 Fn 𝑁 )
91		eqcom	⊢ ( ( 𝑖 ∈ 𝑁 ↦ ( 𝑌 ‘ 𝑖 ) ) = 𝑌 ↔ 𝑌 = ( 𝑖 ∈ 𝑁 ↦ ( 𝑌 ‘ 𝑖 ) ) )
92		dffn5	⊢ ( 𝑌 Fn 𝑁 ↔ 𝑌 = ( 𝑖 ∈ 𝑁 ↦ ( 𝑌 ‘ 𝑖 ) ) )
93	91 92	bitr4i	⊢ ( ( 𝑖 ∈ 𝑁 ↦ ( 𝑌 ‘ 𝑖 ) ) = 𝑌 ↔ 𝑌 Fn 𝑁 )
94	90 93	sylibr	⊢ ( 𝜑 → ( 𝑖 ∈ 𝑁 ↦ ( 𝑌 ‘ 𝑖 ) ) = 𝑌 )
95	12 87 94	3eqtrd	⊢ ( 𝜑 → ( ( 1r ‘ 𝐴 ) · 𝑌 ) = 𝑌 )