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 = ( 1_r ‘ 𝑅 )
	mamumat1cl.z	⊢ 0 = ( 0_g ‘ 𝑅 )
	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 = ( 1_r ‘ 𝑅 )
4		mamumat1cl.z	⊢ 0 = ( 0_g ‘ 𝑅 )
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	⊢ ( 𝜑 → ( 𝑋 𝐹 𝐼 ) = 𝑋 )

Metamath Proof Explorer

Theorem mamurid

Proof