This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 · ( 𝐺 ↾ ( { 𝐻 } × 𝑁 ) ) ) ∧ ( 𝐸 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) = ( 𝐺 ↾ ( ( 𝑁 ∖ { 𝐻 } ) × 𝑁 ) ) ) ) → ( 𝐷 ‘ 𝐸 ) = ( 𝐹 · ( 𝐷 ‘ 𝐺 ) ) )