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

Theorem mdetunilem3 20614
Description: Lemma for mdetuni 20622. (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 1248 . 2 (((𝜑𝐸𝐵𝐹𝐵) ∧ (𝐺𝐵𝐻𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝐻} × 𝑁)))) ∧ ((𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝐻} × 𝑁))))
2 simp3l 1241 . 2 (((𝜑𝐸𝐵𝐹𝐵) ∧ (𝐺𝐵𝐻𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝐻} × 𝑁)))) ∧ ((𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))
3 simp3r 1242 . 2 (((𝜑𝐸𝐵𝐹𝐵) ∧ (𝐺𝐵𝐻𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝐻} × 𝑁)))) ∧ ((𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))
4 simprl 811 . . . . 5 (((𝜑𝐸𝐵𝐹𝐵) ∧ (𝐺𝐵𝐻𝑁)) → 𝐺𝐵)
5 simprr 813 . . . . 5 (((𝜑𝐸𝐵𝐹𝐵) ∧ (𝐺𝐵𝐻𝑁)) → 𝐻𝑁)
6 simpl2 1227 . . . . . 6 (((𝜑𝐸𝐵𝐹𝐵) ∧ (𝐺𝐵𝐻𝑁)) → 𝐸𝐵)
7 simpl3 1229 . . . . . 6 (((𝜑𝐸𝐵𝐹𝐵) ∧ (𝐺𝐵𝐻𝑁)) → 𝐹𝐵)
8 simpl1 1225 . . . . . . 7 (((𝜑𝐸𝐵𝐹𝐵) ∧ (𝐺𝐵𝐻𝑁)) → 𝜑)
9 mdetuni.li . . . . . . 7 (𝜑 → ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑤𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = ((𝐷𝑦) + (𝐷𝑧))))
108, 9syl 17 . . . . . 6 (((𝜑𝐸𝐵𝐹𝐵) ∧ (𝐺𝐵𝐻𝑁)) → ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑤𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = ((𝐷𝑦) + (𝐷𝑧))))
11 reseq1 5537 . . . . . . . . . . 11 (𝑥 = 𝐸 → (𝑥 ↾ ({𝑤} × 𝑁)) = (𝐸 ↾ ({𝑤} × 𝑁)))
1211eqeq1d 2754 . . . . . . . . . 10 (𝑥 = 𝐸 → ((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ↔ (𝐸 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁)))))
13 reseq1 5537 . . . . . . . . . . 11 (𝑥 = 𝐸 → (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))
1413eqeq1d 2754 . . . . . . . . . 10 (𝑥 = 𝐸 → ((𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ↔ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))))
1513eqeq1d 2754 . . . . . . . . . 10 (𝑥 = 𝐸 → ((𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ↔ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))))
1612, 14, 153anbi123d 1540 . . . . . . . . 9 (𝑥 = 𝐸 → (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) ↔ ((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))))
17 fveq2 6344 . . . . . . . . . 10 (𝑥 = 𝐸 → (𝐷𝑥) = (𝐷𝐸))
1817eqeq1d 2754 . . . . . . . . 9 (𝑥 = 𝐸 → ((𝐷𝑥) = ((𝐷𝑦) + (𝐷𝑧)) ↔ (𝐷𝐸) = ((𝐷𝑦) + (𝐷𝑧))))
1916, 18imbi12d 333 . . . . . . . 8 (𝑥 = 𝐸 → ((((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = ((𝐷𝑦) + (𝐷𝑧))) ↔ (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = ((𝐷𝑦) + (𝐷𝑧)))))
20192ralbidv 3119 . . . . . . 7 (𝑥 = 𝐸 → (∀𝑧𝐵𝑤𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = ((𝐷𝑦) + (𝐷𝑧))) ↔ ∀𝑧𝐵𝑤𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = ((𝐷𝑦) + (𝐷𝑧)))))
21 reseq1 5537 . . . . . . . . . . . 12 (𝑦 = 𝐹 → (𝑦 ↾ ({𝑤} × 𝑁)) = (𝐹 ↾ ({𝑤} × 𝑁)))
2221oveq1d 6820 . . . . . . . . . . 11 (𝑦 = 𝐹 → ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))))
2322eqeq2d 2762 . . . . . . . . . 10 (𝑦 = 𝐹 → ((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ↔ (𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁)))))
24 reseq1 5537 . . . . . . . . . . 11 (𝑦 = 𝐹 → (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))
2524eqeq2d 2762 . . . . . . . . . 10 (𝑦 = 𝐹 → ((𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ↔ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))))
2623, 253anbi12d 1541 . . . . . . . . 9 (𝑦 = 𝐹 → (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) ↔ ((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))))
27 fveq2 6344 . . . . . . . . . . 11 (𝑦 = 𝐹 → (𝐷𝑦) = (𝐷𝐹))
2827oveq1d 6820 . . . . . . . . . 10 (𝑦 = 𝐹 → ((𝐷𝑦) + (𝐷𝑧)) = ((𝐷𝐹) + (𝐷𝑧)))
2928eqeq2d 2762 . . . . . . . . 9 (𝑦 = 𝐹 → ((𝐷𝐸) = ((𝐷𝑦) + (𝐷𝑧)) ↔ (𝐷𝐸) = ((𝐷𝐹) + (𝐷𝑧))))
3026, 29imbi12d 333 . . . . . . . 8 (𝑦 = 𝐹 → ((((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = ((𝐷𝑦) + (𝐷𝑧))) ↔ (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = ((𝐷𝐹) + (𝐷𝑧)))))
31302ralbidv 3119 . . . . . . 7 (𝑦 = 𝐹 → (∀𝑧𝐵𝑤𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = ((𝐷𝑦) + (𝐷𝑧))) ↔ ∀𝑧𝐵𝑤𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = ((𝐷𝐹) + (𝐷𝑧)))))
3220, 31rspc2va 3454 . . . . . 6 (((𝐸𝐵𝐹𝐵) ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑤𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = ((𝐷𝑦) + (𝐷𝑧)))) → ∀𝑧𝐵𝑤𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = ((𝐷𝐹) + (𝐷𝑧))))
336, 7, 10, 32syl21anc 1472 . . . . 5 (((𝜑𝐸𝐵𝐹𝐵) ∧ (𝐺𝐵𝐻𝑁)) → ∀𝑧𝐵𝑤𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = ((𝐷𝐹) + (𝐷𝑧))))
34 reseq1 5537 . . . . . . . . . 10 (𝑧 = 𝐺 → (𝑧 ↾ ({𝑤} × 𝑁)) = (𝐺 ↾ ({𝑤} × 𝑁)))
3534oveq2d 6821 . . . . . . . . 9 (𝑧 = 𝐺 → ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝑤} × 𝑁))))
3635eqeq2d 2762 . . . . . . . 8 (𝑧 = 𝐺 → ((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ↔ (𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝑤} × 𝑁)))))
37 reseq1 5537 . . . . . . . . 9 (𝑧 = 𝐺 → (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))
3837eqeq2d 2762 . . . . . . . 8 (𝑧 = 𝐺 → ((𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ↔ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))))
3936, 383anbi13d 1542 . . . . . . 7 (𝑧 = 𝐺 → (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) ↔ ((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))))
40 fveq2 6344 . . . . . . . . 9 (𝑧 = 𝐺 → (𝐷𝑧) = (𝐷𝐺))
4140oveq2d 6821 . . . . . . . 8 (𝑧 = 𝐺 → ((𝐷𝐹) + (𝐷𝑧)) = ((𝐷𝐹) + (𝐷𝐺)))
4241eqeq2d 2762 . . . . . . 7 (𝑧 = 𝐺 → ((𝐷𝐸) = ((𝐷𝐹) + (𝐷𝑧)) ↔ (𝐷𝐸) = ((𝐷𝐹) + (𝐷𝐺))))
4339, 42imbi12d 333 . . . . . 6 (𝑧 = 𝐺 → ((((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = ((𝐷𝐹) + (𝐷𝑧))) ↔ (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = ((𝐷𝐹) + (𝐷𝐺)))))
44 sneq 4323 . . . . . . . . . . 11 (𝑤 = 𝐻 → {𝑤} = {𝐻})
4544xpeq1d 5287 . . . . . . . . . 10 (𝑤 = 𝐻 → ({𝑤} × 𝑁) = ({𝐻} × 𝑁))
4645reseq2d 5543 . . . . . . . . 9 (𝑤 = 𝐻 → (𝐸 ↾ ({𝑤} × 𝑁)) = (𝐸 ↾ ({𝐻} × 𝑁)))
4745reseq2d 5543 . . . . . . . . . 10 (𝑤 = 𝐻 → (𝐹 ↾ ({𝑤} × 𝑁)) = (𝐹 ↾ ({𝐻} × 𝑁)))
4845reseq2d 5543 . . . . . . . . . 10 (𝑤 = 𝐻 → (𝐺 ↾ ({𝑤} × 𝑁)) = (𝐺 ↾ ({𝐻} × 𝑁)))
4947, 48oveq12d 6823 . . . . . . . . 9 (𝑤 = 𝐻 → ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝑤} × 𝑁))) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝐻} × 𝑁))))
5046, 49eqeq12d 2767 . . . . . . . 8 (𝑤 = 𝐻 → ((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝑤} × 𝑁))) ↔ (𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝐻} × 𝑁)))))
5144difeq2d 3863 . . . . . . . . . . 11 (𝑤 = 𝐻 → (𝑁 ∖ {𝑤}) = (𝑁 ∖ {𝐻}))
5251xpeq1d 5287 . . . . . . . . . 10 (𝑤 = 𝐻 → ((𝑁 ∖ {𝑤}) × 𝑁) = ((𝑁 ∖ {𝐻}) × 𝑁))
5352reseq2d 5543 . . . . . . . . 9 (𝑤 = 𝐻 → (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))
5452reseq2d 5543 . . . . . . . . 9 (𝑤 = 𝐻 → (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))
5553, 54eqeq12d 2767 . . . . . . . 8 (𝑤 = 𝐻 → ((𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ↔ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))))
5652reseq2d 5543 . . . . . . . . 9 (𝑤 = 𝐻 → (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))
5753, 56eqeq12d 2767 . . . . . . . 8 (𝑤 = 𝐻 → ((𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ↔ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))))
5850, 55, 573anbi123d 1540 . . . . . . 7 (𝑤 = 𝐻 → (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) ↔ ((𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))))
5958imbi1d 330 . . . . . 6 (𝑤 = 𝐻 → ((((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = ((𝐷𝐹) + (𝐷𝐺))) ↔ (((𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → (𝐷𝐸) = ((𝐷𝐹) + (𝐷𝐺)))))
6043, 59rspc2va 3454 . . . . 5 (((𝐺𝐵𝐻𝑁) ∧ ∀𝑧𝐵𝑤𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘𝑓 + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = ((𝐷𝐹) + (𝐷𝑧)))) → (((𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → (𝐷𝐸) = ((𝐷𝐹) + (𝐷𝐺))))
614, 5, 33, 60syl21anc 1472 . . . 4 (((𝜑𝐸𝐵𝐹𝐵) ∧ (𝐺𝐵𝐻𝑁)) → (((𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → (𝐷𝐸) = ((𝐷𝐹) + (𝐷𝐺))))
62613adantr3 1174 . . 3 (((𝜑𝐸𝐵𝐹𝐵) ∧ (𝐺𝐵𝐻𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝐻} × 𝑁))))) → (((𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → (𝐷𝐸) = ((𝐷𝐹) + (𝐷𝐺))))
63623adant3 1126 . 2 (((𝜑𝐸𝐵𝐹𝐵) ∧ (𝐺𝐵𝐻𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝐻} × 𝑁)))) ∧ ((𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (((𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → (𝐷𝐸) = ((𝐷𝐹) + (𝐷𝐺))))
641, 2, 3, 63mp3and 1568 1 (((𝜑𝐸𝐵𝐹𝐵) ∧ (𝐺𝐵𝐻𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘𝑓 + (𝐺 ↾ ({𝐻} × 𝑁)))) ∧ ((𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (𝐷𝐸) = ((𝐷𝐹) + (𝐷𝐺)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072   = wceq 1624  wcel 2131  wne 2924  wral 3042  cdif 3704  {csn 4313   × cxp 5256  cres 5260  wf 6037  cfv 6041  (class class class)co 6805  𝑓 cof 7052  Fincfn 8113  Basecbs 16051  +gcplusg 16135  .rcmulr 16136  0gc0g 16294  1rcur 18693  Ringcrg 18739   Mat cmat 20407
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ral 3047  df-rex 3048  df-rab 3051  df-v 3334  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-sn 4314  df-pr 4316  df-op 4320  df-uni 4581  df-br 4797  df-opab 4857  df-xp 5264  df-res 5270  df-iota 6004  df-fv 6049  df-ov 6808
This theorem is referenced by:  mdetunilem5  20616  mdetuni0  20621
  Copyright terms: Public domain W3C validator