scmatscmiddistr - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > scmatscmiddistr		Structured version Visualization version GIF version

Theorem scmatscmiddistr 22829

Description: Distributive law for scalar and ring multiplication for scalar matrices expressed as multiplications of a scalar with the identity matrix. (Contributed by AV, 19-Dec-2019.)

**Hypotheses**
Ref	Expression
scmatscmide.a	⊢ 𝐴 = (𝑁 Mat 𝑅)
scmatscmide.b	⊢ 𝐵 = (Base‘𝑅)
scmatscmide.0	⊢ 0 = (0_g‘𝑅)
scmatscmide.1	⊢ 1 = (1_r‘𝐴)
scmatscmide.m	⊢ ∗ = ( ·_𝑠 ‘𝐴)
scmatscmiddistr.t	⊢ · = (._r‘𝑅)
scmatscmiddistr.m	⊢ × = (._r‘𝐴)

**Assertion**
Ref	Expression
scmatscmiddistr	⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) → ((𝑆 ∗ 1 ) × (𝑇 ∗ 1 )) = ((𝑆 · 𝑇) ∗ 1 ))

Proof of Theorem scmatscmiddistr Dummy variables 𝑖 𝑗 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simprl 783	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) → 𝑆 ∈ 𝐵)
2		scmatscmide.1	. . . . . . . 8 ⊢ 1 = (1_r‘𝐴)
3		scmatscmide.a	. . . . . . . . 9 ⊢ 𝐴 = (𝑁 Mat 𝑅)
4		eqid 2760	. . . . . . . . 9 ⊢ (Base‘𝐴) = (Base‘𝐴)
5		scmatscmide.0	. . . . . . . . 9 ⊢ 0 = (0_g‘𝑅)
6		eqid 2760	. . . . . . . . 9 ⊢ (𝑁 DMat 𝑅) = (𝑁 DMat 𝑅)
7	3, 4, 5, 6	dmatid 22816	. . . . . . . 8 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (1_r‘𝐴) ∈ (𝑁 DMat 𝑅))
8	2, 7	eqeltrid 2864	. . . . . . 7 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 1 ∈ (𝑁 DMat 𝑅))
9	8	adantr 486	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) → 1 ∈ (𝑁 DMat 𝑅))
10	1, 9	jca 521	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) → (𝑆 ∈ 𝐵 ∧ 1 ∈ (𝑁 DMat 𝑅)))
11		scmatscmide.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝑅)
12		scmatscmide.m	. . . . . 6 ⊢ ∗ = ( ·_𝑠 ‘𝐴)
13	11, 3, 4, 12, 6	dmatscmcl 22824	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 1 ∈ (𝑁 DMat 𝑅))) → (𝑆 ∗ 1 ) ∈ (𝑁 DMat 𝑅))
14	10, 13	syldan 603	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) → (𝑆 ∗ 1 ) ∈ (𝑁 DMat 𝑅))
15		simprr 785	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) → 𝑇 ∈ 𝐵)
16	15, 9	jca 521	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) → (𝑇 ∈ 𝐵 ∧ 1 ∈ (𝑁 DMat 𝑅)))
17	11, 3, 4, 12, 6	dmatscmcl 22824	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑇 ∈ 𝐵 ∧ 1 ∈ (𝑁 DMat 𝑅))) → (𝑇 ∗ 1 ) ∈ (𝑁 DMat 𝑅))
18	16, 17	syldan 603	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) → (𝑇 ∗ 1 ) ∈ (𝑁 DMat 𝑅))
19	14, 18	jca 521	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) → ((𝑆 ∗ 1 ) ∈ (𝑁 DMat 𝑅) ∧ (𝑇 ∗ 1 ) ∈ (𝑁 DMat 𝑅)))
20		scmatscmiddistr.m	. . . . 5 ⊢ × = (._r‘𝐴)
21	20	oveqi 7434	. . . 4 ⊢ ((𝑆 ∗ 1 ) × (𝑇 ∗ 1 )) = ((𝑆 ∗ 1 )(._r‘𝐴)(𝑇 ∗ 1 ))
22	3, 4, 5, 6	dmatmul 22818	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ ((𝑆 ∗ 1 ) ∈ (𝑁 DMat 𝑅) ∧ (𝑇 ∗ 1 ) ∈ (𝑁 DMat 𝑅))) → ((𝑆 ∗ 1 )(._r‘𝐴)(𝑇 ∗ 1 )) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, ((𝑖(𝑆 ∗ 1 )𝑗)(._r‘𝑅)(𝑖(𝑇 ∗ 1 )𝑗)), 0 )))
23	21, 22	eqtrid 2807	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ ((𝑆 ∗ 1 ) ∈ (𝑁 DMat 𝑅) ∧ (𝑇 ∗ 1 ) ∈ (𝑁 DMat 𝑅))) → ((𝑆 ∗ 1 ) × (𝑇 ∗ 1 )) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, ((𝑖(𝑆 ∗ 1 )𝑗)(._r‘𝑅)(𝑖(𝑇 ∗ 1 )𝑗)), 0 )))
24	19, 23	syldan 603	. 2 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) → ((𝑆 ∗ 1 ) × (𝑇 ∗ 1 )) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, ((𝑖(𝑆 ∗ 1 )𝑗)(._r‘𝑅)(𝑖(𝑇 ∗ 1 )𝑗)), 0 )))
25		simpll 779	. . . . . . . . 9 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) → 𝑁 ∈ Fin)
26		simplr 781	. . . . . . . . 9 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) → 𝑅 ∈ Ring)
27	25, 26, 1	3jca 1146	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐵))
28	27	3ad2ant1 1151	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐵))
29		3simpc 1168	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁))
30	3, 11, 5, 2, 12	scmatscmide 22828	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖(𝑆 ∗ 1 )𝑗) = if(𝑖 = 𝑗, 𝑆, 0 ))
31	28, 29, 30	syl2anc 596	. . . . . 6 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑖(𝑆 ∗ 1 )𝑗) = if(𝑖 = 𝑗, 𝑆, 0 ))
32	25, 26, 15	3jca 1146	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑇 ∈ 𝐵))
33	32	3ad2ant1 1151	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑇 ∈ 𝐵))
34	3, 11, 5, 2, 12	scmatscmide 22828	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑇 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖(𝑇 ∗ 1 )𝑗) = if(𝑖 = 𝑗, 𝑇, 0 ))
35	33, 29, 34	syl2anc 596	. . . . . 6 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑖(𝑇 ∗ 1 )𝑗) = if(𝑖 = 𝑗, 𝑇, 0 ))
36	31, 35	oveq12d 7439	. . . . 5 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((𝑖(𝑆 ∗ 1 )𝑗)(._r‘𝑅)(𝑖(𝑇 ∗ 1 )𝑗)) = (if(𝑖 = 𝑗, 𝑆, 0 )(._r‘𝑅)if(𝑖 = 𝑗, 𝑇, 0 )))
37	36	ifeq1d 4501	. . . 4 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → if(𝑖 = 𝑗, ((𝑖(𝑆 ∗ 1 )𝑗)(._r‘𝑅)(𝑖(𝑇 ∗ 1 )𝑗)), 0 ) = if(𝑖 = 𝑗, (if(𝑖 = 𝑗, 𝑆, 0 )(._r‘𝑅)if(𝑖 = 𝑗, 𝑇, 0 )), 0 ))
38	37	mpoeq3dva 7498	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, ((𝑖(𝑆 ∗ 1 )𝑗)(._r‘𝑅)(𝑖(𝑇 ∗ 1 )𝑗)), 0 )) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, (if(𝑖 = 𝑗, 𝑆, 0 )(._r‘𝑅)if(𝑖 = 𝑗, 𝑇, 0 )), 0 )))
39		iftrue 4487	. . . . . . . 8 ⊢ (𝑖 = 𝑗 → if(𝑖 = 𝑗, 𝑆, 0 ) = 𝑆)
40		iftrue 4487	. . . . . . . 8 ⊢ (𝑖 = 𝑗 → if(𝑖 = 𝑗, 𝑇, 0 ) = 𝑇)
41	39, 40	oveq12d 7439	. . . . . . 7 ⊢ (𝑖 = 𝑗 → (if(𝑖 = 𝑗, 𝑆, 0 )(._r‘𝑅)if(𝑖 = 𝑗, 𝑇, 0 )) = (𝑆(._r‘𝑅)𝑇))
42	41	adantl 487	. . . . . 6 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) ∧ 𝑖 = 𝑗) → (if(𝑖 = 𝑗, 𝑆, 0 )(._r‘𝑅)if(𝑖 = 𝑗, 𝑇, 0 )) = (𝑆(._r‘𝑅)𝑇))
43	42	ifeq1da 4513	. . . . 5 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → if(𝑖 = 𝑗, (if(𝑖 = 𝑗, 𝑆, 0 )(._r‘𝑅)if(𝑖 = 𝑗, 𝑇, 0 )), 0 ) = if(𝑖 = 𝑗, (𝑆(._r‘𝑅)𝑇), 0 ))
44	43	mpoeq3dva 7498	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, (if(𝑖 = 𝑗, 𝑆, 0 )(._r‘𝑅)if(𝑖 = 𝑗, 𝑇, 0 )), 0 )) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, (𝑆(._r‘𝑅)𝑇), 0 )))
45		eqidd 2761	. . . . . . . 8 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, (𝑆(._r‘𝑅)𝑇), 0 )) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, (𝑆(._r‘𝑅)𝑇), 0 )))
46		eqeq12 2777	. . . . . . . . . 10 ⊢ ((𝑖 = 𝑥 ∧ 𝑗 = 𝑦) → (𝑖 = 𝑗 ↔ 𝑥 = 𝑦))
47		scmatscmiddistr.t	. . . . . . . . . . . . 13 ⊢ · = (._r‘𝑅)
48	47	eqcomi 2769	. . . . . . . . . . . 12 ⊢ (._r‘𝑅) = ·
49	48	oveqi 7434	. . . . . . . . . . 11 ⊢ (𝑆(._r‘𝑅)𝑇) = (𝑆 · 𝑇)
50	49	a1i 11	. . . . . . . . . 10 ⊢ ((𝑖 = 𝑥 ∧ 𝑗 = 𝑦) → (𝑆(._r‘𝑅)𝑇) = (𝑆 · 𝑇))
51	46, 50	ifbieq1d 4506	. . . . . . . . 9 ⊢ ((𝑖 = 𝑥 ∧ 𝑗 = 𝑦) → if(𝑖 = 𝑗, (𝑆(._r‘𝑅)𝑇), 0 ) = if(𝑥 = 𝑦, (𝑆 · 𝑇), 0 ))
52	51	adantl 487	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) ∧ (𝑖 = 𝑥 ∧ 𝑗 = 𝑦)) → if(𝑖 = 𝑗, (𝑆(._r‘𝑅)𝑇), 0 ) = if(𝑥 = 𝑦, (𝑆 · 𝑇), 0 ))
53		simprl 783	. . . . . . . 8 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → 𝑥 ∈ 𝑁)
54		simprr 785	. . . . . . . 8 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → 𝑦 ∈ 𝑁)
55		ovex 7454	. . . . . . . . . 10 ⊢ (𝑆 · 𝑇) ∈ V
56	5	fvexi 6900	. . . . . . . . . 10 ⊢ 0 ∈ V
57	55, 56	ifex 4532	. . . . . . . . 9 ⊢ if(𝑥 = 𝑦, (𝑆 · 𝑇), 0 ) ∈ V
58	57	a1i 11	. . . . . . . 8 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → if(𝑥 = 𝑦, (𝑆 · 𝑇), 0 ) ∈ V)
59	45, 52, 53, 54, 58	ovmpod 7573	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → (𝑥(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, (𝑆(._r‘𝑅)𝑇), 0 ))𝑦) = if(𝑥 = 𝑦, (𝑆 · 𝑇), 0 ))
60	26, 1, 15	3jca 1146	. . . . . . . . . 10 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) → (𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵))
61	11, 47	ringcl 20483	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵) → (𝑆 · 𝑇) ∈ 𝐵)
62	60, 61	syl 18	. . . . . . . . 9 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) → (𝑆 · 𝑇) ∈ 𝐵)
63	25, 26, 62	3jca 1146	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑆 · 𝑇) ∈ 𝐵))
64	3, 11, 5, 2, 12	scmatscmide 22828	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑆 · 𝑇) ∈ 𝐵) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → (𝑥((𝑆 · 𝑇) ∗ 1 )𝑦) = if(𝑥 = 𝑦, (𝑆 · 𝑇), 0 ))
65	63, 64	sylan 592	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → (𝑥((𝑆 · 𝑇) ∗ 1 )𝑦) = if(𝑥 = 𝑦, (𝑆 · 𝑇), 0 ))
66	59, 65	eqtr4d 2798	. . . . . 6 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) ∧ (𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁)) → (𝑥(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, (𝑆(._r‘𝑅)𝑇), 0 ))𝑦) = (𝑥((𝑆 · 𝑇) ∗ 1 )𝑦))
67	66	ralrimivva 3205	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) → ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, (𝑆(._r‘𝑅)𝑇), 0 ))𝑦) = (𝑥((𝑆 · 𝑇) ∗ 1 )𝑦))
68		eqid 2760	. . . . . . . . . . 11 ⊢ (._r‘𝑅) = (._r‘𝑅)
69	11, 68	ringcl 20483	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵) → (𝑆(._r‘𝑅)𝑇) ∈ 𝐵)
70	60, 69	syl 18	. . . . . . . . 9 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) → (𝑆(._r‘𝑅)𝑇) ∈ 𝐵)
71	11, 5	ring0cl 20502	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Ring → 0 ∈ 𝐵)
72	71	adantl 487	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 0 ∈ 𝐵)
73	72	adantr 486	. . . . . . . . 9 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) → 0 ∈ 𝐵)
74	70, 73	ifcld 4528	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) → if(𝑖 = 𝑗, (𝑆(._r‘𝑅)𝑇), 0 ) ∈ 𝐵)
75	74	3ad2ant1 1151	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → if(𝑖 = 𝑗, (𝑆(._r‘𝑅)𝑇), 0 ) ∈ 𝐵)
76	3, 11, 4, 25, 26, 75	matbas2d 22744	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, (𝑆(._r‘𝑅)𝑇), 0 )) ∈ (Base‘𝐴))
77	3	matring 22764	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring)
78	4, 2	ringidcl 20500	. . . . . . . . . 10 ⊢ (𝐴 ∈ Ring → 1 ∈ (Base‘𝐴))
79	77, 78	syl 18	. . . . . . . . 9 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 1 ∈ (Base‘𝐴))
80	79	adantr 486	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) → 1 ∈ (Base‘𝐴))
81	62, 80	jca 521	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) → ((𝑆 · 𝑇) ∈ 𝐵 ∧ 1 ∈ (Base‘𝐴)))
82	11, 3, 4, 12	matvscl 22752	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ ((𝑆 · 𝑇) ∈ 𝐵 ∧ 1 ∈ (Base‘𝐴))) → ((𝑆 · 𝑇) ∗ 1 ) ∈ (Base‘𝐴))
83	81, 82	syldan 603	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) → ((𝑆 · 𝑇) ∗ 1 ) ∈ (Base‘𝐴))
84	3, 4	eqmat 22745	. . . . . 6 ⊢ (((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, (𝑆(._r‘𝑅)𝑇), 0 )) ∈ (Base‘𝐴) ∧ ((𝑆 · 𝑇) ∗ 1 ) ∈ (Base‘𝐴)) → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, (𝑆(._r‘𝑅)𝑇), 0 )) = ((𝑆 · 𝑇) ∗ 1 ) ↔ ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, (𝑆(._r‘𝑅)𝑇), 0 ))𝑦) = (𝑥((𝑆 · 𝑇) ∗ 1 )𝑦)))
85	76, 83, 84	syl2anc 596	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, (𝑆(._r‘𝑅)𝑇), 0 )) = ((𝑆 · 𝑇) ∗ 1 ) ↔ ∀𝑥 ∈ 𝑁 ∀𝑦 ∈ 𝑁 (𝑥(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, (𝑆(._r‘𝑅)𝑇), 0 ))𝑦) = (𝑥((𝑆 · 𝑇) ∗ 1 )𝑦)))
86	67, 85	mpbird 260	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, (𝑆(._r‘𝑅)𝑇), 0 )) = ((𝑆 · 𝑇) ∗ 1 ))
87	44, 86	eqtrd 2795	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, (if(𝑖 = 𝑗, 𝑆, 0 )(._r‘𝑅)if(𝑖 = 𝑗, 𝑇, 0 )), 0 )) = ((𝑆 · 𝑇) ∗ 1 ))
88	38, 87	eqtrd 2795	. 2 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, ((𝑖(𝑆 ∗ 1 )𝑗)(._r‘𝑅)(𝑖(𝑇 ∗ 1 )𝑗)), 0 )) = ((𝑆 · 𝑇) ∗ 1 ))
89	24, 88	eqtrd 2795	1 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) → ((𝑆 ∗ 1 ) × (𝑇 ∗ 1 )) = ((𝑆 · 𝑇) ∗ 1 ))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ∀wral 3076 Vcvv 3450 ifcif 4481 ‘cfv 6539 (class class class)co 7421 ∈ cmpo 7423 Fincfn 8977 Basecbs 17393 ._rcmulr 17435 ·_𝑠 cvsca 17438 0_gc0g 17616 1_rcur 20413 Ringcrg 20465 Mat cmat 22728 DMat cdmat 22809

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7752 ax-cnex 11260 ax-resscn 11261 ax-1cn 11262 ax-icn 11263 ax-addcl 11264 ax-addrcl 11265 ax-mulcl 11266 ax-mulrcl 11267 ax-mulcom 11268 ax-addass 11269 ax-mulass 11270 ax-distr 11271 ax-i2m1 11272 ax-1ne0 11273 ax-1rid 11274 ax-rnegex 11275 ax-rrecex 11276 ax-cnre 11277 ax-pre-lttri 11278 ax-pre-lttrn 11279 ax-pre-ltadd 11280 ax-pre-mulgt0 11281

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4835 df-ot 4858 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-isom 6548 df-riota 7378 df-ov 7424 df-oprab 7425 df-mpo 7426 df-of 7694 df-om 7879 df-1st 8002 df-2nd 8003 df-supp 8181 df-frecs 8303 df-wrecs 8334 df-recs 8383 df-rdg 8422 df-1o 8480 df-2o 8481 df-er 8721 df-map 8853 df-ixp 8930 df-en 8978 df-dom 8979 df-sdom 8980 df-fin 8981 df-fsupp 9358 df-sup 9438 df-oi 9508 df-card 10024 df-pnf 11349 df-mnf 11350 df-xr 11351 df-ltxr 11352 df-le 11353 df-sub 11547 df-neg 11548 df-nn 12340 df-2 12409 df-3 12410 df-4 12411 df-5 12412 df-6 12413 df-7 12414 df-8 12415 df-9 12416 df-n0 12611 df-z 12698 df-dec 12819 df-uz 12970 df-fz 13644 df-fzo 13793 df-seq 14149 df-hash 14479 df-struct 17331 df-sets 17348 df-slot 17366 df-ndx 17378 df-base 17394 df-ress 17415 df-plusg 17447 df-mulr 17448 df-sca 17450 df-vsca 17451 df-ip 17452 df-tset 17453 df-ple 17454 df-ds 17456 df-hom 17458 df-cco 17459 df-0g 17618 df-gsum 17619 df-prds 17624 df-pws 17626 df-mre 17762 df-mrc 17763 df-acs 17765 df-mgm 18822 df-sgrp 18914 df-mnd 18930 df-mhm 18984 df-submnd 18985 df-grp 19153 df-minusg 19154 df-sbg 19155 df-mulg 19284 df-subg 19339 df-ghm 19434 df-cntz 19537 df-cmn 20002 df-abl 20003 df-mgp 20367 df-rng 20381 df-ur 20414 df-ring 20467 df-subrg 20828 df-lmod 21143 df-lss 21213 df-sra 21454 df-rgmod 21455 df-dsmm 22044 df-frlm 22059 df-mamu 22712 df-mat 22729 df-dmat 22811

This theorem is used by: scmatmulcl 22839 scmatmhm 22855

W3C validator