Theorem mdetunilem4

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

	Ref	Expression
Hypotheses	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	mdetunilem4	⊢ ( ( 𝜑 ∧ ( 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝐻 ∈ 𝑁 ∧ ( 𝐸 ↾ ( { 𝐻 } × 𝑁 ) ) = ( ( ( { 𝐻 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝐺 ↾ ( { 𝐻 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( 𝐹 · ( 𝐷 ‘ 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mdetuni.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		mdetuni.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		mdetuni.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
4		mdetuni.0g	⊢ 0 = ( 0g ‘ 𝑅 )
5		mdetuni.1r	⊢ 1 = ( 1r ‘ 𝑅 )
6		mdetuni.pg	⊢ + = ( +g ‘ 𝑅 )
7		mdetuni.tg	⊢ · = ( .r ‘ 𝑅 )
8		mdetuni.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
9		mdetuni.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
10		mdetuni.ff	⊢ ( 𝜑 → 𝐷 : 𝐵 ⟶ 𝐾 )
11		mdetuni.al	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑁 ∀ 𝑧 ∈ 𝑁 ( ( 𝑦 ≠ 𝑧 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝑦 𝑥 𝑤 ) = ( 𝑧 𝑥 𝑤 ) ) → ( 𝐷 ‘ 𝑥 ) = 0 ) )
12		mdetuni.li	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝑥 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝑦 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑦 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝑥 ) = ( ( 𝐷 ‘ 𝑦 ) + ( 𝐷 ‘ 𝑧 ) ) ) )
13		mdetuni.sc	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝑥 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝑦 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝑥 ) = ( 𝑦 · ( 𝐷 ‘ 𝑧 ) ) ) )
14		simp32	⊢ ( ( 𝜑 ∧ ( 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝐻 ∈ 𝑁 ∧ ( 𝐸 ↾ ( { 𝐻 } × 𝑁 ) ) = ( ( ( { 𝐻 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝐺 ↾ ( { 𝐻 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ) ) → ( 𝐸 ↾ ( { 𝐻 } × 𝑁 ) ) = ( ( ( { 𝐻 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝐺 ↾ ( { 𝐻 } × 𝑁 ) ) ) )
15		simp33	⊢ ( ( 𝜑 ∧ ( 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝐻 ∈ 𝑁 ∧ ( 𝐸 ↾ ( { 𝐻 } × 𝑁 ) ) = ( ( ( { 𝐻 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝐺 ↾ ( { 𝐻 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ) ) → ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) )
16		simp1	⊢ ( ( 𝐻 ∈ 𝑁 ∧ ( 𝐸 ↾ ( { 𝐻 } × 𝑁 ) ) = ( ( ( { 𝐻 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝐺 ↾ ( { 𝐻 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ) → 𝐻 ∈ 𝑁 )
17		simp23	⊢ ( ( 𝜑 ∧ ( 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝐻 ∈ 𝑁 ) → 𝐺 ∈ 𝐵 )
18		simp3	⊢ ( ( 𝜑 ∧ ( 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝐻 ∈ 𝑁 ) → 𝐻 ∈ 𝑁 )
19		simp21	⊢ ( ( 𝜑 ∧ ( 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝐻 ∈ 𝑁 ) → 𝐸 ∈ 𝐵 )
20		simp22	⊢ ( ( 𝜑 ∧ ( 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝐻 ∈ 𝑁 ) → 𝐹 ∈ 𝐾 )
21	13	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝐻 ∈ 𝑁 ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝑥 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝑦 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝑥 ) = ( 𝑦 · ( 𝐷 ‘ 𝑧 ) ) ) )
22		reseq1	⊢ ( 𝑥 = 𝐸 → ( 𝑥 ↾ ( { 𝑤 } × 𝑁 ) ) = ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) )
23	22	eqeq1d	⊢ ( 𝑥 = 𝐸 → ( ( 𝑥 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝑦 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ↔ ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝑦 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ) )
24		reseq1	⊢ ( 𝑥 = 𝐸 → ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) )
25	24	eqeq1d	⊢ ( 𝑥 = 𝐸 → ( ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ↔ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) )
26	23 25	anbi12d	⊢ ( 𝑥 = 𝐸 → ( ( ( 𝑥 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝑦 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) ↔ ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝑦 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) ) )
27		fveqeq2	⊢ ( 𝑥 = 𝐸 → ( ( 𝐷 ‘ 𝑥 ) = ( 𝑦 · ( 𝐷 ‘ 𝑧 ) ) ↔ ( 𝐷 ‘ 𝐸 ) = ( 𝑦 · ( 𝐷 ‘ 𝑧 ) ) ) )
28	26 27	imbi12d	⊢ ( 𝑥 = 𝐸 → ( ( ( ( 𝑥 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝑦 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝑥 ) = ( 𝑦 · ( 𝐷 ‘ 𝑧 ) ) ) ↔ ( ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝑦 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( 𝑦 · ( 𝐷 ‘ 𝑧 ) ) ) ) )
29	28	2ralbidv	⊢ ( 𝑥 = 𝐸 → ( ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝑥 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝑦 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝑥 ) = ( 𝑦 · ( 𝐷 ‘ 𝑧 ) ) ) ↔ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝑦 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( 𝑦 · ( 𝐷 ‘ 𝑧 ) ) ) ) )
30		sneq	⊢ ( 𝑦 = 𝐹 → { 𝑦 } = { 𝐹 } )
31	30	xpeq2d	⊢ ( 𝑦 = 𝐹 → ( ( { 𝑤 } × 𝑁 ) × { 𝑦 } ) = ( ( { 𝑤 } × 𝑁 ) × { 𝐹 } ) )
32	31	oveq1d	⊢ ( 𝑦 = 𝐹 → ( ( ( { 𝑤 } × 𝑁 ) × { 𝑦 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) )
33	32	eqeq2d	⊢ ( 𝑦 = 𝐹 → ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝑦 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ↔ ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ) )
34	33	anbi1d	⊢ ( 𝑦 = 𝐹 → ( ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝑦 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) ↔ ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) ) )
35		oveq1	⊢ ( 𝑦 = 𝐹 → ( 𝑦 · ( 𝐷 ‘ 𝑧 ) ) = ( 𝐹 · ( 𝐷 ‘ 𝑧 ) ) )
36	35	eqeq2d	⊢ ( 𝑦 = 𝐹 → ( ( 𝐷 ‘ 𝐸 ) = ( 𝑦 · ( 𝐷 ‘ 𝑧 ) ) ↔ ( 𝐷 ‘ 𝐸 ) = ( 𝐹 · ( 𝐷 ‘ 𝑧 ) ) ) )
37	34 36	imbi12d	⊢ ( 𝑦 = 𝐹 → ( ( ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝑦 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( 𝑦 · ( 𝐷 ‘ 𝑧 ) ) ) ↔ ( ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( 𝐹 · ( 𝐷 ‘ 𝑧 ) ) ) ) )
38	37	2ralbidv	⊢ ( 𝑦 = 𝐹 → ( ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝑦 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( 𝑦 · ( 𝐷 ‘ 𝑧 ) ) ) ↔ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( 𝐹 · ( 𝐷 ‘ 𝑧 ) ) ) ) )
39	29 38	rspc2va	⊢ ( ( ( 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝑥 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝑦 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝑥 ) = ( 𝑦 · ( 𝐷 ‘ 𝑧 ) ) ) ) → ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( 𝐹 · ( 𝐷 ‘ 𝑧 ) ) ) )
40	19 20 21 39	syl21anc	⊢ ( ( 𝜑 ∧ ( 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝐻 ∈ 𝑁 ) → ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( 𝐹 · ( 𝐷 ‘ 𝑧 ) ) ) )
41		reseq1	⊢ ( 𝑧 = 𝐺 → ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) = ( 𝐺 ↾ ( { 𝑤 } × 𝑁 ) ) )
42	41	oveq2d	⊢ ( 𝑧 = 𝐺 → ( ( ( { 𝑤 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝐺 ↾ ( { 𝑤 } × 𝑁 ) ) ) )
43	42	eqeq2d	⊢ ( 𝑧 = 𝐺 → ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ↔ ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝐺 ↾ ( { 𝑤 } × 𝑁 ) ) ) ) )
44		reseq1	⊢ ( 𝑧 = 𝐺 → ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) )
45	44	eqeq2d	⊢ ( 𝑧 = 𝐺 → ( ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ↔ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) )
46	43 45	anbi12d	⊢ ( 𝑧 = 𝐺 → ( ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) ↔ ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝐺 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) ) )
47		fveq2	⊢ ( 𝑧 = 𝐺 → ( 𝐷 ‘ 𝑧 ) = ( 𝐷 ‘ 𝐺 ) )
48	47	oveq2d	⊢ ( 𝑧 = 𝐺 → ( 𝐹 · ( 𝐷 ‘ 𝑧 ) ) = ( 𝐹 · ( 𝐷 ‘ 𝐺 ) ) )
49	48	eqeq2d	⊢ ( 𝑧 = 𝐺 → ( ( 𝐷 ‘ 𝐸 ) = ( 𝐹 · ( 𝐷 ‘ 𝑧 ) ) ↔ ( 𝐷 ‘ 𝐸 ) = ( 𝐹 · ( 𝐷 ‘ 𝐺 ) ) ) )
50	46 49	imbi12d	⊢ ( 𝑧 = 𝐺 → ( ( ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( 𝐹 · ( 𝐷 ‘ 𝑧 ) ) ) ↔ ( ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝐺 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( 𝐹 · ( 𝐷 ‘ 𝐺 ) ) ) ) )
51		sneq	⊢ ( 𝑤 = 𝐻 → { 𝑤 } = { 𝐻 } )
52	51	xpeq1d	⊢ ( 𝑤 = 𝐻 → ( { 𝑤 } × 𝑁 ) = ( { 𝐻 } × 𝑁 ) )
53	52	reseq2d	⊢ ( 𝑤 = 𝐻 → ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( 𝐸 ↾ ( { 𝐻 } × 𝑁 ) ) )
54	52	xpeq1d	⊢ ( 𝑤 = 𝐻 → ( ( { 𝑤 } × 𝑁 ) × { 𝐹 } ) = ( ( { 𝐻 } × 𝑁 ) × { 𝐹 } ) )
55	52	reseq2d	⊢ ( 𝑤 = 𝐻 → ( 𝐺 ↾ ( { 𝑤 } × 𝑁 ) ) = ( 𝐺 ↾ ( { 𝐻 } × 𝑁 ) ) )
56	54 55	oveq12d	⊢ ( 𝑤 = 𝐻 → ( ( ( { 𝑤 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝐺 ↾ ( { 𝑤 } × 𝑁 ) ) ) = ( ( ( { 𝐻 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝐺 ↾ ( { 𝐻 } × 𝑁 ) ) ) )
57	53 56	eqeq12d	⊢ ( 𝑤 = 𝐻 → ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝐺 ↾ ( { 𝑤 } × 𝑁 ) ) ) ↔ ( 𝐸 ↾ ( { 𝐻 } × 𝑁 ) ) = ( ( ( { 𝐻 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝐺 ↾ ( { 𝐻 } × 𝑁 ) ) ) ) )
58	51	difeq2d	⊢ ( 𝑤 = 𝐻 → ( 𝑁 ∖ { 𝑤 } ) = ( 𝑁 ∖ { 𝐻 } ) )
59	58	xpeq1d	⊢ ( 𝑤 = 𝐻 → ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) = ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) )
60	59	reseq2d	⊢ ( 𝑤 = 𝐻 → ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) )
61	59	reseq2d	⊢ ( 𝑤 = 𝐻 → ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) )
62	60 61	eqeq12d	⊢ ( 𝑤 = 𝐻 → ( ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ↔ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ) )
63	57 62	anbi12d	⊢ ( 𝑤 = 𝐻 → ( ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝐺 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) ↔ ( ( 𝐸 ↾ ( { 𝐻 } × 𝑁 ) ) = ( ( ( { 𝐻 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝐺 ↾ ( { 𝐻 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ) ) )
64	63	imbi1d	⊢ ( 𝑤 = 𝐻 → ( ( ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝐺 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( 𝐹 · ( 𝐷 ‘ 𝐺 ) ) ) ↔ ( ( ( 𝐸 ↾ ( { 𝐻 } × 𝑁 ) ) = ( ( ( { 𝐻 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝐺 ↾ ( { 𝐻 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( 𝐹 · ( 𝐷 ‘ 𝐺 ) ) ) ) )
65	50 64	rspc2va	⊢ ( ( ( 𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁 ) ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝐸 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( 𝐹 · ( 𝐷 ‘ 𝑧 ) ) ) ) → ( ( ( 𝐸 ↾ ( { 𝐻 } × 𝑁 ) ) = ( ( ( { 𝐻 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝐺 ↾ ( { 𝐻 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( 𝐹 · ( 𝐷 ‘ 𝐺 ) ) ) )
66	17 18 40 65	syl21anc	⊢ ( ( 𝜑 ∧ ( 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝐻 ∈ 𝑁 ) → ( ( ( 𝐸 ↾ ( { 𝐻 } × 𝑁 ) ) = ( ( ( { 𝐻 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝐺 ↾ ( { 𝐻 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( 𝐹 · ( 𝐷 ‘ 𝐺 ) ) ) )
67	16 66	syl3an3	⊢ ( ( 𝜑 ∧ ( 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝐻 ∈ 𝑁 ∧ ( 𝐸 ↾ ( { 𝐻 } × 𝑁 ) ) = ( ( ( { 𝐻 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝐺 ↾ ( { 𝐻 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ) ) → ( ( ( 𝐸 ↾ ( { 𝐻 } × 𝑁 ) ) = ( ( ( { 𝐻 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝐺 ↾ ( { 𝐻 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( 𝐹 · ( 𝐷 ‘ 𝐺 ) ) ) )
68	14 15 67	mp2and	⊢ ( ( 𝜑 ∧ ( 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝐻 ∈ 𝑁 ∧ ( 𝐸 ↾ ( { 𝐻 } × 𝑁 ) ) = ( ( ( { 𝐻 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝐺 ↾ ( { 𝐻 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( 𝐹 · ( 𝐷 ‘ 𝐺 ) ) )