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

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 fovcdmd ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀 ) ) ∧ 𝑘 ∈ 𝑀 ) → ( 𝑙 𝑋 𝑘 ) ∈ 𝐵 )
29 elmapi ⊢ ( 𝐼 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑀 ) ) → 𝐼 : ( 𝑀 × 𝑀 ) ⟶ 𝐵 )
30 15 29 syl ⊢ ( 𝜑 → 𝐼 : ( 𝑀 × 𝑀 ) ⟶ 𝐵 )
31 30 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀 ) ) ∧ 𝑘 ∈ 𝑀 ) → 𝐼 : ( 𝑀 × 𝑀 ) ⟶ 𝐵 )
32 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀 ) ) ∧ 𝑘 ∈ 𝑀 ) → 𝑚 ∈ 𝑀 )
33 31 27 32 fovcdmd ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀 ) ) ∧ 𝑘 ∈ 𝑀 ) → ( 𝑘 𝐼 𝑚 ) ∈ 𝐵 )
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 fovcdmda ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑁 ∧ 𝑚 ∈ 𝑀 ) ) → ( 𝑙 𝑋 𝑚 ) ∈ 𝐵 )
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 ⊢ ( 𝜑 → ( 𝑋 𝐹 𝐼 ) = 𝑋 )