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 20240

Description: Lemma for mdetuni 20247. (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 1091	. 2 ⊢ ((𝜑 ∧ (𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ (𝐻 ∈ 𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))))
2		simp33 1092	. 2 ⊢ ((𝜑 ∧ (𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ (𝐻 ∈ 𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))
3		simp1 1054	. . 3 ⊢ ((𝐻 ∈ 𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → 𝐻 ∈ 𝑁)
4		simp23 1089	. . . 4 ⊢ ((𝜑 ∧ (𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝐻 ∈ 𝑁) → 𝐺 ∈ 𝐵)
5		simp3 1056	. . . 4 ⊢ ((𝜑 ∧ (𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝐻 ∈ 𝑁) → 𝐻 ∈ 𝑁)
6		simp21 1087	. . . . 5 ⊢ ((𝜑 ∧ (𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝐻 ∈ 𝑁) → 𝐸 ∈ 𝐵)
7		simp22 1088	. . . . 5 ⊢ ((𝜑 ∧ (𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝐻 ∈ 𝑁) → 𝐹 ∈ 𝐾)
8		mdetuni.sc	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧))))
9	8	3ad2ant1 1075	. . . . 5 ⊢ ((𝜑 ∧ (𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝐻 ∈ 𝑁) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧))))
10		reseq1 5311	. . . . . . . . . 10 ⊢ (𝑥 = 𝐸 → (𝑥 ↾ ({𝑤} × 𝑁)) = (𝐸 ↾ ({𝑤} × 𝑁)))
11	10	eqeq1d 2612	. . . . . . . . 9 ⊢ (𝑥 = 𝐸 → ((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ↔ (𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁)))))
12		reseq1 5311	. . . . . . . . . 10 ⊢ (𝑥 = 𝐸 → (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))
13	12	eqeq1d 2612	. . . . . . . . 9 ⊢ (𝑥 = 𝐸 → ((𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ↔ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))))
14	11, 13	anbi12d 743	. . . . . . . 8 ⊢ (𝑥 = 𝐸 → (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) ↔ ((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))))
15		fveq2 6103	. . . . . . . . 9 ⊢ (𝑥 = 𝐸 → (𝐷‘𝑥) = (𝐷‘𝐸))
16	15	eqeq1d 2612	. . . . . . . 8 ⊢ (𝑥 = 𝐸 → ((𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧)) ↔ (𝐷‘𝐸) = (𝑦 · (𝐷‘𝑧))))
17	14, 16	imbi12d 333	. . . . . . 7 ⊢ (𝑥 = 𝐸 → ((((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧))) ↔ (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = (𝑦 · (𝐷‘𝑧)))))
18	17	2ralbidv 2972	. . . . . 6 ⊢ (𝑥 = 𝐸 → (∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧))) ↔ ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = (𝑦 · (𝐷‘𝑧)))))
19		sneq 4135	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝐹 → {𝑦} = {𝐹})
20	19	xpeq2d 5063	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐹 → (({𝑤} × 𝑁) × {𝑦}) = (({𝑤} × 𝑁) × {𝐹}))
21	20	oveq1d 6564	. . . . . . . . . 10 ⊢ (𝑦 = 𝐹 → ((({𝑤} × 𝑁) × {𝑦}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))))
22	21	eqeq2d 2620	. . . . . . . . 9 ⊢ (𝑦 = 𝐹 → ((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ↔ (𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁)))))
23	22	anbi1d 737	. . . . . . . 8 ⊢ (𝑦 = 𝐹 → (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) ↔ ((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))))
24		oveq1 6556	. . . . . . . . 9 ⊢ (𝑦 = 𝐹 → (𝑦 · (𝐷‘𝑧)) = (𝐹 · (𝐷‘𝑧)))
25	24	eqeq2d 2620	. . . . . . . 8 ⊢ (𝑦 = 𝐹 → ((𝐷‘𝐸) = (𝑦 · (𝐷‘𝑧)) ↔ (𝐷‘𝐸) = (𝐹 · (𝐷‘𝑧))))
26	23, 25	imbi12d 333	. . . . . . 7 ⊢ (𝑦 = 𝐹 → ((((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = (𝑦 · (𝐷‘𝑧))) ↔ (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = (𝐹 · (𝐷‘𝑧)))))
27	26	2ralbidv 2972	. . . . . 6 ⊢ (𝑦 = 𝐹 → (∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = (𝑦 · (𝐷‘𝑧))) ↔ ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = (𝐹 · (𝐷‘𝑧)))))
28	18, 27	rspc2va 3294	. . . . 5 ⊢ (((𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧)))) → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = (𝐹 · (𝐷‘𝑧))))
29	6, 7, 9, 28	syl21anc 1317	. . . 4 ⊢ ((𝜑 ∧ (𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝐻 ∈ 𝑁) → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = (𝐹 · (𝐷‘𝑧))))
30		reseq1 5311	. . . . . . . . 9 ⊢ (𝑧 = 𝐺 → (𝑧 ↾ ({𝑤} × 𝑁)) = (𝐺 ↾ ({𝑤} × 𝑁)))
31	30	oveq2d 6565	. . . . . . . 8 ⊢ (𝑧 = 𝐺 → ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝑤} × 𝑁))))
32	31	eqeq2d 2620	. . . . . . 7 ⊢ (𝑧 = 𝐺 → ((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ↔ (𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝑤} × 𝑁)))))
33		reseq1 5311	. . . . . . . 8 ⊢ (𝑧 = 𝐺 → (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))
34	33	eqeq2d 2620	. . . . . . 7 ⊢ (𝑧 = 𝐺 → ((𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ↔ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))))
35	32, 34	anbi12d 743	. . . . . 6 ⊢ (𝑧 = 𝐺 → (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) ↔ ((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))))
36		fveq2 6103	. . . . . . . 8 ⊢ (𝑧 = 𝐺 → (𝐷‘𝑧) = (𝐷‘𝐺))
37	36	oveq2d 6565	. . . . . . 7 ⊢ (𝑧 = 𝐺 → (𝐹 · (𝐷‘𝑧)) = (𝐹 · (𝐷‘𝐺)))
38	37	eqeq2d 2620	. . . . . 6 ⊢ (𝑧 = 𝐺 → ((𝐷‘𝐸) = (𝐹 · (𝐷‘𝑧)) ↔ (𝐷‘𝐸) = (𝐹 · (𝐷‘𝐺))))
39	35, 38	imbi12d 333	. . . . 5 ⊢ (𝑧 = 𝐺 → ((((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = (𝐹 · (𝐷‘𝑧))) ↔ (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = (𝐹 · (𝐷‘𝐺)))))
40		sneq 4135	. . . . . . . . . 10 ⊢ (𝑤 = 𝐻 → {𝑤} = {𝐻})
41	40	xpeq1d 5062	. . . . . . . . 9 ⊢ (𝑤 = 𝐻 → ({𝑤} × 𝑁) = ({𝐻} × 𝑁))
42	41	reseq2d 5317	. . . . . . . 8 ⊢ (𝑤 = 𝐻 → (𝐸 ↾ ({𝑤} × 𝑁)) = (𝐸 ↾ ({𝐻} × 𝑁)))
43	41	xpeq1d 5062	. . . . . . . . 9 ⊢ (𝑤 = 𝐻 → (({𝑤} × 𝑁) × {𝐹}) = (({𝐻} × 𝑁) × {𝐹}))
44	41	reseq2d 5317	. . . . . . . . 9 ⊢ (𝑤 = 𝐻 → (𝐺 ↾ ({𝑤} × 𝑁)) = (𝐺 ↾ ({𝐻} × 𝑁)))
45	43, 44	oveq12d 6567	. . . . . . . 8 ⊢ (𝑤 = 𝐻 → ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝑤} × 𝑁))) = ((({𝐻} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))))
46	42, 45	eqeq12d 2625	. . . . . . 7 ⊢ (𝑤 = 𝐻 → ((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝑤} × 𝑁))) ↔ (𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝐻} × 𝑁)))))
47	40	difeq2d 3690	. . . . . . . . . 10 ⊢ (𝑤 = 𝐻 → (𝑁 ∖ {𝑤}) = (𝑁 ∖ {𝐻}))
48	47	xpeq1d 5062	. . . . . . . . 9 ⊢ (𝑤 = 𝐻 → ((𝑁 ∖ {𝑤}) × 𝑁) = ((𝑁 ∖ {𝐻}) × 𝑁))
49	48	reseq2d 5317	. . . . . . . 8 ⊢ (𝑤 = 𝐻 → (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))
50	48	reseq2d 5317	. . . . . . . 8 ⊢ (𝑤 = 𝐻 → (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))
51	49, 50	eqeq12d 2625	. . . . . . 7 ⊢ (𝑤 = 𝐻 → ((𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ↔ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))))
52	46, 51	anbi12d 743	. . . . . 6 ⊢ (𝑤 = 𝐻 → (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) ↔ ((𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))))
53	52	imbi1d 330	. . . . 5 ⊢ (𝑤 = 𝐻 → ((((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = (𝐹 · (𝐷‘𝐺))) ↔ (((𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → (𝐷‘𝐸) = (𝐹 · (𝐷‘𝐺)))))
54	39, 53	rspc2va 3294	. . . 4 ⊢ (((𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁) ∧ ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝐹}) ∘_𝑓 · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = (𝐹 · (𝐷‘𝑧)))) → (((𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → (𝐷‘𝐸) = (𝐹 · (𝐷‘𝐺))))
55	4, 5, 29, 54	syl21anc 1317	. . 3 ⊢ ((𝜑 ∧ (𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝐻 ∈ 𝑁) → (((𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → (𝐷‘𝐸) = (𝐹 · (𝐷‘𝐺))))
56	3, 55	syl3an3 1353	. 2 ⊢ ((𝜑 ∧ (𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ (𝐻 ∈ 𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (((𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → (𝐷‘𝐸) = (𝐹 · (𝐷‘𝐺))))
57	1, 2, 56	mp2and 711	1 ⊢ ((𝜑 ∧ (𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ (𝐻 ∈ 𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘_𝑓 · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (𝐷‘𝐸) = (𝐹 · (𝐷‘𝐺)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 ≠ wne 2780 ∀wral 2896 ∖ cdif 3537 {csn 4125 × cxp 5036 ↾ cres 5040 ⟶wf 5800 ‘cfv 5804 (class class class)co 6549 ∘_𝑓 cof 6793 Fincfn 7841 Basecbs 15695 +_gcplusg 15768 ._rcmulr 15769 0_gc0g 15923 1_rcur 18324 Ringcrg 18370 Mat cmat 20032

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-br 4584 df-opab 4644 df-xp 5044 df-res 5050 df-iota 5768 df-fv 5812 df-ov 6552

This theorem is referenced by: mdetuni0 20246

W3C validator