This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐴 ) · 𝑌 ) = 𝑌 )