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

Theorem mamuvs2 22350
Description: Matrix multiplication distributes over scalar multiplication on the left. (Contributed by Stefan O'Rear, 5-Sep-2015.) (Proof shortened by AV, 22-Jul-2019.)
Hypotheses
Ref Expression
mamuvs2.r (𝜑𝑅 ∈ CRing)
mamuvs2.b 𝐵 = (Base‘𝑅)
mamuvs2.t · = (.r𝑅)
mamuvs2.f 𝐹 = (𝑅 maMul ⟨𝑀, 𝑁, 𝑂⟩)
mamuvs2.m (𝜑𝑀 ∈ Fin)
mamuvs2.n (𝜑𝑁 ∈ Fin)
mamuvs2.o (𝜑𝑂 ∈ Fin)
mamuvs2.x (𝜑𝑋 ∈ (𝐵m (𝑀 × 𝑁)))
mamuvs2.y (𝜑𝑌𝐵)
mamuvs2.z (𝜑𝑍 ∈ (𝐵m (𝑁 × 𝑂)))
Assertion
Ref Expression
mamuvs2 (𝜑 → (𝑋𝐹(((𝑁 × 𝑂) × {𝑌}) ∘f · 𝑍)) = (((𝑀 × 𝑂) × {𝑌}) ∘f · (𝑋𝐹𝑍)))

Proof of Theorem mamuvs2
Dummy variables 𝑖 𝑘 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ov 7422 . . . . . . . . . 10 (𝑗(((𝑁 × 𝑂) × {𝑌}) ∘f · 𝑍)𝑘) = ((((𝑁 × 𝑂) × {𝑌}) ∘f · 𝑍)‘⟨𝑗, 𝑘⟩)
2 simpr 483 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑀𝑘𝑂)) ∧ 𝑗𝑁) → 𝑗𝑁)
3 simplrr 776 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑀𝑘𝑂)) ∧ 𝑗𝑁) → 𝑘𝑂)
4 opelxpi 5715 . . . . . . . . . . . 12 ((𝑗𝑁𝑘𝑂) → ⟨𝑗, 𝑘⟩ ∈ (𝑁 × 𝑂))
52, 3, 4syl2anc 582 . . . . . . . . . . 11 (((𝜑 ∧ (𝑖𝑀𝑘𝑂)) ∧ 𝑗𝑁) → ⟨𝑗, 𝑘⟩ ∈ (𝑁 × 𝑂))
6 mamuvs2.n . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ Fin)
7 mamuvs2.o . . . . . . . . . . . . . 14 (𝜑𝑂 ∈ Fin)
8 xpfi 9343 . . . . . . . . . . . . . 14 ((𝑁 ∈ Fin ∧ 𝑂 ∈ Fin) → (𝑁 × 𝑂) ∈ Fin)
96, 7, 8syl2anc 582 . . . . . . . . . . . . 13 (𝜑 → (𝑁 × 𝑂) ∈ Fin)
109ad2antrr 724 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑀𝑘𝑂)) ∧ 𝑗𝑁) → (𝑁 × 𝑂) ∈ Fin)
11 mamuvs2.y . . . . . . . . . . . . 13 (𝜑𝑌𝐵)
1211ad2antrr 724 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑀𝑘𝑂)) ∧ 𝑗𝑁) → 𝑌𝐵)
13 mamuvs2.z . . . . . . . . . . . . . 14 (𝜑𝑍 ∈ (𝐵m (𝑁 × 𝑂)))
14 elmapi 8868 . . . . . . . . . . . . . 14 (𝑍 ∈ (𝐵m (𝑁 × 𝑂)) → 𝑍:(𝑁 × 𝑂)⟶𝐵)
15 ffn 6723 . . . . . . . . . . . . . 14 (𝑍:(𝑁 × 𝑂)⟶𝐵𝑍 Fn (𝑁 × 𝑂))
1613, 14, 153syl 18 . . . . . . . . . . . . 13 (𝜑𝑍 Fn (𝑁 × 𝑂))
1716ad2antrr 724 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖𝑀𝑘𝑂)) ∧ 𝑗𝑁) → 𝑍 Fn (𝑁 × 𝑂))
18 df-ov 7422 . . . . . . . . . . . . . 14 (𝑗𝑍𝑘) = (𝑍‘⟨𝑗, 𝑘⟩)
1918eqcomi 2734 . . . . . . . . . . . . 13 (𝑍‘⟨𝑗, 𝑘⟩) = (𝑗𝑍𝑘)
2019a1i 11 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑖𝑀𝑘𝑂)) ∧ 𝑗𝑁) ∧ ⟨𝑗, 𝑘⟩ ∈ (𝑁 × 𝑂)) → (𝑍‘⟨𝑗, 𝑘⟩) = (𝑗𝑍𝑘))
2110, 12, 17, 20ofc1 7712 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑖𝑀𝑘𝑂)) ∧ 𝑗𝑁) ∧ ⟨𝑗, 𝑘⟩ ∈ (𝑁 × 𝑂)) → ((((𝑁 × 𝑂) × {𝑌}) ∘f · 𝑍)‘⟨𝑗, 𝑘⟩) = (𝑌 · (𝑗𝑍𝑘)))
225, 21mpdan 685 . . . . . . . . . 10 (((𝜑 ∧ (𝑖𝑀𝑘𝑂)) ∧ 𝑗𝑁) → ((((𝑁 × 𝑂) × {𝑌}) ∘f · 𝑍)‘⟨𝑗, 𝑘⟩) = (𝑌 · (𝑗𝑍𝑘)))
231, 22eqtrid 2777 . . . . . . . . 9 (((𝜑 ∧ (𝑖𝑀𝑘𝑂)) ∧ 𝑗𝑁) → (𝑗(((𝑁 × 𝑂) × {𝑌}) ∘f · 𝑍)𝑘) = (𝑌 · (𝑗𝑍𝑘)))
2423oveq2d 7435 . . . . . . . 8 (((𝜑 ∧ (𝑖𝑀𝑘𝑂)) ∧ 𝑗𝑁) → ((𝑖𝑋𝑗) · (𝑗(((𝑁 × 𝑂) × {𝑌}) ∘f · 𝑍)𝑘)) = ((𝑖𝑋𝑗) · (𝑌 · (𝑗𝑍𝑘))))
25 mamuvs2.r . . . . . . . . . . 11 (𝜑𝑅 ∈ CRing)
26 eqid 2725 . . . . . . . . . . . 12 (mulGrp‘𝑅) = (mulGrp‘𝑅)
2726crngmgp 20193 . . . . . . . . . . 11 (𝑅 ∈ CRing → (mulGrp‘𝑅) ∈ CMnd)
2825, 27syl 17 . . . . . . . . . 10 (𝜑 → (mulGrp‘𝑅) ∈ CMnd)
2928ad2antrr 724 . . . . . . . . 9 (((𝜑 ∧ (𝑖𝑀𝑘𝑂)) ∧ 𝑗𝑁) → (mulGrp‘𝑅) ∈ CMnd)
30 mamuvs2.x . . . . . . . . . . . 12 (𝜑𝑋 ∈ (𝐵m (𝑀 × 𝑁)))
31 elmapi 8868 . . . . . . . . . . . 12 (𝑋 ∈ (𝐵m (𝑀 × 𝑁)) → 𝑋:(𝑀 × 𝑁)⟶𝐵)
3230, 31syl 17 . . . . . . . . . . 11 (𝜑𝑋:(𝑀 × 𝑁)⟶𝐵)
3332ad2antrr 724 . . . . . . . . . 10 (((𝜑 ∧ (𝑖𝑀𝑘𝑂)) ∧ 𝑗𝑁) → 𝑋:(𝑀 × 𝑁)⟶𝐵)
34 simplrl 775 . . . . . . . . . 10 (((𝜑 ∧ (𝑖𝑀𝑘𝑂)) ∧ 𝑗𝑁) → 𝑖𝑀)
3533, 34, 2fovcdmd 7593 . . . . . . . . 9 (((𝜑 ∧ (𝑖𝑀𝑘𝑂)) ∧ 𝑗𝑁) → (𝑖𝑋𝑗) ∈ 𝐵)
3613, 14syl 17 . . . . . . . . . . 11 (𝜑𝑍:(𝑁 × 𝑂)⟶𝐵)
3736ad2antrr 724 . . . . . . . . . 10 (((𝜑 ∧ (𝑖𝑀𝑘𝑂)) ∧ 𝑗𝑁) → 𝑍:(𝑁 × 𝑂)⟶𝐵)
3837, 2, 3fovcdmd 7593 . . . . . . . . 9 (((𝜑 ∧ (𝑖𝑀𝑘𝑂)) ∧ 𝑗𝑁) → (𝑗𝑍𝑘) ∈ 𝐵)
39 mamuvs2.b . . . . . . . . . . 11 𝐵 = (Base‘𝑅)
4026, 39mgpbas 20092 . . . . . . . . . 10 𝐵 = (Base‘(mulGrp‘𝑅))
41 mamuvs2.t . . . . . . . . . . 11 · = (.r𝑅)
4226, 41mgpplusg 20090 . . . . . . . . . 10 · = (+g‘(mulGrp‘𝑅))
4340, 42cmn12 19769 . . . . . . . . 9 (((mulGrp‘𝑅) ∈ CMnd ∧ ((𝑖𝑋𝑗) ∈ 𝐵𝑌𝐵 ∧ (𝑗𝑍𝑘) ∈ 𝐵)) → ((𝑖𝑋𝑗) · (𝑌 · (𝑗𝑍𝑘))) = (𝑌 · ((𝑖𝑋𝑗) · (𝑗𝑍𝑘))))
4429, 35, 12, 38, 43syl13anc 1369 . . . . . . . 8 (((𝜑 ∧ (𝑖𝑀𝑘𝑂)) ∧ 𝑗𝑁) → ((𝑖𝑋𝑗) · (𝑌 · (𝑗𝑍𝑘))) = (𝑌 · ((𝑖𝑋𝑗) · (𝑗𝑍𝑘))))
4524, 44eqtrd 2765 . . . . . . 7 (((𝜑 ∧ (𝑖𝑀𝑘𝑂)) ∧ 𝑗𝑁) → ((𝑖𝑋𝑗) · (𝑗(((𝑁 × 𝑂) × {𝑌}) ∘f · 𝑍)𝑘)) = (𝑌 · ((𝑖𝑋𝑗) · (𝑗𝑍𝑘))))
4645mpteq2dva 5249 . . . . . 6 ((𝜑 ∧ (𝑖𝑀𝑘𝑂)) → (𝑗𝑁 ↦ ((𝑖𝑋𝑗) · (𝑗(((𝑁 × 𝑂) × {𝑌}) ∘f · 𝑍)𝑘))) = (𝑗𝑁 ↦ (𝑌 · ((𝑖𝑋𝑗) · (𝑗𝑍𝑘)))))
4746oveq2d 7435 . . . . 5 ((𝜑 ∧ (𝑖𝑀𝑘𝑂)) → (𝑅 Σg (𝑗𝑁 ↦ ((𝑖𝑋𝑗) · (𝑗(((𝑁 × 𝑂) × {𝑌}) ∘f · 𝑍)𝑘)))) = (𝑅 Σg (𝑗𝑁 ↦ (𝑌 · ((𝑖𝑋𝑗) · (𝑗𝑍𝑘))))))
48 eqid 2725 . . . . . 6 (0g𝑅) = (0g𝑅)
49 crngring 20197 . . . . . . . 8 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
5025, 49syl 17 . . . . . . 7 (𝜑𝑅 ∈ Ring)
5150adantr 479 . . . . . 6 ((𝜑 ∧ (𝑖𝑀𝑘𝑂)) → 𝑅 ∈ Ring)
526adantr 479 . . . . . 6 ((𝜑 ∧ (𝑖𝑀𝑘𝑂)) → 𝑁 ∈ Fin)
5311adantr 479 . . . . . 6 ((𝜑 ∧ (𝑖𝑀𝑘𝑂)) → 𝑌𝐵)
5450ad2antrr 724 . . . . . . 7 (((𝜑 ∧ (𝑖𝑀𝑘𝑂)) ∧ 𝑗𝑁) → 𝑅 ∈ Ring)
5539, 41, 54, 35, 38ringcld 20211 . . . . . 6 (((𝜑 ∧ (𝑖𝑀𝑘𝑂)) ∧ 𝑗𝑁) → ((𝑖𝑋𝑗) · (𝑗𝑍𝑘)) ∈ 𝐵)
56 eqid 2725 . . . . . . 7 (𝑗𝑁 ↦ ((𝑖𝑋𝑗) · (𝑗𝑍𝑘))) = (𝑗𝑁 ↦ ((𝑖𝑋𝑗) · (𝑗𝑍𝑘)))
57 ovexd 7454 . . . . . . 7 (((𝜑 ∧ (𝑖𝑀𝑘𝑂)) ∧ 𝑗𝑁) → ((𝑖𝑋𝑗) · (𝑗𝑍𝑘)) ∈ V)
58 fvexd 6911 . . . . . . 7 ((𝜑 ∧ (𝑖𝑀𝑘𝑂)) → (0g𝑅) ∈ V)
5956, 52, 57, 58fsuppmptdm 9401 . . . . . 6 ((𝜑 ∧ (𝑖𝑀𝑘𝑂)) → (𝑗𝑁 ↦ ((𝑖𝑋𝑗) · (𝑗𝑍𝑘))) finSupp (0g𝑅))
6039, 48, 41, 51, 52, 53, 55, 59gsummulc2 20265 . . . . 5 ((𝜑 ∧ (𝑖𝑀𝑘𝑂)) → (𝑅 Σg (𝑗𝑁 ↦ (𝑌 · ((𝑖𝑋𝑗) · (𝑗𝑍𝑘))))) = (𝑌 · (𝑅 Σg (𝑗𝑁 ↦ ((𝑖𝑋𝑗) · (𝑗𝑍𝑘))))))
6147, 60eqtrd 2765 . . . 4 ((𝜑 ∧ (𝑖𝑀𝑘𝑂)) → (𝑅 Σg (𝑗𝑁 ↦ ((𝑖𝑋𝑗) · (𝑗(((𝑁 × 𝑂) × {𝑌}) ∘f · 𝑍)𝑘)))) = (𝑌 · (𝑅 Σg (𝑗𝑁 ↦ ((𝑖𝑋𝑗) · (𝑗𝑍𝑘))))))
62 mamuvs2.f . . . . 5 𝐹 = (𝑅 maMul ⟨𝑀, 𝑁, 𝑂⟩)
6325adantr 479 . . . . 5 ((𝜑 ∧ (𝑖𝑀𝑘𝑂)) → 𝑅 ∈ CRing)
64 mamuvs2.m . . . . . 6 (𝜑𝑀 ∈ Fin)
6564adantr 479 . . . . 5 ((𝜑 ∧ (𝑖𝑀𝑘𝑂)) → 𝑀 ∈ Fin)
667adantr 479 . . . . 5 ((𝜑 ∧ (𝑖𝑀𝑘𝑂)) → 𝑂 ∈ Fin)
6730adantr 479 . . . . 5 ((𝜑 ∧ (𝑖𝑀𝑘𝑂)) → 𝑋 ∈ (𝐵m (𝑀 × 𝑁)))
68 fconst6g 6786 . . . . . . . . 9 (𝑌𝐵 → ((𝑁 × 𝑂) × {𝑌}):(𝑁 × 𝑂)⟶𝐵)
6911, 68syl 17 . . . . . . . 8 (𝜑 → ((𝑁 × 𝑂) × {𝑌}):(𝑁 × 𝑂)⟶𝐵)
7039fvexi 6910 . . . . . . . . 9 𝐵 ∈ V
71 elmapg 8858 . . . . . . . . 9 ((𝐵 ∈ V ∧ (𝑁 × 𝑂) ∈ Fin) → (((𝑁 × 𝑂) × {𝑌}) ∈ (𝐵m (𝑁 × 𝑂)) ↔ ((𝑁 × 𝑂) × {𝑌}):(𝑁 × 𝑂)⟶𝐵))
7270, 9, 71sylancr 585 . . . . . . . 8 (𝜑 → (((𝑁 × 𝑂) × {𝑌}) ∈ (𝐵m (𝑁 × 𝑂)) ↔ ((𝑁 × 𝑂) × {𝑌}):(𝑁 × 𝑂)⟶𝐵))
7369, 72mpbird 256 . . . . . . 7 (𝜑 → ((𝑁 × 𝑂) × {𝑌}) ∈ (𝐵m (𝑁 × 𝑂)))
7439, 41ringvcl 22344 . . . . . . 7 ((𝑅 ∈ Ring ∧ ((𝑁 × 𝑂) × {𝑌}) ∈ (𝐵m (𝑁 × 𝑂)) ∧ 𝑍 ∈ (𝐵m (𝑁 × 𝑂))) → (((𝑁 × 𝑂) × {𝑌}) ∘f · 𝑍) ∈ (𝐵m (𝑁 × 𝑂)))
7550, 73, 13, 74syl3anc 1368 . . . . . 6 (𝜑 → (((𝑁 × 𝑂) × {𝑌}) ∘f · 𝑍) ∈ (𝐵m (𝑁 × 𝑂)))
7675adantr 479 . . . . 5 ((𝜑 ∧ (𝑖𝑀𝑘𝑂)) → (((𝑁 × 𝑂) × {𝑌}) ∘f · 𝑍) ∈ (𝐵m (𝑁 × 𝑂)))
77 simprl 769 . . . . 5 ((𝜑 ∧ (𝑖𝑀𝑘𝑂)) → 𝑖𝑀)
78 simprr 771 . . . . 5 ((𝜑 ∧ (𝑖𝑀𝑘𝑂)) → 𝑘𝑂)
7962, 39, 41, 63, 65, 52, 66, 67, 76, 77, 78mamufv 22338 . . . 4 ((𝜑 ∧ (𝑖𝑀𝑘𝑂)) → (𝑖(𝑋𝐹(((𝑁 × 𝑂) × {𝑌}) ∘f · 𝑍))𝑘) = (𝑅 Σg (𝑗𝑁 ↦ ((𝑖𝑋𝑗) · (𝑗(((𝑁 × 𝑂) × {𝑌}) ∘f · 𝑍)𝑘)))))
80 df-ov 7422 . . . . 5 (𝑖(((𝑀 × 𝑂) × {𝑌}) ∘f · (𝑋𝐹𝑍))𝑘) = ((((𝑀 × 𝑂) × {𝑌}) ∘f · (𝑋𝐹𝑍))‘⟨𝑖, 𝑘⟩)
81 opelxpi 5715 . . . . . . 7 ((𝑖𝑀𝑘𝑂) → ⟨𝑖, 𝑘⟩ ∈ (𝑀 × 𝑂))
8281adantl 480 . . . . . 6 ((𝜑 ∧ (𝑖𝑀𝑘𝑂)) → ⟨𝑖, 𝑘⟩ ∈ (𝑀 × 𝑂))
83 xpfi 9343 . . . . . . . . 9 ((𝑀 ∈ Fin ∧ 𝑂 ∈ Fin) → (𝑀 × 𝑂) ∈ Fin)
8464, 7, 83syl2anc 582 . . . . . . . 8 (𝜑 → (𝑀 × 𝑂) ∈ Fin)
8584adantr 479 . . . . . . 7 ((𝜑 ∧ (𝑖𝑀𝑘𝑂)) → (𝑀 × 𝑂) ∈ Fin)
8639, 50, 62, 64, 6, 7, 30, 13mamucl 22345 . . . . . . . . 9 (𝜑 → (𝑋𝐹𝑍) ∈ (𝐵m (𝑀 × 𝑂)))
87 elmapi 8868 . . . . . . . . 9 ((𝑋𝐹𝑍) ∈ (𝐵m (𝑀 × 𝑂)) → (𝑋𝐹𝑍):(𝑀 × 𝑂)⟶𝐵)
88 ffn 6723 . . . . . . . . 9 ((𝑋𝐹𝑍):(𝑀 × 𝑂)⟶𝐵 → (𝑋𝐹𝑍) Fn (𝑀 × 𝑂))
8986, 87, 883syl 18 . . . . . . . 8 (𝜑 → (𝑋𝐹𝑍) Fn (𝑀 × 𝑂))
9089adantr 479 . . . . . . 7 ((𝜑 ∧ (𝑖𝑀𝑘𝑂)) → (𝑋𝐹𝑍) Fn (𝑀 × 𝑂))
91 df-ov 7422 . . . . . . . . 9 (𝑖(𝑋𝐹𝑍)𝑘) = ((𝑋𝐹𝑍)‘⟨𝑖, 𝑘⟩)
9213adantr 479 . . . . . . . . . 10 ((𝜑 ∧ (𝑖𝑀𝑘𝑂)) → 𝑍 ∈ (𝐵m (𝑁 × 𝑂)))
9362, 39, 41, 63, 65, 52, 66, 67, 92, 77, 78mamufv 22338 . . . . . . . . 9 ((𝜑 ∧ (𝑖𝑀𝑘𝑂)) → (𝑖(𝑋𝐹𝑍)𝑘) = (𝑅 Σg (𝑗𝑁 ↦ ((𝑖𝑋𝑗) · (𝑗𝑍𝑘)))))
9491, 93eqtr3id 2779 . . . . . . . 8 ((𝜑 ∧ (𝑖𝑀𝑘𝑂)) → ((𝑋𝐹𝑍)‘⟨𝑖, 𝑘⟩) = (𝑅 Σg (𝑗𝑁 ↦ ((𝑖𝑋𝑗) · (𝑗𝑍𝑘)))))
9594adantr 479 . . . . . . 7 (((𝜑 ∧ (𝑖𝑀𝑘𝑂)) ∧ ⟨𝑖, 𝑘⟩ ∈ (𝑀 × 𝑂)) → ((𝑋𝐹𝑍)‘⟨𝑖, 𝑘⟩) = (𝑅 Σg (𝑗𝑁 ↦ ((𝑖𝑋𝑗) · (𝑗𝑍𝑘)))))
9685, 53, 90, 95ofc1 7712 . . . . . 6 (((𝜑 ∧ (𝑖𝑀𝑘𝑂)) ∧ ⟨𝑖, 𝑘⟩ ∈ (𝑀 × 𝑂)) → ((((𝑀 × 𝑂) × {𝑌}) ∘f · (𝑋𝐹𝑍))‘⟨𝑖, 𝑘⟩) = (𝑌 · (𝑅 Σg (𝑗𝑁 ↦ ((𝑖𝑋𝑗) · (𝑗𝑍𝑘))))))
9782, 96mpdan 685 . . . . 5 ((𝜑 ∧ (𝑖𝑀𝑘𝑂)) → ((((𝑀 × 𝑂) × {𝑌}) ∘f · (𝑋𝐹𝑍))‘⟨𝑖, 𝑘⟩) = (𝑌 · (𝑅 Σg (𝑗𝑁 ↦ ((𝑖𝑋𝑗) · (𝑗𝑍𝑘))))))
9880, 97eqtrid 2777 . . . 4 ((𝜑 ∧ (𝑖𝑀𝑘𝑂)) → (𝑖(((𝑀 × 𝑂) × {𝑌}) ∘f · (𝑋𝐹𝑍))𝑘) = (𝑌 · (𝑅 Σg (𝑗𝑁 ↦ ((𝑖𝑋𝑗) · (𝑗𝑍𝑘))))))
9961, 79, 983eqtr4d 2775 . . 3 ((𝜑 ∧ (𝑖𝑀𝑘𝑂)) → (𝑖(𝑋𝐹(((𝑁 × 𝑂) × {𝑌}) ∘f · 𝑍))𝑘) = (𝑖(((𝑀 × 𝑂) × {𝑌}) ∘f · (𝑋𝐹𝑍))𝑘))
10099ralrimivva 3190 . 2 (𝜑 → ∀𝑖𝑀𝑘𝑂 (𝑖(𝑋𝐹(((𝑁 × 𝑂) × {𝑌}) ∘f · 𝑍))𝑘) = (𝑖(((𝑀 × 𝑂) × {𝑌}) ∘f · (𝑋𝐹𝑍))𝑘))
10139, 50, 62, 64, 6, 7, 30, 75mamucl 22345 . . . 4 (𝜑 → (𝑋𝐹(((𝑁 × 𝑂) × {𝑌}) ∘f · 𝑍)) ∈ (𝐵m (𝑀 × 𝑂)))
102 elmapi 8868 . . . 4 ((𝑋𝐹(((𝑁 × 𝑂) × {𝑌}) ∘f · 𝑍)) ∈ (𝐵m (𝑀 × 𝑂)) → (𝑋𝐹(((𝑁 × 𝑂) × {𝑌}) ∘f · 𝑍)):(𝑀 × 𝑂)⟶𝐵)
103 ffn 6723 . . . 4 ((𝑋𝐹(((𝑁 × 𝑂) × {𝑌}) ∘f · 𝑍)):(𝑀 × 𝑂)⟶𝐵 → (𝑋𝐹(((𝑁 × 𝑂) × {𝑌}) ∘f · 𝑍)) Fn (𝑀 × 𝑂))
104101, 102, 1033syl 18 . . 3 (𝜑 → (𝑋𝐹(((𝑁 × 𝑂) × {𝑌}) ∘f · 𝑍)) Fn (𝑀 × 𝑂))
105 fconst6g 6786 . . . . . . 7 (𝑌𝐵 → ((𝑀 × 𝑂) × {𝑌}):(𝑀 × 𝑂)⟶𝐵)
10611, 105syl 17 . . . . . 6 (𝜑 → ((𝑀 × 𝑂) × {𝑌}):(𝑀 × 𝑂)⟶𝐵)
107 elmapg 8858 . . . . . . 7 ((𝐵 ∈ V ∧ (𝑀 × 𝑂) ∈ Fin) → (((𝑀 × 𝑂) × {𝑌}) ∈ (𝐵m (𝑀 × 𝑂)) ↔ ((𝑀 × 𝑂) × {𝑌}):(𝑀 × 𝑂)⟶𝐵))
10870, 84, 107sylancr 585 . . . . . 6 (𝜑 → (((𝑀 × 𝑂) × {𝑌}) ∈ (𝐵m (𝑀 × 𝑂)) ↔ ((𝑀 × 𝑂) × {𝑌}):(𝑀 × 𝑂)⟶𝐵))
109106, 108mpbird 256 . . . . 5 (𝜑 → ((𝑀 × 𝑂) × {𝑌}) ∈ (𝐵m (𝑀 × 𝑂)))
11039, 41ringvcl 22344 . . . . 5 ((𝑅 ∈ Ring ∧ ((𝑀 × 𝑂) × {𝑌}) ∈ (𝐵m (𝑀 × 𝑂)) ∧ (𝑋𝐹𝑍) ∈ (𝐵m (𝑀 × 𝑂))) → (((𝑀 × 𝑂) × {𝑌}) ∘f · (𝑋𝐹𝑍)) ∈ (𝐵m (𝑀 × 𝑂)))
11150, 109, 86, 110syl3anc 1368 . . . 4 (𝜑 → (((𝑀 × 𝑂) × {𝑌}) ∘f · (𝑋𝐹𝑍)) ∈ (𝐵m (𝑀 × 𝑂)))
112 elmapi 8868 . . . 4 ((((𝑀 × 𝑂) × {𝑌}) ∘f · (𝑋𝐹𝑍)) ∈ (𝐵m (𝑀 × 𝑂)) → (((𝑀 × 𝑂) × {𝑌}) ∘f · (𝑋𝐹𝑍)):(𝑀 × 𝑂)⟶𝐵)
113 ffn 6723 . . . 4 ((((𝑀 × 𝑂) × {𝑌}) ∘f · (𝑋𝐹𝑍)):(𝑀 × 𝑂)⟶𝐵 → (((𝑀 × 𝑂) × {𝑌}) ∘f · (𝑋𝐹𝑍)) Fn (𝑀 × 𝑂))
114111, 112, 1133syl 18 . . 3 (𝜑 → (((𝑀 × 𝑂) × {𝑌}) ∘f · (𝑋𝐹𝑍)) Fn (𝑀 × 𝑂))
115 eqfnov2 7551 . . 3 (((𝑋𝐹(((𝑁 × 𝑂) × {𝑌}) ∘f · 𝑍)) Fn (𝑀 × 𝑂) ∧ (((𝑀 × 𝑂) × {𝑌}) ∘f · (𝑋𝐹𝑍)) Fn (𝑀 × 𝑂)) → ((𝑋𝐹(((𝑁 × 𝑂) × {𝑌}) ∘f · 𝑍)) = (((𝑀 × 𝑂) × {𝑌}) ∘f · (𝑋𝐹𝑍)) ↔ ∀𝑖𝑀𝑘𝑂 (𝑖(𝑋𝐹(((𝑁 × 𝑂) × {𝑌}) ∘f · 𝑍))𝑘) = (𝑖(((𝑀 × 𝑂) × {𝑌}) ∘f · (𝑋𝐹𝑍))𝑘)))
116104, 114, 115syl2anc 582 . 2 (𝜑 → ((𝑋𝐹(((𝑁 × 𝑂) × {𝑌}) ∘f · 𝑍)) = (((𝑀 × 𝑂) × {𝑌}) ∘f · (𝑋𝐹𝑍)) ↔ ∀𝑖𝑀𝑘𝑂 (𝑖(𝑋𝐹(((𝑁 × 𝑂) × {𝑌}) ∘f · 𝑍))𝑘) = (𝑖(((𝑀 × 𝑂) × {𝑌}) ∘f · (𝑋𝐹𝑍))𝑘)))
117100, 116mpbird 256 1 (𝜑 → (𝑋𝐹(((𝑁 × 𝑂) × {𝑌}) ∘f · 𝑍)) = (((𝑀 × 𝑂) × {𝑌}) ∘f · (𝑋𝐹𝑍)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394   = wceq 1533  wcel 2098  wral 3050  Vcvv 3461  {csn 4630  cop 4636  cotp 4638  cmpt 5232   × cxp 5676   Fn wfn 6544  wf 6545  cfv 6549  (class class class)co 7419  f cof 7683  m cmap 8845  Fincfn 8964  Basecbs 17183  .rcmulr 17237  0gc0g 17424   Σg cgsu 17425  CMndccmn 19747  mulGrpcmgp 20086  Ringcrg 20185  CRingccrg 20186   maMul cmmul 22334
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-cnex 11196  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-mulcom 11204  ax-addass 11205  ax-mulass 11206  ax-distr 11207  ax-i2m1 11208  ax-1ne0 11209  ax-1rid 11210  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213  ax-pre-lttri 11214  ax-pre-lttrn 11215  ax-pre-ltadd 11216  ax-pre-mulgt0 11217
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-ot 4639  df-uni 4910  df-int 4951  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-se 5634  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-isom 6558  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-of 7685  df-om 7872  df-1st 7994  df-2nd 7995  df-supp 8166  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-er 8725  df-map 8847  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-fsupp 9388  df-oi 9535  df-card 9964  df-pnf 11282  df-mnf 11283  df-xr 11284  df-ltxr 11285  df-le 11286  df-sub 11478  df-neg 11479  df-nn 12246  df-2 12308  df-n0 12506  df-z 12592  df-uz 12856  df-fz 13520  df-fzo 13663  df-seq 14003  df-hash 14326  df-sets 17136  df-slot 17154  df-ndx 17166  df-base 17184  df-plusg 17249  df-0g 17426  df-gsum 17427  df-mgm 18603  df-sgrp 18682  df-mnd 18698  df-mhm 18743  df-grp 18901  df-minusg 18902  df-ghm 19176  df-cntz 19280  df-cmn 19749  df-abl 19750  df-mgp 20087  df-ur 20134  df-ring 20187  df-cring 20188  df-mamu 22335
This theorem is referenced by:  matassa  22390
  Copyright terms: Public domain W3C validator