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

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

Proof of Theorem mdetunilem4
StepHypRef Expression
1 simp32 1202 . 2 ((𝜑 ∧ (𝐸𝐵𝐹𝐾𝐺𝐵) ∧ (𝐻𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘f · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘f · (𝐺 ↾ ({𝐻} × 𝑁))))
2 simp33 1203 . 2 ((𝜑 ∧ (𝐸𝐵𝐹𝐾𝐺𝐵) ∧ (𝐻𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘f · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))
3 simp1 1128 . . 3 ((𝐻𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘f · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → 𝐻𝑁)
4 simp23 1200 . . . 4 ((𝜑 ∧ (𝐸𝐵𝐹𝐾𝐺𝐵) ∧ 𝐻𝑁) → 𝐺𝐵)
5 simp3 1130 . . . 4 ((𝜑 ∧ (𝐸𝐵𝐹𝐾𝐺𝐵) ∧ 𝐻𝑁) → 𝐻𝑁)
6 simp21 1198 . . . . 5 ((𝜑 ∧ (𝐸𝐵𝐹𝐾𝐺𝐵) ∧ 𝐻𝑁) → 𝐸𝐵)
7 simp22 1199 . . . . 5 ((𝜑 ∧ (𝐸𝐵𝐹𝐾𝐺𝐵) ∧ 𝐻𝑁) → 𝐹𝐾)
8 mdetuni.sc . . . . . 6 (𝜑 → ∀𝑥𝐵𝑦𝐾𝑧𝐵𝑤𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = (𝑦 · (𝐷𝑧))))
983ad2ant1 1125 . . . . 5 ((𝜑 ∧ (𝐸𝐵𝐹𝐾𝐺𝐵) ∧ 𝐻𝑁) → ∀𝑥𝐵𝑦𝐾𝑧𝐵𝑤𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = (𝑦 · (𝐷𝑧))))
10 reseq1 5840 . . . . . . . . . 10 (𝑥 = 𝐸 → (𝑥 ↾ ({𝑤} × 𝑁)) = (𝐸 ↾ ({𝑤} × 𝑁)))
1110eqeq1d 2820 . . . . . . . . 9 (𝑥 = 𝐸 → ((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ↔ (𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁)))))
12 reseq1 5840 . . . . . . . . . 10 (𝑥 = 𝐸 → (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))
1312eqeq1d 2820 . . . . . . . . 9 (𝑥 = 𝐸 → ((𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ↔ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))))
1411, 13anbi12d 630 . . . . . . . 8 (𝑥 = 𝐸 → (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) ↔ ((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))))
15 fveqeq2 6672 . . . . . . . 8 (𝑥 = 𝐸 → ((𝐷𝑥) = (𝑦 · (𝐷𝑧)) ↔ (𝐷𝐸) = (𝑦 · (𝐷𝑧))))
1614, 15imbi12d 346 . . . . . . 7 (𝑥 = 𝐸 → ((((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = (𝑦 · (𝐷𝑧))) ↔ (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = (𝑦 · (𝐷𝑧)))))
17162ralbidv 3196 . . . . . 6 (𝑥 = 𝐸 → (∀𝑧𝐵𝑤𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = (𝑦 · (𝐷𝑧))) ↔ ∀𝑧𝐵𝑤𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = (𝑦 · (𝐷𝑧)))))
18 sneq 4567 . . . . . . . . . . . 12 (𝑦 = 𝐹 → {𝑦} = {𝐹})
1918xpeq2d 5578 . . . . . . . . . . 11 (𝑦 = 𝐹 → (({𝑤} × 𝑁) × {𝑦}) = (({𝑤} × 𝑁) × {𝐹}))
2019oveq1d 7160 . . . . . . . . . 10 (𝑦 = 𝐹 → ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) = ((({𝑤} × 𝑁) × {𝐹}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))))
2120eqeq2d 2829 . . . . . . . . 9 (𝑦 = 𝐹 → ((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ↔ (𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁)))))
2221anbi1d 629 . . . . . . . 8 (𝑦 = 𝐹 → (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) ↔ ((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))))
23 oveq1 7152 . . . . . . . . 9 (𝑦 = 𝐹 → (𝑦 · (𝐷𝑧)) = (𝐹 · (𝐷𝑧)))
2423eqeq2d 2829 . . . . . . . 8 (𝑦 = 𝐹 → ((𝐷𝐸) = (𝑦 · (𝐷𝑧)) ↔ (𝐷𝐸) = (𝐹 · (𝐷𝑧))))
2522, 24imbi12d 346 . . . . . . 7 (𝑦 = 𝐹 → ((((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = (𝑦 · (𝐷𝑧))) ↔ (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = (𝐹 · (𝐷𝑧)))))
26252ralbidv 3196 . . . . . 6 (𝑦 = 𝐹 → (∀𝑧𝐵𝑤𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = (𝑦 · (𝐷𝑧))) ↔ ∀𝑧𝐵𝑤𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = (𝐹 · (𝐷𝑧)))))
2717, 26rspc2va 3631 . . . . 5 (((𝐸𝐵𝐹𝐾) ∧ ∀𝑥𝐵𝑦𝐾𝑧𝐵𝑤𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = (𝑦 · (𝐷𝑧)))) → ∀𝑧𝐵𝑤𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = (𝐹 · (𝐷𝑧))))
286, 7, 9, 27syl21anc 833 . . . 4 ((𝜑 ∧ (𝐸𝐵𝐹𝐾𝐺𝐵) ∧ 𝐻𝑁) → ∀𝑧𝐵𝑤𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = (𝐹 · (𝐷𝑧))))
29 reseq1 5840 . . . . . . . . 9 (𝑧 = 𝐺 → (𝑧 ↾ ({𝑤} × 𝑁)) = (𝐺 ↾ ({𝑤} × 𝑁)))
3029oveq2d 7161 . . . . . . . 8 (𝑧 = 𝐺 → ((({𝑤} × 𝑁) × {𝐹}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) = ((({𝑤} × 𝑁) × {𝐹}) ∘f · (𝐺 ↾ ({𝑤} × 𝑁))))
3130eqeq2d 2829 . . . . . . 7 (𝑧 = 𝐺 → ((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ↔ (𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘f · (𝐺 ↾ ({𝑤} × 𝑁)))))
32 reseq1 5840 . . . . . . . 8 (𝑧 = 𝐺 → (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))
3332eqeq2d 2829 . . . . . . 7 (𝑧 = 𝐺 → ((𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ↔ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))))
3431, 33anbi12d 630 . . . . . 6 (𝑧 = 𝐺 → (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) ↔ ((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘f · (𝐺 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))))
35 fveq2 6663 . . . . . . . 8 (𝑧 = 𝐺 → (𝐷𝑧) = (𝐷𝐺))
3635oveq2d 7161 . . . . . . 7 (𝑧 = 𝐺 → (𝐹 · (𝐷𝑧)) = (𝐹 · (𝐷𝐺)))
3736eqeq2d 2829 . . . . . 6 (𝑧 = 𝐺 → ((𝐷𝐸) = (𝐹 · (𝐷𝑧)) ↔ (𝐷𝐸) = (𝐹 · (𝐷𝐺))))
3834, 37imbi12d 346 . . . . 5 (𝑧 = 𝐺 → ((((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = (𝐹 · (𝐷𝑧))) ↔ (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘f · (𝐺 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = (𝐹 · (𝐷𝐺)))))
39 sneq 4567 . . . . . . . . . 10 (𝑤 = 𝐻 → {𝑤} = {𝐻})
4039xpeq1d 5577 . . . . . . . . 9 (𝑤 = 𝐻 → ({𝑤} × 𝑁) = ({𝐻} × 𝑁))
4140reseq2d 5846 . . . . . . . 8 (𝑤 = 𝐻 → (𝐸 ↾ ({𝑤} × 𝑁)) = (𝐸 ↾ ({𝐻} × 𝑁)))
4240xpeq1d 5577 . . . . . . . . 9 (𝑤 = 𝐻 → (({𝑤} × 𝑁) × {𝐹}) = (({𝐻} × 𝑁) × {𝐹}))
4340reseq2d 5846 . . . . . . . . 9 (𝑤 = 𝐻 → (𝐺 ↾ ({𝑤} × 𝑁)) = (𝐺 ↾ ({𝐻} × 𝑁)))
4442, 43oveq12d 7163 . . . . . . . 8 (𝑤 = 𝐻 → ((({𝑤} × 𝑁) × {𝐹}) ∘f · (𝐺 ↾ ({𝑤} × 𝑁))) = ((({𝐻} × 𝑁) × {𝐹}) ∘f · (𝐺 ↾ ({𝐻} × 𝑁))))
4541, 44eqeq12d 2834 . . . . . . 7 (𝑤 = 𝐻 → ((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘f · (𝐺 ↾ ({𝑤} × 𝑁))) ↔ (𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘f · (𝐺 ↾ ({𝐻} × 𝑁)))))
4639difeq2d 4096 . . . . . . . . . 10 (𝑤 = 𝐻 → (𝑁 ∖ {𝑤}) = (𝑁 ∖ {𝐻}))
4746xpeq1d 5577 . . . . . . . . 9 (𝑤 = 𝐻 → ((𝑁 ∖ {𝑤}) × 𝑁) = ((𝑁 ∖ {𝐻}) × 𝑁))
4847reseq2d 5846 . . . . . . . 8 (𝑤 = 𝐻 → (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))
4947reseq2d 5846 . . . . . . . 8 (𝑤 = 𝐻 → (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))
5048, 49eqeq12d 2834 . . . . . . 7 (𝑤 = 𝐻 → ((𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ↔ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))))
5145, 50anbi12d 630 . . . . . 6 (𝑤 = 𝐻 → (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘f · (𝐺 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) ↔ ((𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘f · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))))
5251imbi1d 343 . . . . 5 (𝑤 = 𝐻 → ((((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘f · (𝐺 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = (𝐹 · (𝐷𝐺))) ↔ (((𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘f · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → (𝐷𝐸) = (𝐹 · (𝐷𝐺)))))
5338, 52rspc2va 3631 . . . 4 (((𝐺𝐵𝐻𝑁) ∧ ∀𝑧𝐵𝑤𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝐸) = (𝐹 · (𝐷𝑧)))) → (((𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘f · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → (𝐷𝐸) = (𝐹 · (𝐷𝐺))))
544, 5, 28, 53syl21anc 833 . . 3 ((𝜑 ∧ (𝐸𝐵𝐹𝐾𝐺𝐵) ∧ 𝐻𝑁) → (((𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘f · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → (𝐷𝐸) = (𝐹 · (𝐷𝐺))))
553, 54syl3an3 1157 . 2 ((𝜑 ∧ (𝐸𝐵𝐹𝐾𝐺𝐵) ∧ (𝐻𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘f · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (((𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘f · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → (𝐷𝐸) = (𝐹 · (𝐷𝐺))))
561, 2, 55mp2and 695 1 ((𝜑 ∧ (𝐸𝐵𝐹𝐾𝐺𝐵) ∧ (𝐻𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘f · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (𝐷𝐸) = (𝐹 · (𝐷𝐺)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079   = wceq 1528  wcel 2105  wne 3013  wral 3135  cdif 3930  {csn 4557   × cxp 5546  cres 5550  wf 6344  cfv 6348  (class class class)co 7145  f cof 7396  Fincfn 8497  Basecbs 16471  +gcplusg 16553  .rcmulr 16554  0gc0g 16701  1rcur 19180  Ringcrg 19226   Mat cmat 20944
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-xp 5554  df-res 5560  df-iota 6307  df-fv 6356  df-ov 7148
This theorem is referenced by:  mdetuni0  21158
  Copyright terms: Public domain W3C validator