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

Theorem mdetunilem3 20627
Description: Lemma for mdetuni 20635. (Contributed by SO, 15-Jul-2018.)
Hypotheses
Ref Expression
mdetuni.a 𝐴 = (𝑁 Mat 𝑅)
mdetuni.b 𝐵 = (Base‘𝐴)
mdetuni.k 𝐾 = (Base‘𝑅)
mdetuni.0g 0 = (0g𝑅)
mdetuni.1r 1 = (1r𝑅)
mdetuni.pg + = (+g𝑅)
mdetuni.tg · = (.r𝑅)
mdetuni.n (𝜑𝑁 ∈ Fin)
mdetuni.r (𝜑𝑅 ∈ Ring)
mdetuni.ff (𝜑𝐷:𝐵𝐾)
mdetuni.al (𝜑 → ∀𝑥𝐵𝑦𝑁𝑧𝑁 ((𝑦𝑧 ∧ ∀𝑤𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷𝑥) = 0 ))
mdetuni.li (𝜑 → ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑤𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = ((𝐷𝑦) + (𝐷𝑧))))
mdetuni.sc (𝜑 → ∀𝑥𝐵𝑦𝐾𝑧𝐵𝑤𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = (𝑦 · (𝐷𝑧))))
Assertion
Ref Expression
mdetunilem3 (((𝜑𝐸𝐵𝐹𝐵) ∧ (𝐺𝐵𝐻𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝐻} × 𝑁)))) ∧ ((𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (𝐷𝐸) = ((𝐷𝐹) + (𝐷𝐺)))
Distinct variable groups:   𝜑,𝑥,𝑦,𝑧,𝑤   𝑥,𝐵,𝑦,𝑧,𝑤   𝑥,𝐾,𝑦,𝑧,𝑤   𝑥,𝑁,𝑦,𝑧,𝑤   𝑥,𝐷,𝑦,𝑧,𝑤   𝑥, · ,𝑦,𝑧,𝑤   𝑥, + ,𝑦,𝑧,𝑤   𝑥, 0 ,𝑦,𝑧,𝑤   𝑥, 1 ,𝑦,𝑧,𝑤   𝑥,𝑅,𝑦,𝑧,𝑤   𝑥,𝐴,𝑦,𝑧,𝑤   𝑥,𝐸,𝑦,𝑧,𝑤   𝑥,𝐹,𝑦,𝑧,𝑤   𝑥,𝐺,𝑦,𝑧,𝑤   𝑥,𝐻,𝑦,𝑧,𝑤

Proof of Theorem mdetunilem3
StepHypRef Expression
1 simp23 1258 . 2 (((𝜑𝐸𝐵𝐹𝐵) ∧ (𝐺𝐵𝐻𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝐻} × 𝑁)))) ∧ ((𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝐻} × 𝑁))))
2 simp3l 1251 . 2 (((𝜑𝐸𝐵𝐹𝐵) ∧ (𝐺𝐵𝐻𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝐻} × 𝑁)))) ∧ ((𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))
3 simp3r 1252 . 2 (((𝜑𝐸𝐵𝐹𝐵) ∧ (𝐺𝐵𝐻𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝐻} × 𝑁)))) ∧ ((𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))
4 simprl 778 . . . . 5 (((𝜑𝐸𝐵𝐹𝐵) ∧ (𝐺𝐵𝐻𝑁)) → 𝐺𝐵)
5 simprr 780 . . . . 5 (((𝜑𝐸𝐵𝐹𝐵) ∧ (𝐺𝐵𝐻𝑁)) → 𝐻𝑁)
6 simpl2 1237 . . . . . 6 (((𝜑𝐸𝐵𝐹𝐵) ∧ (𝐺𝐵𝐻𝑁)) → 𝐸𝐵)
7 simpl3 1239 . . . . . 6 (((𝜑𝐸𝐵𝐹𝐵) ∧ (𝐺𝐵𝐻𝑁)) → 𝐹𝐵)
8 simpl1 1235 . . . . . . 7 (((𝜑𝐸𝐵𝐹𝐵) ∧ (𝐺𝐵𝐻𝑁)) → 𝜑)
9 mdetuni.li . . . . . . 7 (𝜑 → ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑤𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = ((𝐷𝑦) + (𝐷𝑧))))
108, 9syl 17 . . . . . 6 (((𝜑𝐸𝐵𝐹𝐵) ∧ (𝐺𝐵𝐻𝑁)) → ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑤𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = ((𝐷𝑦) + (𝐷𝑧))))
11 reseq1 5591 . . . . . . . . . . 11 (𝑥 = 𝐸 → (𝑥 ↾ ({𝑤} × 𝑁)) = (𝐸 ↾ ({𝑤} × 𝑁)))
1211eqeq1d 2808 . . . . . . . . . 10 (𝑥 = 𝐸 → ((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ↔ (𝐸 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁)))))
13 reseq1 5591 . . . . . . . . . . 11 (𝑥 = 𝐸 → (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))
1413eqeq1d 2808 . . . . . . . . . 10 (𝑥 = 𝐸 → ((𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ↔ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))))
1513eqeq1d 2808 . . . . . . . . . 10 (𝑥 = 𝐸 → ((𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ↔ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))))
1612, 14, 153anbi123d 1553 . . . . . . . . 9 (𝑥 = 𝐸 → (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) ↔ ((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))))
17 fveq2 6404 . . . . . . . . . 10 (𝑥 = 𝐸 → (𝐷𝑥) = (𝐷𝐸))
1817eqeq1d 2808 . . . . . . . . 9 (𝑥 = 𝐸 → ((𝐷𝑥) = ((𝐷𝑦) + (𝐷𝑧)) ↔ (𝐷𝐸) = ((𝐷𝑦) + (𝐷𝑧))))
1916, 18imbi12d 335 . . . . . . . 8 (𝑥 = 𝐸 → ((((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = ((𝐷𝑦) + (𝐷𝑧))) ↔ (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = ((𝐷𝑦) + (𝐷𝑧)))))
20192ralbidv 3177 . . . . . . 7 (𝑥 = 𝐸 → (∀𝑧𝐵𝑤𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = ((𝐷𝑦) + (𝐷𝑧))) ↔ ∀𝑧𝐵𝑤𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = ((𝐷𝑦) + (𝐷𝑧)))))
21 reseq1 5591 . . . . . . . . . . . 12 (𝑦 = 𝐹 → (𝑦 ↾ ({𝑤} × 𝑁)) = (𝐹 ↾ ({𝑤} × 𝑁)))
2221oveq1d 6885 . . . . . . . . . . 11 (𝑦 = 𝐹 → ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))))
2322eqeq2d 2816 . . . . . . . . . 10 (𝑦 = 𝐹 → ((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ↔ (𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁)))))
24 reseq1 5591 . . . . . . . . . . 11 (𝑦 = 𝐹 → (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))
2524eqeq2d 2816 . . . . . . . . . 10 (𝑦 = 𝐹 → ((𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ↔ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))))
2623, 253anbi12d 1554 . . . . . . . . 9 (𝑦 = 𝐹 → (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) ↔ ((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))))
27 fveq2 6404 . . . . . . . . . . 11 (𝑦 = 𝐹 → (𝐷𝑦) = (𝐷𝐹))
2827oveq1d 6885 . . . . . . . . . 10 (𝑦 = 𝐹 → ((𝐷𝑦) + (𝐷𝑧)) = ((𝐷𝐹) + (𝐷𝑧)))
2928eqeq2d 2816 . . . . . . . . 9 (𝑦 = 𝐹 → ((𝐷𝐸) = ((𝐷𝑦) + (𝐷𝑧)) ↔ (𝐷𝐸) = ((𝐷𝐹) + (𝐷𝑧))))
3026, 29imbi12d 335 . . . . . . . 8 (𝑦 = 𝐹 → ((((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = ((𝐷𝑦) + (𝐷𝑧))) ↔ (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = ((𝐷𝐹) + (𝐷𝑧)))))
31302ralbidv 3177 . . . . . . 7 (𝑦 = 𝐹 → (∀𝑧𝐵𝑤𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = ((𝐷𝑦) + (𝐷𝑧))) ↔ ∀𝑧𝐵𝑤𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = ((𝐷𝐹) + (𝐷𝑧)))))
3220, 31rspc2va 3516 . . . . . 6 (((𝐸𝐵𝐹𝐵) ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑤𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = ((𝐷𝑦) + (𝐷𝑧)))) → ∀𝑧𝐵𝑤𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = ((𝐷𝐹) + (𝐷𝑧))))
336, 7, 10, 32syl21anc 857 . . . . 5 (((𝜑𝐸𝐵𝐹𝐵) ∧ (𝐺𝐵𝐻𝑁)) → ∀𝑧𝐵𝑤𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = ((𝐷𝐹) + (𝐷𝑧))))
34 reseq1 5591 . . . . . . . . . 10 (𝑧 = 𝐺 → (𝑧 ↾ ({𝑤} × 𝑁)) = (𝐺 ↾ ({𝑤} × 𝑁)))
3534oveq2d 6886 . . . . . . . . 9 (𝑧 = 𝐺 → ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝑤} × 𝑁))))
3635eqeq2d 2816 . . . . . . . 8 (𝑧 = 𝐺 → ((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ↔ (𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝑤} × 𝑁)))))
37 reseq1 5591 . . . . . . . . 9 (𝑧 = 𝐺 → (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))
3837eqeq2d 2816 . . . . . . . 8 (𝑧 = 𝐺 → ((𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ↔ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))))
3936, 383anbi13d 1555 . . . . . . 7 (𝑧 = 𝐺 → (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) ↔ ((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))))
40 fveq2 6404 . . . . . . . . 9 (𝑧 = 𝐺 → (𝐷𝑧) = (𝐷𝐺))
4140oveq2d 6886 . . . . . . . 8 (𝑧 = 𝐺 → ((𝐷𝐹) + (𝐷𝑧)) = ((𝐷𝐹) + (𝐷𝐺)))
4241eqeq2d 2816 . . . . . . 7 (𝑧 = 𝐺 → ((𝐷𝐸) = ((𝐷𝐹) + (𝐷𝑧)) ↔ (𝐷𝐸) = ((𝐷𝐹) + (𝐷𝐺))))
4339, 42imbi12d 335 . . . . . 6 (𝑧 = 𝐺 → ((((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = ((𝐷𝐹) + (𝐷𝑧))) ↔ (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = ((𝐷𝐹) + (𝐷𝐺)))))
44 sneq 4380 . . . . . . . . . . 11 (𝑤 = 𝐻 → {𝑤} = {𝐻})
4544xpeq1d 5339 . . . . . . . . . 10 (𝑤 = 𝐻 → ({𝑤} × 𝑁) = ({𝐻} × 𝑁))
4645reseq2d 5597 . . . . . . . . 9 (𝑤 = 𝐻 → (𝐸 ↾ ({𝑤} × 𝑁)) = (𝐸 ↾ ({𝐻} × 𝑁)))
4745reseq2d 5597 . . . . . . . . . 10 (𝑤 = 𝐻 → (𝐹 ↾ ({𝑤} × 𝑁)) = (𝐹 ↾ ({𝐻} × 𝑁)))
4845reseq2d 5597 . . . . . . . . . 10 (𝑤 = 𝐻 → (𝐺 ↾ ({𝑤} × 𝑁)) = (𝐺 ↾ ({𝐻} × 𝑁)))
4947, 48oveq12d 6888 . . . . . . . . 9 (𝑤 = 𝐻 → ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝑤} × 𝑁))) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝐻} × 𝑁))))
5046, 49eqeq12d 2821 . . . . . . . 8 (𝑤 = 𝐻 → ((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝑤} × 𝑁))) ↔ (𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝐻} × 𝑁)))))
5144difeq2d 3927 . . . . . . . . . . 11 (𝑤 = 𝐻 → (𝑁 ∖ {𝑤}) = (𝑁 ∖ {𝐻}))
5251xpeq1d 5339 . . . . . . . . . 10 (𝑤 = 𝐻 → ((𝑁 ∖ {𝑤}) × 𝑁) = ((𝑁 ∖ {𝐻}) × 𝑁))
5352reseq2d 5597 . . . . . . . . 9 (𝑤 = 𝐻 → (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))
5452reseq2d 5597 . . . . . . . . 9 (𝑤 = 𝐻 → (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))
5553, 54eqeq12d 2821 . . . . . . . 8 (𝑤 = 𝐻 → ((𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ↔ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))))
5652reseq2d 5597 . . . . . . . . 9 (𝑤 = 𝐻 → (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))
5753, 56eqeq12d 2821 . . . . . . . 8 (𝑤 = 𝐻 → ((𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ↔ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))))
5850, 55, 573anbi123d 1553 . . . . . . 7 (𝑤 = 𝐻 → (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) ↔ ((𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))))
5958imbi1d 332 . . . . . 6 (𝑤 = 𝐻 → ((((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = ((𝐷𝐹) + (𝐷𝐺))) ↔ (((𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → (𝐷𝐸) = ((𝐷𝐹) + (𝐷𝐺)))))
6043, 59rspc2va 3516 . . . . 5 (((𝐺𝐵𝐻𝑁) ∧ ∀𝑧𝐵𝑤𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = ((𝐷𝐹) + (𝐷𝑧)))) → (((𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → (𝐷𝐸) = ((𝐷𝐹) + (𝐷𝐺))))
614, 5, 33, 60syl21anc 857 . . . 4 (((𝜑𝐸𝐵𝐹𝐵) ∧ (𝐺𝐵𝐻𝑁)) → (((𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → (𝐷𝐸) = ((𝐷𝐹) + (𝐷𝐺))))
62613adantr3 1205 . . 3 (((𝜑𝐸𝐵𝐹𝐵) ∧ (𝐺𝐵𝐻𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝐻} × 𝑁))))) → (((𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → (𝐷𝐸) = ((𝐷𝐹) + (𝐷𝐺))))
63623adant3 1155 . 2 (((𝜑𝐸𝐵𝐹𝐵) ∧ (𝐺𝐵𝐻𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝐻} × 𝑁)))) ∧ ((𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (((𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → (𝐷𝐸) = ((𝐷𝐹) + (𝐷𝐺))))
641, 2, 3, 63mp3and 1581 1 (((𝜑𝐸𝐵𝐹𝐵) ∧ (𝐺𝐵𝐻𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝐻} × 𝑁)))) ∧ ((𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (𝐷𝐸) = ((𝐷𝐹) + (𝐷𝐺)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100   = wceq 1637  wcel 2156  wne 2978  wral 3096  cdif 3766  {csn 4370   × cxp 5309  cres 5313  wf 6093  cfv 6097  (class class class)co 6870  𝑓 cof 7121  Fincfn 8188  Basecbs 16064  +gcplusg 16149  .rcmulr 16150  0gc0g 16301  1rcur 18699  Ringcrg 18745   Mat cmat 20419
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-br 4845  df-opab 4907  df-xp 5317  df-res 5323  df-iota 6060  df-fv 6105  df-ov 6873
This theorem is referenced by:  mdetunilem5  20629  mdetuni0  20634
  Copyright terms: Public domain W3C validator