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

Metamath Proof Explorer

Theorem mamulid

Proof