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

Theorem mdetunilem4 20340
Description: Lemma for mdetuni 20347. (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
mdetunilem4 ((𝜑 ∧ (𝐸𝐵𝐹𝐾𝐺𝐵) ∧ (𝐻𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (𝐷𝐸) = (𝐹 · (𝐷𝐺)))
Distinct variable groups:   𝜑,𝑥,𝑦,𝑧,𝑤   𝑥,𝐵,𝑦,𝑧,𝑤   𝑥,𝐾,𝑦,𝑧,𝑤   𝑥,𝑁,𝑦,𝑧,𝑤   𝑥,𝐷,𝑦,𝑧,𝑤   𝑥, · ,𝑦,𝑧,𝑤   𝑥, + ,𝑦,𝑧,𝑤   𝑥, 0 ,𝑦,𝑧,𝑤   𝑥, 1 ,𝑦,𝑧,𝑤   𝑥,𝑅,𝑦,𝑧,𝑤   𝑥,𝐴,𝑦,𝑧,𝑤   𝑥,𝐸,𝑦,𝑧,𝑤   𝑥,𝐹,𝑦,𝑧,𝑤   𝑥,𝐺,𝑦,𝑧,𝑤   𝑥,𝐻,𝑦,𝑧,𝑤

Proof of Theorem mdetunilem4
StepHypRef Expression
1 simp32 1096 . 2 ((𝜑 ∧ (𝐸𝐵𝐹𝐾𝐺𝐵) ∧ (𝐻𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))))
2 simp33 1097 . 2 ((𝜑 ∧ (𝐸𝐵𝐹𝐾𝐺𝐵) ∧ (𝐻𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))
3 simp1 1059 . . 3 ((𝐻𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → 𝐻𝑁)
4 simp23 1094 . . . 4 ((𝜑 ∧ (𝐸𝐵𝐹𝐾𝐺𝐵) ∧ 𝐻𝑁) → 𝐺𝐵)
5 simp3 1061 . . . 4 ((𝜑 ∧ (𝐸𝐵𝐹𝐾𝐺𝐵) ∧ 𝐻𝑁) → 𝐻𝑁)
6 simp21 1092 . . . . 5 ((𝜑 ∧ (𝐸𝐵𝐹𝐾𝐺𝐵) ∧ 𝐻𝑁) → 𝐸𝐵)
7 simp22 1093 . . . . 5 ((𝜑 ∧ (𝐸𝐵𝐹𝐾𝐺𝐵) ∧ 𝐻𝑁) → 𝐹𝐾)
8 mdetuni.sc . . . . . 6 (𝜑 → ∀𝑥𝐵𝑦𝐾𝑧𝐵𝑤𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = (𝑦 · (𝐷𝑧))))
983ad2ant1 1080 . . . . 5 ((𝜑 ∧ (𝐸𝐵𝐹𝐾𝐺𝐵) ∧ 𝐻𝑁) → ∀𝑥𝐵𝑦𝐾𝑧𝐵𝑤𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = (𝑦 · (𝐷𝑧))))
10 reseq1 5350 . . . . . . . . . 10 (𝑥 = 𝐸 → (𝑥 ↾ ({𝑤} × 𝑁)) = (𝐸 ↾ ({𝑤} × 𝑁)))
1110eqeq1d 2623 . . . . . . . . 9 (𝑥 = 𝐸 → ((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ↔ (𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘𝑓 · (𝑧 ↾ ({𝑤} × 𝑁)))))
12 reseq1 5350 . . . . . . . . . 10 (𝑥 = 𝐸 → (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))
1312eqeq1d 2623 . . . . . . . . 9 (𝑥 = 𝐸 → ((𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ↔ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))))
1411, 13anbi12d 746 . . . . . . . 8 (𝑥 = 𝐸 → (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) ↔ ((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))))
15 fveq2 6148 . . . . . . . . 9 (𝑥 = 𝐸 → (𝐷𝑥) = (𝐷𝐸))
1615eqeq1d 2623 . . . . . . . 8 (𝑥 = 𝐸 → ((𝐷𝑥) = (𝑦 · (𝐷𝑧)) ↔ (𝐷𝐸) = (𝑦 · (𝐷𝑧))))
1714, 16imbi12d 334 . . . . . . 7 (𝑥 = 𝐸 → ((((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = (𝑦 · (𝐷𝑧))) ↔ (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = (𝑦 · (𝐷𝑧)))))
18172ralbidv 2983 . . . . . 6 (𝑥 = 𝐸 → (∀𝑧𝐵𝑤𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = (𝑦 · (𝐷𝑧))) ↔ ∀𝑧𝐵𝑤𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = (𝑦 · (𝐷𝑧)))))
19 sneq 4158 . . . . . . . . . . . 12 (𝑦 = 𝐹 → {𝑦} = {𝐹})
2019xpeq2d 5099 . . . . . . . . . . 11 (𝑦 = 𝐹 → (({𝑤} × 𝑁) × {𝑦}) = (({𝑤} × 𝑁) × {𝐹}))
2120oveq1d 6619 . . . . . . . . . 10 (𝑦 = 𝐹 → ((({𝑤} × 𝑁) × {𝑦}) ∘𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) = ((({𝑤} × 𝑁) × {𝐹}) ∘𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))))
2221eqeq2d 2631 . . . . . . . . 9 (𝑦 = 𝐹 → ((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ↔ (𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘𝑓 · (𝑧 ↾ ({𝑤} × 𝑁)))))
2322anbi1d 740 . . . . . . . 8 (𝑦 = 𝐹 → (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) ↔ ((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))))
24 oveq1 6611 . . . . . . . . 9 (𝑦 = 𝐹 → (𝑦 · (𝐷𝑧)) = (𝐹 · (𝐷𝑧)))
2524eqeq2d 2631 . . . . . . . 8 (𝑦 = 𝐹 → ((𝐷𝐸) = (𝑦 · (𝐷𝑧)) ↔ (𝐷𝐸) = (𝐹 · (𝐷𝑧))))
2623, 25imbi12d 334 . . . . . . 7 (𝑦 = 𝐹 → ((((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = (𝑦 · (𝐷𝑧))) ↔ (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = (𝐹 · (𝐷𝑧)))))
27262ralbidv 2983 . . . . . 6 (𝑦 = 𝐹 → (∀𝑧𝐵𝑤𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = (𝑦 · (𝐷𝑧))) ↔ ∀𝑧𝐵𝑤𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = (𝐹 · (𝐷𝑧)))))
2818, 27rspc2va 3307 . . . . 5 (((𝐸𝐵𝐹𝐾) ∧ ∀𝑥𝐵𝑦𝐾𝑧𝐵𝑤𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = (𝑦 · (𝐷𝑧)))) → ∀𝑧𝐵𝑤𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = (𝐹 · (𝐷𝑧))))
296, 7, 9, 28syl21anc 1322 . . . 4 ((𝜑 ∧ (𝐸𝐵𝐹𝐾𝐺𝐵) ∧ 𝐻𝑁) → ∀𝑧𝐵𝑤𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = (𝐹 · (𝐷𝑧))))
30 reseq1 5350 . . . . . . . . 9 (𝑧 = 𝐺 → (𝑧 ↾ ({𝑤} × 𝑁)) = (𝐺 ↾ ({𝑤} × 𝑁)))
3130oveq2d 6620 . . . . . . . 8 (𝑧 = 𝐺 → ((({𝑤} × 𝑁) × {𝐹}) ∘𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) = ((({𝑤} × 𝑁) × {𝐹}) ∘𝑓 · (𝐺 ↾ ({𝑤} × 𝑁))))
3231eqeq2d 2631 . . . . . . 7 (𝑧 = 𝐺 → ((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ↔ (𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘𝑓 · (𝐺 ↾ ({𝑤} × 𝑁)))))
33 reseq1 5350 . . . . . . . 8 (𝑧 = 𝐺 → (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))
3433eqeq2d 2631 . . . . . . 7 (𝑧 = 𝐺 → ((𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ↔ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))))
3532, 34anbi12d 746 . . . . . 6 (𝑧 = 𝐺 → (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) ↔ ((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘𝑓 · (𝐺 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))))
36 fveq2 6148 . . . . . . . 8 (𝑧 = 𝐺 → (𝐷𝑧) = (𝐷𝐺))
3736oveq2d 6620 . . . . . . 7 (𝑧 = 𝐺 → (𝐹 · (𝐷𝑧)) = (𝐹 · (𝐷𝐺)))
3837eqeq2d 2631 . . . . . 6 (𝑧 = 𝐺 → ((𝐷𝐸) = (𝐹 · (𝐷𝑧)) ↔ (𝐷𝐸) = (𝐹 · (𝐷𝐺))))
3935, 38imbi12d 334 . . . . 5 (𝑧 = 𝐺 → ((((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = (𝐹 · (𝐷𝑧))) ↔ (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘𝑓 · (𝐺 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = (𝐹 · (𝐷𝐺)))))
40 sneq 4158 . . . . . . . . . 10 (𝑤 = 𝐻 → {𝑤} = {𝐻})
4140xpeq1d 5098 . . . . . . . . 9 (𝑤 = 𝐻 → ({𝑤} × 𝑁) = ({𝐻} × 𝑁))
4241reseq2d 5356 . . . . . . . 8 (𝑤 = 𝐻 → (𝐸 ↾ ({𝑤} × 𝑁)) = (𝐸 ↾ ({𝐻} × 𝑁)))
4341xpeq1d 5098 . . . . . . . . 9 (𝑤 = 𝐻 → (({𝑤} × 𝑁) × {𝐹}) = (({𝐻} × 𝑁) × {𝐹}))
4441reseq2d 5356 . . . . . . . . 9 (𝑤 = 𝐻 → (𝐺 ↾ ({𝑤} × 𝑁)) = (𝐺 ↾ ({𝐻} × 𝑁)))
4543, 44oveq12d 6622 . . . . . . . 8 (𝑤 = 𝐻 → ((({𝑤} × 𝑁) × {𝐹}) ∘𝑓 · (𝐺 ↾ ({𝑤} × 𝑁))) = ((({𝐻} × 𝑁) × {𝐹}) ∘𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))))
4642, 45eqeq12d 2636 . . . . . . 7 (𝑤 = 𝐻 → ((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘𝑓 · (𝐺 ↾ ({𝑤} × 𝑁))) ↔ (𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘𝑓 · (𝐺 ↾ ({𝐻} × 𝑁)))))
4740difeq2d 3706 . . . . . . . . . 10 (𝑤 = 𝐻 → (𝑁 ∖ {𝑤}) = (𝑁 ∖ {𝐻}))
4847xpeq1d 5098 . . . . . . . . 9 (𝑤 = 𝐻 → ((𝑁 ∖ {𝑤}) × 𝑁) = ((𝑁 ∖ {𝐻}) × 𝑁))
4948reseq2d 5356 . . . . . . . 8 (𝑤 = 𝐻 → (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))
5048reseq2d 5356 . . . . . . . 8 (𝑤 = 𝐻 → (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))
5149, 50eqeq12d 2636 . . . . . . 7 (𝑤 = 𝐻 → ((𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ↔ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))))
5246, 51anbi12d 746 . . . . . 6 (𝑤 = 𝐻 → (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘𝑓 · (𝐺 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) ↔ ((𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))))
5352imbi1d 331 . . . . 5 (𝑤 = 𝐻 → ((((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘𝑓 · (𝐺 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = (𝐹 · (𝐷𝐺))) ↔ (((𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → (𝐷𝐸) = (𝐹 · (𝐷𝐺)))))
5439, 53rspc2va 3307 . . . 4 (((𝐺𝐵𝐻𝑁) ∧ ∀𝑧𝐵𝑤𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = (𝐹 · (𝐷𝑧)))) → (((𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → (𝐷𝐸) = (𝐹 · (𝐷𝐺))))
554, 5, 29, 54syl21anc 1322 . . 3 ((𝜑 ∧ (𝐸𝐵𝐹𝐾𝐺𝐵) ∧ 𝐻𝑁) → (((𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → (𝐷𝐸) = (𝐹 · (𝐷𝐺))))
563, 55syl3an3 1358 . 2 ((𝜑 ∧ (𝐸𝐵𝐹𝐾𝐺𝐵) ∧ (𝐻𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (((𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → (𝐷𝐸) = (𝐹 · (𝐷𝐺))))
571, 2, 56mp2and 714 1 ((𝜑 ∧ (𝐸𝐵𝐹𝐾𝐺𝐵) ∧ (𝐻𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (𝐷𝐸) = (𝐹 · (𝐷𝐺)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036   = wceq 1480  wcel 1987  wne 2790  wral 2907  cdif 3552  {csn 4148   × cxp 5072  cres 5076  wf 5843  cfv 5847  (class class class)co 6604  𝑓 cof 6848  Fincfn 7899  Basecbs 15781  +gcplusg 15862  .rcmulr 15863  0gc0g 16021  1rcur 18422  Ringcrg 18468   Mat cmat 20132
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-opab 4674  df-xp 5080  df-res 5086  df-iota 5810  df-fv 5855  df-ov 6607
This theorem is referenced by:  mdetuni0  20346
  Copyright terms: Public domain W3C validator