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 ffvelrn ( ( 𝑌 : 𝑁𝐵𝑗𝑁 ) → ( 𝑌𝑗 ) ∈ 𝐵 )
42 41 ex ( 𝑌 : 𝑁𝐵 → ( 𝑗𝑁 → ( 𝑌𝑗 ) ∈ 𝐵 ) )
43 40 42 syl6bi ( 𝜑 → ( 𝑌 ∈ ( 𝐵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 ffvelrn ( ( 𝑌 : 𝑁𝐵𝑖𝑁 ) → ( 𝑌𝑖 ) ∈ 𝐵 )
80 79 2 eleqtrdi ( ( 𝑌 : 𝑁𝐵𝑖𝑁 ) → ( 𝑌𝑖 ) ∈ ( Base ‘ 𝑅 ) )
81 80 ex ( 𝑌 : 𝑁𝐵 → ( 𝑖𝑁 → ( 𝑌𝑖 ) ∈ ( Base ‘ 𝑅 ) ) )
82 40 81 syl6bi ( 𝜑 → ( 𝑌 ∈ ( 𝐵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 syl6bi ( 𝜑 → ( 𝑌 ∈ ( 𝐵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𝐴 ) · 𝑌 ) = 𝑌 )