Metamath Proof Explorer


Theorem mamurid

Description: The identity matrix (as operation in maps-to notation) is a right identity (for any matrix with the same number of columns). (Contributed by Stefan O'Rear, 3-Sep-2015) (Proof shortened by AV, 22-Jul-2019)

Ref Expression
Hypotheses mamumat1cl.b 𝐵 = ( Base ‘ 𝑅 )
mamumat1cl.r ( 𝜑𝑅 ∈ Ring )
mamumat1cl.o 1 = ( 1r𝑅 )
mamumat1cl.z 0 = ( 0g𝑅 )
mamumat1cl.i 𝐼 = ( 𝑖𝑀 , 𝑗𝑀 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) )
mamumat1cl.m ( 𝜑𝑀 ∈ Fin )
mamulid.n ( 𝜑𝑁 ∈ Fin )
mamurid.f 𝐹 = ( 𝑅 maMul ⟨ 𝑁 , 𝑀 , 𝑀 ⟩ )
mamurid.x ( 𝜑𝑋 ∈ ( 𝐵m ( 𝑁 × 𝑀 ) ) )
Assertion mamurid ( 𝜑 → ( 𝑋 𝐹 𝐼 ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 mamumat1cl.b 𝐵 = ( Base ‘ 𝑅 )
2 mamumat1cl.r ( 𝜑𝑅 ∈ Ring )
3 mamumat1cl.o 1 = ( 1r𝑅 )
4 mamumat1cl.z 0 = ( 0g𝑅 )
5 mamumat1cl.i 𝐼 = ( 𝑖𝑀 , 𝑗𝑀 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) )
6 mamumat1cl.m ( 𝜑𝑀 ∈ Fin )
7 mamulid.n ( 𝜑𝑁 ∈ Fin )
8 mamurid.f 𝐹 = ( 𝑅 maMul ⟨ 𝑁 , 𝑀 , 𝑀 ⟩ )
9 mamurid.x ( 𝜑𝑋 ∈ ( 𝐵m ( 𝑁 × 𝑀 ) ) )
10 eqid ( .r𝑅 ) = ( .r𝑅 )
11 2 adantr ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) → 𝑅 ∈ Ring )
12 7 adantr ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) → 𝑁 ∈ Fin )
13 6 adantr ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) → 𝑀 ∈ Fin )
14 9 adantr ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) → 𝑋 ∈ ( 𝐵m ( 𝑁 × 𝑀 ) ) )
15 1 2 3 4 5 6 mamumat1cl ( 𝜑𝐼 ∈ ( 𝐵m ( 𝑀 × 𝑀 ) ) )
16 15 adantr ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) → 𝐼 ∈ ( 𝐵m ( 𝑀 × 𝑀 ) ) )
17 simprl ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) → 𝑙𝑁 )
18 simprr ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) → 𝑚𝑀 )
19 8 1 10 11 12 13 13 14 16 17 18 mamufv ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) → ( 𝑙 ( 𝑋 𝐹 𝐼 ) 𝑚 ) = ( 𝑅 Σg ( 𝑘𝑀 ↦ ( ( 𝑙 𝑋 𝑘 ) ( .r𝑅 ) ( 𝑘 𝐼 𝑚 ) ) ) ) )
20 ringmnd ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
21 11 20 syl ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) → 𝑅 ∈ Mnd )
22 2 ad2antrr ( ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) ∧ 𝑘𝑀 ) → 𝑅 ∈ Ring )
23 elmapi ( 𝑋 ∈ ( 𝐵m ( 𝑁 × 𝑀 ) ) → 𝑋 : ( 𝑁 × 𝑀 ) ⟶ 𝐵 )
24 9 23 syl ( 𝜑𝑋 : ( 𝑁 × 𝑀 ) ⟶ 𝐵 )
25 24 ad2antrr ( ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) ∧ 𝑘𝑀 ) → 𝑋 : ( 𝑁 × 𝑀 ) ⟶ 𝐵 )
26 simplrl ( ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) ∧ 𝑘𝑀 ) → 𝑙𝑁 )
27 simpr ( ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) ∧ 𝑘𝑀 ) → 𝑘𝑀 )
28 25 26 27 fovrnd ( ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) ∧ 𝑘𝑀 ) → ( 𝑙 𝑋 𝑘 ) ∈ 𝐵 )
29 elmapi ( 𝐼 ∈ ( 𝐵m ( 𝑀 × 𝑀 ) ) → 𝐼 : ( 𝑀 × 𝑀 ) ⟶ 𝐵 )
30 15 29 syl ( 𝜑𝐼 : ( 𝑀 × 𝑀 ) ⟶ 𝐵 )
31 30 ad2antrr ( ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) ∧ 𝑘𝑀 ) → 𝐼 : ( 𝑀 × 𝑀 ) ⟶ 𝐵 )
32 simplrr ( ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) ∧ 𝑘𝑀 ) → 𝑚𝑀 )
33 31 27 32 fovrnd ( ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) ∧ 𝑘𝑀 ) → ( 𝑘 𝐼 𝑚 ) ∈ 𝐵 )
34 1 10 ringcl ( ( 𝑅 ∈ Ring ∧ ( 𝑙 𝑋 𝑘 ) ∈ 𝐵 ∧ ( 𝑘 𝐼 𝑚 ) ∈ 𝐵 ) → ( ( 𝑙 𝑋 𝑘 ) ( .r𝑅 ) ( 𝑘 𝐼 𝑚 ) ) ∈ 𝐵 )
35 22 28 33 34 syl3anc ( ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) ∧ 𝑘𝑀 ) → ( ( 𝑙 𝑋 𝑘 ) ( .r𝑅 ) ( 𝑘 𝐼 𝑚 ) ) ∈ 𝐵 )
36 35 fmpttd ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) → ( 𝑘𝑀 ↦ ( ( 𝑙 𝑋 𝑘 ) ( .r𝑅 ) ( 𝑘 𝐼 𝑚 ) ) ) : 𝑀𝐵 )
37 simp2 ( ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) ∧ 𝑘𝑀𝑘𝑚 ) → 𝑘𝑀 )
38 32 3adant3 ( ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) ∧ 𝑘𝑀𝑘𝑚 ) → 𝑚𝑀 )
39 1 2 3 4 5 6 mat1comp ( ( 𝑘𝑀𝑚𝑀 ) → ( 𝑘 𝐼 𝑚 ) = if ( 𝑘 = 𝑚 , 1 , 0 ) )
40 37 38 39 syl2anc ( ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) ∧ 𝑘𝑀𝑘𝑚 ) → ( 𝑘 𝐼 𝑚 ) = if ( 𝑘 = 𝑚 , 1 , 0 ) )
41 ifnefalse ( 𝑘𝑚 → if ( 𝑘 = 𝑚 , 1 , 0 ) = 0 )
42 41 3ad2ant3 ( ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) ∧ 𝑘𝑀𝑘𝑚 ) → if ( 𝑘 = 𝑚 , 1 , 0 ) = 0 )
43 40 42 eqtrd ( ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) ∧ 𝑘𝑀𝑘𝑚 ) → ( 𝑘 𝐼 𝑚 ) = 0 )
44 43 oveq2d ( ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) ∧ 𝑘𝑀𝑘𝑚 ) → ( ( 𝑙 𝑋 𝑘 ) ( .r𝑅 ) ( 𝑘 𝐼 𝑚 ) ) = ( ( 𝑙 𝑋 𝑘 ) ( .r𝑅 ) 0 ) )
45 1 10 4 ringrz ( ( 𝑅 ∈ Ring ∧ ( 𝑙 𝑋 𝑘 ) ∈ 𝐵 ) → ( ( 𝑙 𝑋 𝑘 ) ( .r𝑅 ) 0 ) = 0 )
46 22 28 45 syl2anc ( ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) ∧ 𝑘𝑀 ) → ( ( 𝑙 𝑋 𝑘 ) ( .r𝑅 ) 0 ) = 0 )
47 46 3adant3 ( ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) ∧ 𝑘𝑀𝑘𝑚 ) → ( ( 𝑙 𝑋 𝑘 ) ( .r𝑅 ) 0 ) = 0 )
48 44 47 eqtrd ( ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) ∧ 𝑘𝑀𝑘𝑚 ) → ( ( 𝑙 𝑋 𝑘 ) ( .r𝑅 ) ( 𝑘 𝐼 𝑚 ) ) = 0 )
49 48 13 suppsssn ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) → ( ( 𝑘𝑀 ↦ ( ( 𝑙 𝑋 𝑘 ) ( .r𝑅 ) ( 𝑘 𝐼 𝑚 ) ) ) supp 0 ) ⊆ { 𝑚 } )
50 1 4 21 13 18 36 49 gsumpt ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) → ( 𝑅 Σg ( 𝑘𝑀 ↦ ( ( 𝑙 𝑋 𝑘 ) ( .r𝑅 ) ( 𝑘 𝐼 𝑚 ) ) ) ) = ( ( 𝑘𝑀 ↦ ( ( 𝑙 𝑋 𝑘 ) ( .r𝑅 ) ( 𝑘 𝐼 𝑚 ) ) ) ‘ 𝑚 ) )
51 oveq2 ( 𝑘 = 𝑚 → ( 𝑙 𝑋 𝑘 ) = ( 𝑙 𝑋 𝑚 ) )
52 oveq1 ( 𝑘 = 𝑚 → ( 𝑘 𝐼 𝑚 ) = ( 𝑚 𝐼 𝑚 ) )
53 51 52 oveq12d ( 𝑘 = 𝑚 → ( ( 𝑙 𝑋 𝑘 ) ( .r𝑅 ) ( 𝑘 𝐼 𝑚 ) ) = ( ( 𝑙 𝑋 𝑚 ) ( .r𝑅 ) ( 𝑚 𝐼 𝑚 ) ) )
54 eqid ( 𝑘𝑀 ↦ ( ( 𝑙 𝑋 𝑘 ) ( .r𝑅 ) ( 𝑘 𝐼 𝑚 ) ) ) = ( 𝑘𝑀 ↦ ( ( 𝑙 𝑋 𝑘 ) ( .r𝑅 ) ( 𝑘 𝐼 𝑚 ) ) )
55 ovex ( ( 𝑙 𝑋 𝑚 ) ( .r𝑅 ) ( 𝑚 𝐼 𝑚 ) ) ∈ V
56 53 54 55 fvmpt ( 𝑚𝑀 → ( ( 𝑘𝑀 ↦ ( ( 𝑙 𝑋 𝑘 ) ( .r𝑅 ) ( 𝑘 𝐼 𝑚 ) ) ) ‘ 𝑚 ) = ( ( 𝑙 𝑋 𝑚 ) ( .r𝑅 ) ( 𝑚 𝐼 𝑚 ) ) )
57 56 ad2antll ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) → ( ( 𝑘𝑀 ↦ ( ( 𝑙 𝑋 𝑘 ) ( .r𝑅 ) ( 𝑘 𝐼 𝑚 ) ) ) ‘ 𝑚 ) = ( ( 𝑙 𝑋 𝑚 ) ( .r𝑅 ) ( 𝑚 𝐼 𝑚 ) ) )
58 equequ1 ( 𝑖 = 𝑚 → ( 𝑖 = 𝑗𝑚 = 𝑗 ) )
59 58 ifbid ( 𝑖 = 𝑚 → if ( 𝑖 = 𝑗 , 1 , 0 ) = if ( 𝑚 = 𝑗 , 1 , 0 ) )
60 equequ2 ( 𝑗 = 𝑚 → ( 𝑚 = 𝑗𝑚 = 𝑚 ) )
61 60 ifbid ( 𝑗 = 𝑚 → if ( 𝑚 = 𝑗 , 1 , 0 ) = if ( 𝑚 = 𝑚 , 1 , 0 ) )
62 eqid 𝑚 = 𝑚
63 62 iftruei if ( 𝑚 = 𝑚 , 1 , 0 ) = 1
64 61 63 eqtrdi ( 𝑗 = 𝑚 → if ( 𝑚 = 𝑗 , 1 , 0 ) = 1 )
65 3 fvexi 1 ∈ V
66 59 64 5 65 ovmpo ( ( 𝑚𝑀𝑚𝑀 ) → ( 𝑚 𝐼 𝑚 ) = 1 )
67 66 anidms ( 𝑚𝑀 → ( 𝑚 𝐼 𝑚 ) = 1 )
68 67 oveq2d ( 𝑚𝑀 → ( ( 𝑙 𝑋 𝑚 ) ( .r𝑅 ) ( 𝑚 𝐼 𝑚 ) ) = ( ( 𝑙 𝑋 𝑚 ) ( .r𝑅 ) 1 ) )
69 68 ad2antll ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) → ( ( 𝑙 𝑋 𝑚 ) ( .r𝑅 ) ( 𝑚 𝐼 𝑚 ) ) = ( ( 𝑙 𝑋 𝑚 ) ( .r𝑅 ) 1 ) )
70 24 fovrnda ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) → ( 𝑙 𝑋 𝑚 ) ∈ 𝐵 )
71 1 10 3 ringridm ( ( 𝑅 ∈ Ring ∧ ( 𝑙 𝑋 𝑚 ) ∈ 𝐵 ) → ( ( 𝑙 𝑋 𝑚 ) ( .r𝑅 ) 1 ) = ( 𝑙 𝑋 𝑚 ) )
72 11 70 71 syl2anc ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) → ( ( 𝑙 𝑋 𝑚 ) ( .r𝑅 ) 1 ) = ( 𝑙 𝑋 𝑚 ) )
73 57 69 72 3eqtrd ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) → ( ( 𝑘𝑀 ↦ ( ( 𝑙 𝑋 𝑘 ) ( .r𝑅 ) ( 𝑘 𝐼 𝑚 ) ) ) ‘ 𝑚 ) = ( 𝑙 𝑋 𝑚 ) )
74 19 50 73 3eqtrd ( ( 𝜑 ∧ ( 𝑙𝑁𝑚𝑀 ) ) → ( 𝑙 ( 𝑋 𝐹 𝐼 ) 𝑚 ) = ( 𝑙 𝑋 𝑚 ) )
75 74 ralrimivva ( 𝜑 → ∀ 𝑙𝑁𝑚𝑀 ( 𝑙 ( 𝑋 𝐹 𝐼 ) 𝑚 ) = ( 𝑙 𝑋 𝑚 ) )
76 1 2 8 7 6 6 9 15 mamucl ( 𝜑 → ( 𝑋 𝐹 𝐼 ) ∈ ( 𝐵m ( 𝑁 × 𝑀 ) ) )
77 elmapi ( ( 𝑋 𝐹 𝐼 ) ∈ ( 𝐵m ( 𝑁 × 𝑀 ) ) → ( 𝑋 𝐹 𝐼 ) : ( 𝑁 × 𝑀 ) ⟶ 𝐵 )
78 76 77 syl ( 𝜑 → ( 𝑋 𝐹 𝐼 ) : ( 𝑁 × 𝑀 ) ⟶ 𝐵 )
79 78 ffnd ( 𝜑 → ( 𝑋 𝐹 𝐼 ) Fn ( 𝑁 × 𝑀 ) )
80 24 ffnd ( 𝜑𝑋 Fn ( 𝑁 × 𝑀 ) )
81 eqfnov2 ( ( ( 𝑋 𝐹 𝐼 ) Fn ( 𝑁 × 𝑀 ) ∧ 𝑋 Fn ( 𝑁 × 𝑀 ) ) → ( ( 𝑋 𝐹 𝐼 ) = 𝑋 ↔ ∀ 𝑙𝑁𝑚𝑀 ( 𝑙 ( 𝑋 𝐹 𝐼 ) 𝑚 ) = ( 𝑙 𝑋 𝑚 ) ) )
82 79 80 81 syl2anc ( 𝜑 → ( ( 𝑋 𝐹 𝐼 ) = 𝑋 ↔ ∀ 𝑙𝑁𝑚𝑀 ( 𝑙 ( 𝑋 𝐹 𝐼 ) 𝑚 ) = ( 𝑙 𝑋 𝑚 ) ) )
83 75 82 mpbird ( 𝜑 → ( 𝑋 𝐹 𝐼 ) = 𝑋 )