mdetunilem3 - Metamath Proof Explorer

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

Theorem mdetunilem3 21763

Description: Lemma for mdetuni 21771. (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	⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘_f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧))))
mdetuni.sc	⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘_f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧))))

**Assertion**
Ref	Expression
mdetunilem3	⊢ (((𝜑 ∧ 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵) ∧ (𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘_f + (𝐺 ↾ ({𝐻} × 𝑁)))) ∧ ((𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (𝐷‘𝐸) = ((𝐷‘𝐹) + (𝐷‘𝐺)))

Distinct variable groups: 𝜑,𝑥,𝑦,𝑧,𝑤 𝑥,𝐵,𝑦,𝑧,𝑤 𝑥,𝐾,𝑦,𝑧,𝑤 𝑥,𝑁,𝑦,𝑧,𝑤 𝑥,𝐷,𝑦,𝑧,𝑤 𝑥, · ,𝑦,𝑧,𝑤 𝑥, + ,𝑦,𝑧,𝑤 𝑥, 0 ,𝑦,𝑧,𝑤 𝑥, 1 ,𝑦,𝑧,𝑤 𝑥,𝑅,𝑦,𝑧,𝑤 𝑥,𝐴,𝑦,𝑧,𝑤 𝑥,𝐸,𝑦,𝑧,𝑤 𝑥,𝐹,𝑦,𝑧,𝑤 𝑥,𝐺,𝑦,𝑧,𝑤 𝑥,𝐻,𝑦,𝑧,𝑤

**Proof of Theorem mdetunilem3**
Step	Hyp	Ref	Expression
1		simp23 1207	. 2 ⊢ (((𝜑 ∧ 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵) ∧ (𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘_f + (𝐺 ↾ ({𝐻} × 𝑁)))) ∧ ((𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘_f + (𝐺 ↾ ({𝐻} × 𝑁))))
2		simp3l 1200	. 2 ⊢ (((𝜑 ∧ 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵) ∧ (𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘_f + (𝐺 ↾ ({𝐻} × 𝑁)))) ∧ ((𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))
3		simp3r 1201	. 2 ⊢ (((𝜑 ∧ 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵) ∧ (𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘_f + (𝐺 ↾ ({𝐻} × 𝑁)))) ∧ ((𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))
4		simprl 768	. . . . 5 ⊢ (((𝜑 ∧ 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵) ∧ (𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁)) → 𝐺 ∈ 𝐵)
5		simprr 770	. . . . 5 ⊢ (((𝜑 ∧ 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵) ∧ (𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁)) → 𝐻 ∈ 𝑁)
6		simpl2 1191	. . . . . 6 ⊢ (((𝜑 ∧ 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵) ∧ (𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁)) → 𝐸 ∈ 𝐵)
7		simpl3 1192	. . . . . 6 ⊢ (((𝜑 ∧ 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵) ∧ (𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁)) → 𝐹 ∈ 𝐵)
8		simpl1 1190	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵) ∧ (𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁)) → 𝜑)
9		mdetuni.li	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘_f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧))))
10	8, 9	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵) ∧ (𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁)) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘_f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧))))
11		reseq1 5885	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐸 → (𝑥 ↾ ({𝑤} × 𝑁)) = (𝐸 ↾ ({𝑤} × 𝑁)))
12	11	eqeq1d 2740	. . . . . . . . . 10 ⊢ (𝑥 = 𝐸 → ((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘_f + (𝑧 ↾ ({𝑤} × 𝑁))) ↔ (𝐸 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘_f + (𝑧 ↾ ({𝑤} × 𝑁)))))
13		reseq1 5885	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐸 → (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))
14	13	eqeq1d 2740	. . . . . . . . . 10 ⊢ (𝑥 = 𝐸 → ((𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ↔ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))))
15	13	eqeq1d 2740	. . . . . . . . . 10 ⊢ (𝑥 = 𝐸 → ((𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ↔ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))))
16	12, 14, 15	3anbi123d 1435	. . . . . . . . 9 ⊢ (𝑥 = 𝐸 → (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘_f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) ↔ ((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘_f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))))
17		fveq2 6774	. . . . . . . . . 10 ⊢ (𝑥 = 𝐸 → (𝐷‘𝑥) = (𝐷‘𝐸))
18	17	eqeq1d 2740	. . . . . . . . 9 ⊢ (𝑥 = 𝐸 → ((𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧)) ↔ (𝐷‘𝐸) = ((𝐷‘𝑦) + (𝐷‘𝑧))))
19	16, 18	imbi12d 345	. . . . . . . 8 ⊢ (𝑥 = 𝐸 → ((((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘_f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧))) ↔ (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘_f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = ((𝐷‘𝑦) + (𝐷‘𝑧)))))
20	19	2ralbidv 3129	. . . . . . 7 ⊢ (𝑥 = 𝐸 → (∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘_f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧))) ↔ ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘_f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = ((𝐷‘𝑦) + (𝐷‘𝑧)))))
21		reseq1 5885	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝐹 → (𝑦 ↾ ({𝑤} × 𝑁)) = (𝐹 ↾ ({𝑤} × 𝑁)))
22	21	oveq1d 7290	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐹 → ((𝑦 ↾ ({𝑤} × 𝑁)) ∘_f + (𝑧 ↾ ({𝑤} × 𝑁))) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘_f + (𝑧 ↾ ({𝑤} × 𝑁))))
23	22	eqeq2d 2749	. . . . . . . . . 10 ⊢ (𝑦 = 𝐹 → ((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘_f + (𝑧 ↾ ({𝑤} × 𝑁))) ↔ (𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘_f + (𝑧 ↾ ({𝑤} × 𝑁)))))
24		reseq1 5885	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐹 → (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))
25	24	eqeq2d 2749	. . . . . . . . . 10 ⊢ (𝑦 = 𝐹 → ((𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ↔ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))))
26	23, 25	3anbi12d 1436	. . . . . . . . 9 ⊢ (𝑦 = 𝐹 → (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘_f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) ↔ ((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘_f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))))
27		fveq2 6774	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐹 → (𝐷‘𝑦) = (𝐷‘𝐹))
28	27	oveq1d 7290	. . . . . . . . . 10 ⊢ (𝑦 = 𝐹 → ((𝐷‘𝑦) + (𝐷‘𝑧)) = ((𝐷‘𝐹) + (𝐷‘𝑧)))
29	28	eqeq2d 2749	. . . . . . . . 9 ⊢ (𝑦 = 𝐹 → ((𝐷‘𝐸) = ((𝐷‘𝑦) + (𝐷‘𝑧)) ↔ (𝐷‘𝐸) = ((𝐷‘𝐹) + (𝐷‘𝑧))))
30	26, 29	imbi12d 345	. . . . . . . 8 ⊢ (𝑦 = 𝐹 → ((((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘_f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = ((𝐷‘𝑦) + (𝐷‘𝑧))) ↔ (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘_f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = ((𝐷‘𝐹) + (𝐷‘𝑧)))))
31	30	2ralbidv 3129	. . . . . . 7 ⊢ (𝑦 = 𝐹 → (∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘_f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = ((𝐷‘𝑦) + (𝐷‘𝑧))) ↔ ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘_f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = ((𝐷‘𝐹) + (𝐷‘𝑧)))))
32	20, 31	rspc2va 3571	. . . . . 6 ⊢ (((𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘_f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧)))) → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘_f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = ((𝐷‘𝐹) + (𝐷‘𝑧))))
33	6, 7, 10, 32	syl21anc 835	. . . . 5 ⊢ (((𝜑 ∧ 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵) ∧ (𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁)) → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘_f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = ((𝐷‘𝐹) + (𝐷‘𝑧))))
34		reseq1 5885	. . . . . . . . . 10 ⊢ (𝑧 = 𝐺 → (𝑧 ↾ ({𝑤} × 𝑁)) = (𝐺 ↾ ({𝑤} × 𝑁)))
35	34	oveq2d 7291	. . . . . . . . 9 ⊢ (𝑧 = 𝐺 → ((𝐹 ↾ ({𝑤} × 𝑁)) ∘_f + (𝑧 ↾ ({𝑤} × 𝑁))) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘_f + (𝐺 ↾ ({𝑤} × 𝑁))))
36	35	eqeq2d 2749	. . . . . . . 8 ⊢ (𝑧 = 𝐺 → ((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘_f + (𝑧 ↾ ({𝑤} × 𝑁))) ↔ (𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘_f + (𝐺 ↾ ({𝑤} × 𝑁)))))
37		reseq1 5885	. . . . . . . . 9 ⊢ (𝑧 = 𝐺 → (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))
38	37	eqeq2d 2749	. . . . . . . 8 ⊢ (𝑧 = 𝐺 → ((𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ↔ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))))
39	36, 38	3anbi13d 1437	. . . . . . 7 ⊢ (𝑧 = 𝐺 → (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘_f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) ↔ ((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘_f + (𝐺 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)))))
40		fveq2 6774	. . . . . . . . 9 ⊢ (𝑧 = 𝐺 → (𝐷‘𝑧) = (𝐷‘𝐺))
41	40	oveq2d 7291	. . . . . . . 8 ⊢ (𝑧 = 𝐺 → ((𝐷‘𝐹) + (𝐷‘𝑧)) = ((𝐷‘𝐹) + (𝐷‘𝐺)))
42	41	eqeq2d 2749	. . . . . . 7 ⊢ (𝑧 = 𝐺 → ((𝐷‘𝐸) = ((𝐷‘𝐹) + (𝐷‘𝑧)) ↔ (𝐷‘𝐸) = ((𝐷‘𝐹) + (𝐷‘𝐺))))
43	39, 42	imbi12d 345	. . . . . 6 ⊢ (𝑧 = 𝐺 → ((((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘_f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = ((𝐷‘𝐹) + (𝐷‘𝑧))) ↔ (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘_f + (𝐺 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = ((𝐷‘𝐹) + (𝐷‘𝐺)))))
44		sneq 4571	. . . . . . . . . . 11 ⊢ (𝑤 = 𝐻 → {𝑤} = {𝐻})
45	44	xpeq1d 5618	. . . . . . . . . 10 ⊢ (𝑤 = 𝐻 → ({𝑤} × 𝑁) = ({𝐻} × 𝑁))
46	45	reseq2d 5891	. . . . . . . . 9 ⊢ (𝑤 = 𝐻 → (𝐸 ↾ ({𝑤} × 𝑁)) = (𝐸 ↾ ({𝐻} × 𝑁)))
47	45	reseq2d 5891	. . . . . . . . . 10 ⊢ (𝑤 = 𝐻 → (𝐹 ↾ ({𝑤} × 𝑁)) = (𝐹 ↾ ({𝐻} × 𝑁)))
48	45	reseq2d 5891	. . . . . . . . . 10 ⊢ (𝑤 = 𝐻 → (𝐺 ↾ ({𝑤} × 𝑁)) = (𝐺 ↾ ({𝐻} × 𝑁)))
49	47, 48	oveq12d 7293	. . . . . . . . 9 ⊢ (𝑤 = 𝐻 → ((𝐹 ↾ ({𝑤} × 𝑁)) ∘_f + (𝐺 ↾ ({𝑤} × 𝑁))) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘_f + (𝐺 ↾ ({𝐻} × 𝑁))))
50	46, 49	eqeq12d 2754	. . . . . . . 8 ⊢ (𝑤 = 𝐻 → ((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘_f + (𝐺 ↾ ({𝑤} × 𝑁))) ↔ (𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘_f + (𝐺 ↾ ({𝐻} × 𝑁)))))
51	44	difeq2d 4057	. . . . . . . . . . 11 ⊢ (𝑤 = 𝐻 → (𝑁 ∖ {𝑤}) = (𝑁 ∖ {𝐻}))
52	51	xpeq1d 5618	. . . . . . . . . 10 ⊢ (𝑤 = 𝐻 → ((𝑁 ∖ {𝑤}) × 𝑁) = ((𝑁 ∖ {𝐻}) × 𝑁))
53	52	reseq2d 5891	. . . . . . . . 9 ⊢ (𝑤 = 𝐻 → (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))
54	52	reseq2d 5891	. . . . . . . . 9 ⊢ (𝑤 = 𝐻 → (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))
55	53, 54	eqeq12d 2754	. . . . . . . 8 ⊢ (𝑤 = 𝐻 → ((𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ↔ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))))
56	52	reseq2d 5891	. . . . . . . . 9 ⊢ (𝑤 = 𝐻 → (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))
57	53, 56	eqeq12d 2754	. . . . . . . 8 ⊢ (𝑤 = 𝐻 → ((𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ↔ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))))
58	50, 55, 57	3anbi123d 1435	. . . . . . 7 ⊢ (𝑤 = 𝐻 → (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘_f + (𝐺 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) ↔ ((𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘_f + (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))))
59	58	imbi1d 342	. . . . . 6 ⊢ (𝑤 = 𝐻 → ((((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘_f + (𝐺 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = ((𝐷‘𝐹) + (𝐷‘𝐺))) ↔ (((𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘_f + (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → (𝐷‘𝐸) = ((𝐷‘𝐹) + (𝐷‘𝐺)))))
60	43, 59	rspc2va 3571	. . . . 5 ⊢ (((𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁) ∧ ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝐸 ↾ ({𝑤} × 𝑁)) = ((𝐹 ↾ ({𝑤} × 𝑁)) ∘_f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝐸) = ((𝐷‘𝐹) + (𝐷‘𝑧)))) → (((𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘_f + (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → (𝐷‘𝐸) = ((𝐷‘𝐹) + (𝐷‘𝐺))))
61	4, 5, 33, 60	syl21anc 835	. . . 4 ⊢ (((𝜑 ∧ 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵) ∧ (𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁)) → (((𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘_f + (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → (𝐷‘𝐸) = ((𝐷‘𝐹) + (𝐷‘𝐺))))
62	61	3adantr3 1170	. . 3 ⊢ (((𝜑 ∧ 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵) ∧ (𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘_f + (𝐺 ↾ ({𝐻} × 𝑁))))) → (((𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘_f + (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → (𝐷‘𝐸) = ((𝐷‘𝐹) + (𝐷‘𝐺))))
63	62	3adant3 1131	. 2 ⊢ (((𝜑 ∧ 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵) ∧ (𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘_f + (𝐺 ↾ ({𝐻} × 𝑁)))) ∧ ((𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (((𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘_f + (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁))) → (𝐷‘𝐸) = ((𝐷‘𝐹) + (𝐷‘𝐺))))
64	1, 2, 3, 63	mp3and 1463	1 ⊢ (((𝜑 ∧ 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵) ∧ (𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘_f + (𝐺 ↾ ({𝐻} × 𝑁)))) ∧ ((𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (𝐷‘𝐸) = ((𝐷‘𝐹) + (𝐷‘𝐺)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 ≠ wne 2943 ∀wral 3064 ∖ cdif 3884 {csn 4561 × cxp 5587 ↾ cres 5591 ⟶wf 6429 ‘cfv 6433 (class class class)co 7275 ∘_f cof 7531 Fincfn 8733 Basecbs 16912 +_gcplusg 16962 ._rcmulr 16963 0_gc0g 17150 1_rcur 19737 Ringcrg 19783 Mat cmat 21554

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-ral 3069 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-br 5075 df-opab 5137 df-xp 5595 df-res 5601 df-iota 6391 df-fv 6441 df-ov 7278

This theorem is referenced by: mdetunilem5 21765 mdetuni0 21770

W3C validator