mdetunilem4 - Metamath Proof Explorer

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

Theorem mdetunilem4 20640

Description: Lemma for mdetuni 20647. (Contributed by SO, 15-Jul-2018.)

**Hypotheses**
Ref	Expression
mdetuni.a	⊢ 𝐴 = (𝑁 Mat 𝑅)
mdetuni.b	⊢ 𝐵 = (Base‘𝐴)
mdetuni.k	⊢ 𝐾 = (Base‘𝑅)
mdetuni.0g	⊢ 0 = (0_g‘𝑅)
mdetuni.1r	⊢ 1 = (1_r‘𝑅)
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**
Step	Hyp	Ref	Expression
1		simp32 1252	. 2 ⊢ ((𝜑 ∧ (𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ (𝐻 ∈ 𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))))
2		simp33 1253	. 2 ⊢ ((𝜑 ∧ (𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ (𝐻 ∈ 𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))
3		simp1 1130	. . 3 ⊢ ((𝐻 ∈ 𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → 𝐻 ∈ 𝑁)
4		simp23 1250	. . . 4 ⊢ ((𝜑 ∧ (𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝐻 ∈ 𝑁) → 𝐺 ∈ 𝐵)
5		simp3 1132	. . . 4 ⊢ ((𝜑 ∧ (𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝐻 ∈ 𝑁) → 𝐻 ∈ 𝑁)
6		simp21 1248	. . . . 5 ⊢ ((𝜑 ∧ (𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝐻 ∈ 𝑁) → 𝐸 ∈ 𝐵)
7		simp22 1249	. . . . 5 ⊢ ((𝜑 ∧ (𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝐻 ∈ 𝑁) → 𝐹 ∈ 𝐾)
8		mdetuni.sc	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧))))
9	8	3ad2ant1 1127	. . . . 5 ⊢ ((𝜑 ∧ (𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝐻 ∈ 𝑁) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧))))
10		reseq1 5529	. . . . . . . . . 10 ⊢ (𝑥 = 𝐸 → (𝑥 ↾ ({𝑤} × 𝑁)) = (𝐸 ↾ ({𝑤} × 𝑁)))
11	10	eqeq1d 2773	. . . . . . . . 9 ⊢ (𝑥 = 𝐸 → ((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ↔ (𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁)))))
12		reseq1 5529	. . . . . . . . . 10 ⊢ (𝑥 = 𝐸 → (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))
13	12	eqeq1d 2773	. . . . . . . . 9 ⊢ (𝑥 = 𝐸 → ((𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ↔ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))))
14	11, 13	anbi12d 610	. . . . . . . 8 ⊢ (𝑥 = 𝐸 → (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) ↔ ((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))))
15		fveq2 6333	. . . . . . . . 9 ⊢ (𝑥 = 𝐸 → (𝐷‘𝑥) = (𝐷‘𝐸))
16	15	eqeq1d 2773	. . . . . . . 8 ⊢ (𝑥 = 𝐸 → ((𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧)) ↔ (𝐷‘𝐸) = (𝑦 · (𝐷‘𝑧))))
17	14, 16	imbi12d 333	. . . . . . 7 ⊢ (𝑥 = 𝐸 → ((((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧))) ↔ (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = (𝑦 · (𝐷‘𝑧)))))
18	17	2ralbidv 3138	. . . . . 6 ⊢ (𝑥 = 𝐸 → (∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧))) ↔ ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = (𝑦 · (𝐷‘𝑧)))))
19		sneq 4327	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝐹 → {𝑦} = {𝐹})
20	19	xpeq2d 5280	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐹 → (({𝑤} × 𝑁) × {𝑦}) = (({𝑤} × 𝑁) × {𝐹}))
21	20	oveq1d 6809	. . . . . . . . . 10 ⊢ (𝑦 = 𝐹 → ((({𝑤} × 𝑁) × {𝑦}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))))
22	21	eqeq2d 2781	. . . . . . . . 9 ⊢ (𝑦 = 𝐹 → ((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ↔ (𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁)))))
23	22	anbi1d 609	. . . . . . . 8 ⊢ (𝑦 = 𝐹 → (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) ↔ ((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))))
24		oveq1 6801	. . . . . . . . 9 ⊢ (𝑦 = 𝐹 → (𝑦 · (𝐷‘𝑧)) = (𝐹 · (𝐷‘𝑧)))
25	24	eqeq2d 2781	. . . . . . . 8 ⊢ (𝑦 = 𝐹 → ((𝐷‘𝐸) = (𝑦 · (𝐷‘𝑧)) ↔ (𝐷‘𝐸) = (𝐹 · (𝐷‘𝑧))))
26	23, 25	imbi12d 333	. . . . . . 7 ⊢ (𝑦 = 𝐹 → ((((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = (𝑦 · (𝐷‘𝑧))) ↔ (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = (𝐹 · (𝐷‘𝑧)))))
27	26	2ralbidv 3138	. . . . . 6 ⊢ (𝑦 = 𝐹 → (∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = (𝑦 · (𝐷‘𝑧))) ↔ ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = (𝐹 · (𝐷‘𝑧)))))
28	18, 27	rspc2va 3474	. . . . 5 ⊢ (((𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧)))) → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = (𝐹 · (𝐷‘𝑧))))
29	6, 7, 9, 28	syl21anc 1475	. . . 4 ⊢ ((𝜑 ∧ (𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝐻 ∈ 𝑁) → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = (𝐹 · (𝐷‘𝑧))))
30		reseq1 5529	. . . . . . . . 9 ⊢ (𝑧 = 𝐺 → (𝑧 ↾ ({𝑤} × 𝑁)) = (𝐺 ↾ ({𝑤} × 𝑁)))
31	30	oveq2d 6810	. . . . . . . 8 ⊢ (𝑧 = 𝐺 → ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝑤} × 𝑁))))
32	31	eqeq2d 2781	. . . . . . 7 ⊢ (𝑧 = 𝐺 → ((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ↔ (𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝑤} × 𝑁)))))
33		reseq1 5529	. . . . . . . 8 ⊢ (𝑧 = 𝐺 → (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))
34	33	eqeq2d 2781	. . . . . . 7 ⊢ (𝑧 = 𝐺 → ((𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ↔ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))))
35	32, 34	anbi12d 610	. . . . . 6 ⊢ (𝑧 = 𝐺 → (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) ↔ ((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))))
36		fveq2 6333	. . . . . . . 8 ⊢ (𝑧 = 𝐺 → (𝐷‘𝑧) = (𝐷‘𝐺))
37	36	oveq2d 6810	. . . . . . 7 ⊢ (𝑧 = 𝐺 → (𝐹 · (𝐷‘𝑧)) = (𝐹 · (𝐷‘𝐺)))
38	37	eqeq2d 2781	. . . . . 6 ⊢ (𝑧 = 𝐺 → ((𝐷‘𝐸) = (𝐹 · (𝐷‘𝑧)) ↔ (𝐷‘𝐸) = (𝐹 · (𝐷‘𝐺))))
39	35, 38	imbi12d 333	. . . . 5 ⊢ (𝑧 = 𝐺 → ((((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = (𝐹 · (𝐷‘𝑧))) ↔ (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = (𝐹 · (𝐷‘𝐺)))))
40		sneq 4327	. . . . . . . . . 10 ⊢ (𝑤 = 𝐻 → {𝑤} = {𝐻})
41	40	xpeq1d 5279	. . . . . . . . 9 ⊢ (𝑤 = 𝐻 → ({𝑤} × 𝑁) = ({𝐻} × 𝑁))
42	41	reseq2d 5535	. . . . . . . 8 ⊢ (𝑤 = 𝐻 → (𝐸 ↾ ({𝑤} × 𝑁)) = (𝐸 ↾ ({𝐻} × 𝑁)))
43	41	xpeq1d 5279	. . . . . . . . 9 ⊢ (𝑤 = 𝐻 → (({𝑤} × 𝑁) × {𝐹}) = (({𝐻} × 𝑁) × {𝐹}))
44	41	reseq2d 5535	. . . . . . . . 9 ⊢ (𝑤 = 𝐻 → (𝐺 ↾ ({𝑤} × 𝑁)) = (𝐺 ↾ ({𝐻} × 𝑁)))
45	43, 44	oveq12d 6812	. . . . . . . 8 ⊢ (𝑤 = 𝐻 → ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝑤} × 𝑁))) = ((({𝐻} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))))
46	42, 45	eqeq12d 2786	. . . . . . 7 ⊢ (𝑤 = 𝐻 → ((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝑤} × 𝑁))) ↔ (𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝐻} × 𝑁)))))
47	40	difeq2d 3880	. . . . . . . . . 10 ⊢ (𝑤 = 𝐻 → (𝑁 ∖ {𝑤}) = (𝑁 ∖ {𝐻}))
48	47	xpeq1d 5279	. . . . . . . . 9 ⊢ (𝑤 = 𝐻 → ((𝑁 ∖ {𝑤}) × 𝑁) = ((𝑁 ∖ {𝐻}) × 𝑁))
49	48	reseq2d 5535	. . . . . . . 8 ⊢ (𝑤 = 𝐻 → (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))
50	48	reseq2d 5535	. . . . . . . 8 ⊢ (𝑤 = 𝐻 → (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))
51	49, 50	eqeq12d 2786	. . . . . . 7 ⊢ (𝑤 = 𝐻 → ((𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ↔ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))))
52	46, 51	anbi12d 610	. . . . . 6 ⊢ (𝑤 = 𝐻 → (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) ↔ ((𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))))
53	52	imbi1d 330	. . . . 5 ⊢ (𝑤 = 𝐻 → ((((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = (𝐹 · (𝐷‘𝐺))) ↔ (((𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → (𝐷‘𝐸) = (𝐹 · (𝐷‘𝐺)))))
54	39, 53	rspc2va 3474	. . . 4 ⊢ (((𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁) ∧ ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = (𝐹 · (𝐷‘𝑧)))) → (((𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → (𝐷‘𝐸) = (𝐹 · (𝐷‘𝐺))))
55	4, 5, 29, 54	syl21anc 1475	. . 3 ⊢ ((𝜑 ∧ (𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝐻 ∈ 𝑁) → (((𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → (𝐷‘𝐸) = (𝐹 · (𝐷‘𝐺))))
56	3, 55	syl3an3 1169	. 2 ⊢ ((𝜑 ∧ (𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ (𝐻 ∈ 𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (((𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → (𝐷‘𝐸) = (𝐹 · (𝐷‘𝐺))))
57	1, 2, 56	mp2and 673	1 ⊢ ((𝜑 ∧ (𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ (𝐻 ∈ 𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (𝐷‘𝐸) = (𝐹 · (𝐷‘𝐺)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 382 ∧ w3a 1071 = wceq 1631 ∈ wcel 2145 ≠ wne 2943 ∀wral 3061 ∖ cdif 3721 {csn 4317 × cxp 5248 ↾ cres 5252 ⟶wf 6028 ‘cfv 6032 (class class class)co 6794 ∘_𝑓 cof 7043 Fincfn 8110 Basecbs 16065 +_gcplusg 16150 ._rcmulr 16151 0_gc0g 16309 1_rcur 18710 Ringcrg 18756 Mat cmat 20431

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751

This theorem depends on definitions: df-bi 197 df-an 383 df-or 829 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3353 df-dif 3727 df-un 3729 df-in 3731 df-ss 3738 df-nul 4065 df-if 4227 df-sn 4318 df-pr 4320 df-op 4324 df-uni 4576 df-br 4788 df-opab 4848 df-xp 5256 df-res 5262 df-iota 5995 df-fv 6040 df-ov 6797

This theorem is referenced by: mdetuni0 20646

W3C validator