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

Metamath Proof Explorer

Theorem mamulid

Description: The identity matrix (as operation in maps-to notation) is a left identity (for any matrix with the same number of rows). (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 )
mamulid.f ⊢ 𝐹 = ( 𝑅 maMul ⟨ 𝑀 , 𝑀 , 𝑁 ⟩ )
mamulid.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) )
Assertion mamulid ( 𝜑 → ( 𝐼 𝐹 𝑋 ) = 𝑋 )

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 mamulid.f ⊢ 𝐹 = ( 𝑅 maMul ⟨ 𝑀 , 𝑀 , 𝑁 ⟩ )
9 mamulid.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) )
10 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
11 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑀 ∧ 𝑘 ∈ 𝑁 ) ) → 𝑅 ∈ Ring )
12 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑀 ∧ 𝑘 ∈ 𝑁 ) ) → 𝑀 ∈ Fin )
13 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑀 ∧ 𝑘 ∈ 𝑁 ) ) → 𝑁 ∈ Fin )
14 1 2 3 4 5 6 mamumat1cl ⊢ ( 𝜑 → 𝐼 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑀 ) ) )
15 14 adantr ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑀 ∧ 𝑘 ∈ 𝑁 ) ) → 𝐼 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑀 ) ) )
16 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑀 ∧ 𝑘 ∈ 𝑁 ) ) → 𝑋 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) )
17 simprl ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑀 ∧ 𝑘 ∈ 𝑁 ) ) → 𝑙 ∈ 𝑀 )
18 simprr ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑀 ∧ 𝑘 ∈ 𝑁 ) ) → 𝑘 ∈ 𝑁 )
19 8 1 10 11 12 12 13 15 16 17 18 mamufv ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑀 ∧ 𝑘 ∈ 𝑁 ) ) → ( 𝑙 ( 𝐼 𝐹 𝑋 ) 𝑘 ) = ( 𝑅 Σg ( 𝑚 ∈ 𝑀 ↦ ( ( 𝑙 𝐼 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑋 𝑘 ) ) ) ) )
20 ringmnd ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
21 11 20 syl ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑀 ∧ 𝑘 ∈ 𝑁 ) ) → 𝑅 ∈ Mnd )
22 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑀 ∧ 𝑘 ∈ 𝑁 ) ) ∧ 𝑚 ∈ 𝑀 ) → 𝑅 ∈ Ring )
23 elmapi ⊢ ( 𝐼 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑀 ) ) → 𝐼 : ( 𝑀 × 𝑀 ) ⟶ 𝐵 )
24 14 23 syl ⊢ ( 𝜑 → 𝐼 : ( 𝑀 × 𝑀 ) ⟶ 𝐵 )
25 24 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑀 ∧ 𝑘 ∈ 𝑁 ) ) ∧ 𝑚 ∈ 𝑀 ) → 𝐼 : ( 𝑀 × 𝑀 ) ⟶ 𝐵 )
26 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑀 ∧ 𝑘 ∈ 𝑁 ) ) ∧ 𝑚 ∈ 𝑀 ) → 𝑙 ∈ 𝑀 )
27 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑀 ∧ 𝑘 ∈ 𝑁 ) ) ∧ 𝑚 ∈ 𝑀 ) → 𝑚 ∈ 𝑀 )
28 25 26 27 fovcdmd ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑀 ∧ 𝑘 ∈ 𝑁 ) ) ∧ 𝑚 ∈ 𝑀 ) → ( 𝑙 𝐼 𝑚 ) ∈ 𝐵 )
29 elmapi ⊢ ( 𝑋 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) → 𝑋 : ( 𝑀 × 𝑁 ) ⟶ 𝐵 )
30 9 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 26 3adant3 ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑀 ∧ 𝑘 ∈ 𝑁 ) ) ∧ 𝑚 ∈ 𝑀 ∧ 𝑚 ≠ 𝑙 ) → 𝑙 ∈ 𝑀 )
38 simp2 ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑀 ∧ 𝑘 ∈ 𝑁 ) ) ∧ 𝑚 ∈ 𝑀 ∧ 𝑚 ≠ 𝑙 ) → 𝑚 ∈ 𝑀 )
39 1 2 3 4 5 6 mat1comp ⊢ ( ( 𝑙 ∈ 𝑀 ∧ 𝑚 ∈ 𝑀 ) → ( 𝑙 𝐼 𝑚 ) = if ( 𝑙 = 𝑚 , 1 , 0 ) )
40 equcom ⊢ ( 𝑙 = 𝑚 ↔ 𝑚 = 𝑙 )
41 40 a1i ⊢ ( ( 𝑙 ∈ 𝑀 ∧ 𝑚 ∈ 𝑀 ) → ( 𝑙 = 𝑚 ↔ 𝑚 = 𝑙 ) )
42 41 ifbid ⊢ ( ( 𝑙 ∈ 𝑀 ∧ 𝑚 ∈ 𝑀 ) → if ( 𝑙 = 𝑚 , 1 , 0 ) = if ( 𝑚 = 𝑙 , 1 , 0 ) )
43 39 42 eqtrd ⊢ ( ( 𝑙 ∈ 𝑀 ∧ 𝑚 ∈ 𝑀 ) → ( 𝑙 𝐼 𝑚 ) = if ( 𝑚 = 𝑙 , 1 , 0 ) )
44 37 38 43 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑀 ∧ 𝑘 ∈ 𝑁 ) ) ∧ 𝑚 ∈ 𝑀 ∧ 𝑚 ≠ 𝑙 ) → ( 𝑙 𝐼 𝑚 ) = if ( 𝑚 = 𝑙 , 1 , 0 ) )
45 ifnefalse ⊢ ( 𝑚 ≠ 𝑙 → if ( 𝑚 = 𝑙 , 1 , 0 ) = 0 )
46 45 3ad2ant3 ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑀 ∧ 𝑘 ∈ 𝑁 ) ) ∧ 𝑚 ∈ 𝑀 ∧ 𝑚 ≠ 𝑙 ) → if ( 𝑚 = 𝑙 , 1 , 0 ) = 0 )
47 44 46 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑀 ∧ 𝑘 ∈ 𝑁 ) ) ∧ 𝑚 ∈ 𝑀 ∧ 𝑚 ≠ 𝑙 ) → ( 𝑙 𝐼 𝑚 ) = 0 )
48 47 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑀 ∧ 𝑘 ∈ 𝑁 ) ) ∧ 𝑚 ∈ 𝑀 ∧ 𝑚 ≠ 𝑙 ) → ( ( 𝑙 𝐼 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑋 𝑘 ) ) = ( 0 ( .r ‘ 𝑅 ) ( 𝑚 𝑋 𝑘 ) ) )
49 1 10 4 ringlz ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑚 𝑋 𝑘 ) ∈ 𝐵 ) → ( 0 ( .r ‘ 𝑅 ) ( 𝑚 𝑋 𝑘 ) ) = 0 )
50 22 33 49 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑀 ∧ 𝑘 ∈ 𝑁 ) ) ∧ 𝑚 ∈ 𝑀 ) → ( 0 ( .r ‘ 𝑅 ) ( 𝑚 𝑋 𝑘 ) ) = 0 )
51 50 3adant3 ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑀 ∧ 𝑘 ∈ 𝑁 ) ) ∧ 𝑚 ∈ 𝑀 ∧ 𝑚 ≠ 𝑙 ) → ( 0 ( .r ‘ 𝑅 ) ( 𝑚 𝑋 𝑘 ) ) = 0 )
52 48 51 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑀 ∧ 𝑘 ∈ 𝑁 ) ) ∧ 𝑚 ∈ 𝑀 ∧ 𝑚 ≠ 𝑙 ) → ( ( 𝑙 𝐼 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑋 𝑘 ) ) = 0 )
53 52 12 suppsssn ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑀 ∧ 𝑘 ∈ 𝑁 ) ) → ( ( 𝑚 ∈ 𝑀 ↦ ( ( 𝑙 𝐼 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑋 𝑘 ) ) ) supp 0 ) ⊆ { 𝑙 } )
54 1 4 21 12 17 36 53 gsumpt ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑀 ∧ 𝑘 ∈ 𝑁 ) ) → ( 𝑅 Σg ( 𝑚 ∈ 𝑀 ↦ ( ( 𝑙 𝐼 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑋 𝑘 ) ) ) ) = ( ( 𝑚 ∈ 𝑀 ↦ ( ( 𝑙 𝐼 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑋 𝑘 ) ) ) ‘ 𝑙 ) )
55 oveq2 ⊢ ( 𝑚 = 𝑙 → ( 𝑙 𝐼 𝑚 ) = ( 𝑙 𝐼 𝑙 ) )
56 oveq1 ⊢ ( 𝑚 = 𝑙 → ( 𝑚 𝑋 𝑘 ) = ( 𝑙 𝑋 𝑘 ) )
57 55 56 oveq12d ⊢ ( 𝑚 = 𝑙 → ( ( 𝑙 𝐼 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑋 𝑘 ) ) = ( ( 𝑙 𝐼 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑙 𝑋 𝑘 ) ) )
58 eqid ⊢ ( 𝑚 ∈ 𝑀 ↦ ( ( 𝑙 𝐼 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑋 𝑘 ) ) ) = ( 𝑚 ∈ 𝑀 ↦ ( ( 𝑙 𝐼 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑋 𝑘 ) ) )
59 ovex ⊢ ( ( 𝑙 𝐼 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑙 𝑋 𝑘 ) ) ∈ V
60 57 58 59 fvmpt ⊢ ( 𝑙 ∈ 𝑀 → ( ( 𝑚 ∈ 𝑀 ↦ ( ( 𝑙 𝐼 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑋 𝑘 ) ) ) ‘ 𝑙 ) = ( ( 𝑙 𝐼 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑙 𝑋 𝑘 ) ) )
61 60 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑀 ∧ 𝑘 ∈ 𝑁 ) ) → ( ( 𝑚 ∈ 𝑀 ↦ ( ( 𝑙 𝐼 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑋 𝑘 ) ) ) ‘ 𝑙 ) = ( ( 𝑙 𝐼 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑙 𝑋 𝑘 ) ) )
62 equequ1 ⊢ ( 𝑖 = 𝑙 → ( 𝑖 = 𝑗 ↔ 𝑙 = 𝑗 ) )
63 62 ifbid ⊢ ( 𝑖 = 𝑙 → if ( 𝑖 = 𝑗 , 1 , 0 ) = if ( 𝑙 = 𝑗 , 1 , 0 ) )
64 equequ2 ⊢ ( 𝑗 = 𝑙 → ( 𝑙 = 𝑗 ↔ 𝑙 = 𝑙 ) )
65 64 ifbid ⊢ ( 𝑗 = 𝑙 → if ( 𝑙 = 𝑗 , 1 , 0 ) = if ( 𝑙 = 𝑙 , 1 , 0 ) )
66 equid ⊢ 𝑙 = 𝑙
67 66 iftruei ⊢ if ( 𝑙 = 𝑙 , 1 , 0 ) = 1
68 65 67 eqtrdi ⊢ ( 𝑗 = 𝑙 → if ( 𝑙 = 𝑗 , 1 , 0 ) = 1 )
69 3 fvexi ⊢ 1 ∈ V
70 63 68 5 69 ovmpo ⊢ ( ( 𝑙 ∈ 𝑀 ∧ 𝑙 ∈ 𝑀 ) → ( 𝑙 𝐼 𝑙 ) = 1 )
71 70 anidms ⊢ ( 𝑙 ∈ 𝑀 → ( 𝑙 𝐼 𝑙 ) = 1 )
72 71 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑀 ∧ 𝑘 ∈ 𝑁 ) ) → ( 𝑙 𝐼 𝑙 ) = 1 )
73 72 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑀 ∧ 𝑘 ∈ 𝑁 ) ) → ( ( 𝑙 𝐼 𝑙 ) ( .r ‘ 𝑅 ) ( 𝑙 𝑋 𝑘 ) ) = ( 1 ( .r ‘ 𝑅 ) ( 𝑙 𝑋 𝑘 ) ) )
74 30 fovcdmda ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑀 ∧ 𝑘 ∈ 𝑁 ) ) → ( 𝑙 𝑋 𝑘 ) ∈ 𝐵 )
75 1 10 3 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑙 𝑋 𝑘 ) ∈ 𝐵 ) → ( 1 ( .r ‘ 𝑅 ) ( 𝑙 𝑋 𝑘 ) ) = ( 𝑙 𝑋 𝑘 ) )
76 11 74 75 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑀 ∧ 𝑘 ∈ 𝑁 ) ) → ( 1 ( .r ‘ 𝑅 ) ( 𝑙 𝑋 𝑘 ) ) = ( 𝑙 𝑋 𝑘 ) )
77 61 73 76 3eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑀 ∧ 𝑘 ∈ 𝑁 ) ) → ( ( 𝑚 ∈ 𝑀 ↦ ( ( 𝑙 𝐼 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑚 𝑋 𝑘 ) ) ) ‘ 𝑙 ) = ( 𝑙 𝑋 𝑘 ) )
78 19 54 77 3eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑀 ∧ 𝑘 ∈ 𝑁 ) ) → ( 𝑙 ( 𝐼 𝐹 𝑋 ) 𝑘 ) = ( 𝑙 𝑋 𝑘 ) )
79 78 ralrimivva ⊢ ( 𝜑 → ∀ 𝑙 ∈ 𝑀 ∀ 𝑘 ∈ 𝑁 ( 𝑙 ( 𝐼 𝐹 𝑋 ) 𝑘 ) = ( 𝑙 𝑋 𝑘 ) )
80 1 2 8 6 6 7 14 9 mamucl ⊢ ( 𝜑 → ( 𝐼 𝐹 𝑋 ) ∈ ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) )
81 elmapi ⊢ ( ( 𝐼 𝐹 𝑋 ) ∈ ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) → ( 𝐼 𝐹 𝑋 ) : ( 𝑀 × 𝑁 ) ⟶ 𝐵 )
82 80 81 syl ⊢ ( 𝜑 → ( 𝐼 𝐹 𝑋 ) : ( 𝑀 × 𝑁 ) ⟶ 𝐵 )
83 82 ffnd ⊢ ( 𝜑 → ( 𝐼 𝐹 𝑋 ) Fn ( 𝑀 × 𝑁 ) )
84 30 ffnd ⊢ ( 𝜑 → 𝑋 Fn ( 𝑀 × 𝑁 ) )
85 eqfnov2 ⊢ ( ( ( 𝐼 𝐹 𝑋 ) Fn ( 𝑀 × 𝑁 ) ∧ 𝑋 Fn ( 𝑀 × 𝑁 ) ) → ( ( 𝐼 𝐹 𝑋 ) = 𝑋 ↔ ∀ 𝑙 ∈ 𝑀 ∀ 𝑘 ∈ 𝑁 ( 𝑙 ( 𝐼 𝐹 𝑋 ) 𝑘 ) = ( 𝑙 𝑋 𝑘 ) ) )
86 83 84 85 syl2anc ⊢ ( 𝜑 → ( ( 𝐼 𝐹 𝑋 ) = 𝑋 ↔ ∀ 𝑙 ∈ 𝑀 ∀ 𝑘 ∈ 𝑁 ( 𝑙 ( 𝐼 𝐹 𝑋 ) 𝑘 ) = ( 𝑙 𝑋 𝑘 ) ) )
87 79 86 mpbird ⊢ ( 𝜑 → ( 𝐼 𝐹 𝑋 ) = 𝑋 )