mdetunilem4

	Ref	Expression
Hypotheses	mdetuni.a	$⊢ A = N Mat R$
	mdetuni.b	$⊢ B = {Base}_{A}$
	mdetuni.k	$⊢ K = {Base}_{R}$
	mdetuni.0g	$⊢ \underset{˙}{0} = 0_{R}$
	mdetuni.1r	$⊢ \underset{˙}{1} = 1_{R}$
	mdetuni.pg	$⊢ \underset{˙}{+} = +_{R}$
	mdetuni.tg	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	mdetuni.n	$⊢ φ \to N \in Fin$
	mdetuni.r	$⊢ φ \to R \in Ring$
	mdetuni.ff	$⊢ φ \to D : B ⟶ K$
	mdetuni.al	$⊢ φ \to \forall x \in B \forall y \in N \forall z \in N ((y \neq z \land \forall w \in N y x w = z x w) \to D (x) = \underset{˙}{0})$
	mdetuni.li	$⊢ φ \to \forall x \in B \forall y \in B \forall z \in B \forall w \in N (({x ↾}_{(\{w\} \times N)} = ({y ↾}_{(\{w\} \times N)}) {\underset{˙}{+}}_{f} ({z ↾}_{(\{w\} \times N)}) \land {x ↾}_{((N ∖ \{w\}) \times N)} = {y ↾}_{((N ∖ \{w\}) \times N)} \land {x ↾}_{((N ∖ \{w\}) \times N)} = {z ↾}_{((N ∖ \{w\}) \times N)}) \to D (x) = D (y) \underset{˙}{+} D (z))$
	mdetuni.sc	$⊢ φ \to \forall x \in B \forall y \in K \forall z \in B \forall w \in N (({x ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{y\}) {\underset{˙}{\cdot}}_{f} ({z ↾}_{(\{w\} \times N)}) \land {x ↾}_{((N ∖ \{w\}) \times N)} = {z ↾}_{((N ∖ \{w\}) \times N)}) \to D (x) = y \underset{˙}{\cdot} D (z))$
Assertion	mdetunilem4	$⊢ (φ \land (E \in B \land F \in K \land G \in B) \land (H \in N \land {E ↾}_{(\{H\} \times N)} = ((\{H\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({G ↾}_{(\{H\} \times N)}) \land {E ↾}_{((N ∖ \{H\}) \times N)} = {G ↾}_{((N ∖ \{H\}) \times N)})) \to D (E) = F \underset{˙}{\cdot} D (G)$

Proof

Step	Hyp	Ref	Expression
1		mdetuni.a	$⊢ A = N Mat R$
2		mdetuni.b	$⊢ B = {Base}_{A}$
3		mdetuni.k	$⊢ K = {Base}_{R}$
4		mdetuni.0g	$⊢ \underset{˙}{0} = 0_{R}$
5		mdetuni.1r	$⊢ \underset{˙}{1} = 1_{R}$
6		mdetuni.pg	$⊢ \underset{˙}{+} = +_{R}$
7		mdetuni.tg	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
8		mdetuni.n	$⊢ φ \to N \in Fin$
9		mdetuni.r	$⊢ φ \to R \in Ring$
10		mdetuni.ff	$⊢ φ \to D : B ⟶ K$
11		mdetuni.al	$⊢ φ \to \forall x \in B \forall y \in N \forall z \in N ((y \neq z \land \forall w \in N y x w = z x w) \to D (x) = \underset{˙}{0})$
12		mdetuni.li	$⊢ φ \to \forall x \in B \forall y \in B \forall z \in B \forall w \in N (({x ↾}_{(\{w\} \times N)} = ({y ↾}_{(\{w\} \times N)}) {\underset{˙}{+}}_{f} ({z ↾}_{(\{w\} \times N)}) \land {x ↾}_{((N ∖ \{w\}) \times N)} = {y ↾}_{((N ∖ \{w\}) \times N)} \land {x ↾}_{((N ∖ \{w\}) \times N)} = {z ↾}_{((N ∖ \{w\}) \times N)}) \to D (x) = D (y) \underset{˙}{+} D (z))$
13		mdetuni.sc	$⊢ φ \to \forall x \in B \forall y \in K \forall z \in B \forall w \in N (({x ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{y\}) {\underset{˙}{\cdot}}_{f} ({z ↾}_{(\{w\} \times N)}) \land {x ↾}_{((N ∖ \{w\}) \times N)} = {z ↾}_{((N ∖ \{w\}) \times N)}) \to D (x) = y \underset{˙}{\cdot} D (z))$
14		simp32	$⊢ (φ \land (E \in B \land F \in K \land G \in B) \land (H \in N \land {E ↾}_{(\{H\} \times N)} = ((\{H\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({G ↾}_{(\{H\} \times N)}) \land {E ↾}_{((N ∖ \{H\}) \times N)} = {G ↾}_{((N ∖ \{H\}) \times N)})) \to {E ↾}_{(\{H\} \times N)} = ((\{H\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({G ↾}_{(\{H\} \times N)})$
15		simp33	$⊢ (φ \land (E \in B \land F \in K \land G \in B) \land (H \in N \land {E ↾}_{(\{H\} \times N)} = ((\{H\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({G ↾}_{(\{H\} \times N)}) \land {E ↾}_{((N ∖ \{H\}) \times N)} = {G ↾}_{((N ∖ \{H\}) \times N)})) \to {E ↾}_{((N ∖ \{H\}) \times N)} = {G ↾}_{((N ∖ \{H\}) \times N)}$
16		simp1	$⊢ (H \in N \land {E ↾}_{(\{H\} \times N)} = ((\{H\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({G ↾}_{(\{H\} \times N)}) \land {E ↾}_{((N ∖ \{H\}) \times N)} = {G ↾}_{((N ∖ \{H\}) \times N)}) \to H \in N$
17		simp23	$⊢ (φ \land (E \in B \land F \in K \land G \in B) \land H \in N) \to G \in B$
18		simp3	$⊢ (φ \land (E \in B \land F \in K \land G \in B) \land H \in N) \to H \in N$
19		simp21	$⊢ (φ \land (E \in B \land F \in K \land G \in B) \land H \in N) \to E \in B$
20		simp22	$⊢ (φ \land (E \in B \land F \in K \land G \in B) \land H \in N) \to F \in K$
21	13	3ad2ant1	$⊢ (φ \land (E \in B \land F \in K \land G \in B) \land H \in N) \to \forall x \in B \forall y \in K \forall z \in B \forall w \in N (({x ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{y\}) {\underset{˙}{\cdot}}_{f} ({z ↾}_{(\{w\} \times N)}) \land {x ↾}_{((N ∖ \{w\}) \times N)} = {z ↾}_{((N ∖ \{w\}) \times N)}) \to D (x) = y \underset{˙}{\cdot} D (z))$
22		reseq1	$⊢ x = E \to {x ↾}_{(\{w\} \times N)} = {E ↾}_{(\{w\} \times N)}$
23	22	eqeq1d	$⊢ x = E \to ({x ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{y\}) {\underset{˙}{\cdot}}_{f} ({z ↾}_{(\{w\} \times N)}) \leftrightarrow {E ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{y\}) {\underset{˙}{\cdot}}_{f} ({z ↾}_{(\{w\} \times N)}))$
24		reseq1	$⊢ x = E \to {x ↾}_{((N ∖ \{w\}) \times N)} = {E ↾}_{((N ∖ \{w\}) \times N)}$
25	24	eqeq1d	$⊢ x = E \to ({x ↾}_{((N ∖ \{w\}) \times N)} = {z ↾}_{((N ∖ \{w\}) \times N)} \leftrightarrow {E ↾}_{((N ∖ \{w\}) \times N)} = {z ↾}_{((N ∖ \{w\}) \times N)})$
26	23 25	anbi12d	$⊢ x = E \to (({x ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{y\}) {\underset{˙}{\cdot}}_{f} ({z ↾}_{(\{w\} \times N)}) \land {x ↾}_{((N ∖ \{w\}) \times N)} = {z ↾}_{((N ∖ \{w\}) \times N)}) \leftrightarrow ({E ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{y\}) {\underset{˙}{\cdot}}_{f} ({z ↾}_{(\{w\} \times N)}) \land {E ↾}_{((N ∖ \{w\}) \times N)} = {z ↾}_{((N ∖ \{w\}) \times N)}))$
27		fveqeq2	$⊢ x = E \to (D (x) = y \underset{˙}{\cdot} D (z) \leftrightarrow D (E) = y \underset{˙}{\cdot} D (z))$
28	26 27	imbi12d	$⊢ x = E \to ((({x ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{y\}) {\underset{˙}{\cdot}}_{f} ({z ↾}_{(\{w\} \times N)}) \land {x ↾}_{((N ∖ \{w\}) \times N)} = {z ↾}_{((N ∖ \{w\}) \times N)}) \to D (x) = y \underset{˙}{\cdot} D (z)) \leftrightarrow (({E ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{y\}) {\underset{˙}{\cdot}}_{f} ({z ↾}_{(\{w\} \times N)}) \land {E ↾}_{((N ∖ \{w\}) \times N)} = {z ↾}_{((N ∖ \{w\}) \times N)}) \to D (E) = y \underset{˙}{\cdot} D (z)))$
29	28	2ralbidv	$⊢ x = E \to (\forall z \in B \forall w \in N (({x ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{y\}) {\underset{˙}{\cdot}}_{f} ({z ↾}_{(\{w\} \times N)}) \land {x ↾}_{((N ∖ \{w\}) \times N)} = {z ↾}_{((N ∖ \{w\}) \times N)}) \to D (x) = y \underset{˙}{\cdot} D (z)) \leftrightarrow \forall z \in B \forall w \in N (({E ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{y\}) {\underset{˙}{\cdot}}_{f} ({z ↾}_{(\{w\} \times N)}) \land {E ↾}_{((N ∖ \{w\}) \times N)} = {z ↾}_{((N ∖ \{w\}) \times N)}) \to D (E) = y \underset{˙}{\cdot} D (z)))$
30		sneq	$⊢ y = F \to \{y\} = \{F\}$
31	30	xpeq2d	$⊢ y = F \to (\{w\} \times N) \times \{y\} = (\{w\} \times N) \times \{F\}$
32	31	oveq1d	$⊢ y = F \to ((\{w\} \times N) \times \{y\}) {\underset{˙}{\cdot}}_{f} ({z ↾}_{(\{w\} \times N)}) = ((\{w\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({z ↾}_{(\{w\} \times N)})$
33	32	eqeq2d	$⊢ y = F \to ({E ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{y\}) {\underset{˙}{\cdot}}_{f} ({z ↾}_{(\{w\} \times N)}) \leftrightarrow {E ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({z ↾}_{(\{w\} \times N)}))$
34	33	anbi1d	$⊢ y = F \to (({E ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{y\}) {\underset{˙}{\cdot}}_{f} ({z ↾}_{(\{w\} \times N)}) \land {E ↾}_{((N ∖ \{w\}) \times N)} = {z ↾}_{((N ∖ \{w\}) \times N)}) \leftrightarrow ({E ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({z ↾}_{(\{w\} \times N)}) \land {E ↾}_{((N ∖ \{w\}) \times N)} = {z ↾}_{((N ∖ \{w\}) \times N)}))$
35		oveq1	$⊢ y = F \to y \underset{˙}{\cdot} D (z) = F \underset{˙}{\cdot} D (z)$
36	35	eqeq2d	$⊢ y = F \to (D (E) = y \underset{˙}{\cdot} D (z) \leftrightarrow D (E) = F \underset{˙}{\cdot} D (z))$
37	34 36	imbi12d	$⊢ y = F \to ((({E ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{y\}) {\underset{˙}{\cdot}}_{f} ({z ↾}_{(\{w\} \times N)}) \land {E ↾}_{((N ∖ \{w\}) \times N)} = {z ↾}_{((N ∖ \{w\}) \times N)}) \to D (E) = y \underset{˙}{\cdot} D (z)) \leftrightarrow (({E ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({z ↾}_{(\{w\} \times N)}) \land {E ↾}_{((N ∖ \{w\}) \times N)} = {z ↾}_{((N ∖ \{w\}) \times N)}) \to D (E) = F \underset{˙}{\cdot} D (z)))$
38	37	2ralbidv	$⊢ y = F \to (\forall z \in B \forall w \in N (({E ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{y\}) {\underset{˙}{\cdot}}_{f} ({z ↾}_{(\{w\} \times N)}) \land {E ↾}_{((N ∖ \{w\}) \times N)} = {z ↾}_{((N ∖ \{w\}) \times N)}) \to D (E) = y \underset{˙}{\cdot} D (z)) \leftrightarrow \forall z \in B \forall w \in N (({E ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({z ↾}_{(\{w\} \times N)}) \land {E ↾}_{((N ∖ \{w\}) \times N)} = {z ↾}_{((N ∖ \{w\}) \times N)}) \to D (E) = F \underset{˙}{\cdot} D (z)))$
39	29 38	rspc2va	$⊢ ((E \in B \land F \in K) \land \forall x \in B \forall y \in K \forall z \in B \forall w \in N (({x ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{y\}) {\underset{˙}{\cdot}}_{f} ({z ↾}_{(\{w\} \times N)}) \land {x ↾}_{((N ∖ \{w\}) \times N)} = {z ↾}_{((N ∖ \{w\}) \times N)}) \to D (x) = y \underset{˙}{\cdot} D (z))) \to \forall z \in B \forall w \in N (({E ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({z ↾}_{(\{w\} \times N)}) \land {E ↾}_{((N ∖ \{w\}) \times N)} = {z ↾}_{((N ∖ \{w\}) \times N)}) \to D (E) = F \underset{˙}{\cdot} D (z))$
40	19 20 21 39	syl21anc	$⊢ (φ \land (E \in B \land F \in K \land G \in B) \land H \in N) \to \forall z \in B \forall w \in N (({E ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({z ↾}_{(\{w\} \times N)}) \land {E ↾}_{((N ∖ \{w\}) \times N)} = {z ↾}_{((N ∖ \{w\}) \times N)}) \to D (E) = F \underset{˙}{\cdot} D (z))$
41		reseq1	$⊢ z = G \to {z ↾}_{(\{w\} \times N)} = {G ↾}_{(\{w\} \times N)}$
42	41	oveq2d	$⊢ z = G \to ((\{w\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({z ↾}_{(\{w\} \times N)}) = ((\{w\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({G ↾}_{(\{w\} \times N)})$
43	42	eqeq2d	$⊢ z = G \to ({E ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({z ↾}_{(\{w\} \times N)}) \leftrightarrow {E ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({G ↾}_{(\{w\} \times N)}))$
44		reseq1	$⊢ z = G \to {z ↾}_{((N ∖ \{w\}) \times N)} = {G ↾}_{((N ∖ \{w\}) \times N)}$
45	44	eqeq2d	$⊢ z = G \to ({E ↾}_{((N ∖ \{w\}) \times N)} = {z ↾}_{((N ∖ \{w\}) \times N)} \leftrightarrow {E ↾}_{((N ∖ \{w\}) \times N)} = {G ↾}_{((N ∖ \{w\}) \times N)})$
46	43 45	anbi12d	$⊢ z = G \to (({E ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({z ↾}_{(\{w\} \times N)}) \land {E ↾}_{((N ∖ \{w\}) \times N)} = {z ↾}_{((N ∖ \{w\}) \times N)}) \leftrightarrow ({E ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({G ↾}_{(\{w\} \times N)}) \land {E ↾}_{((N ∖ \{w\}) \times N)} = {G ↾}_{((N ∖ \{w\}) \times N)}))$
47		fveq2	$⊢ z = G \to D (z) = D (G)$
48	47	oveq2d	$⊢ z = G \to F \underset{˙}{\cdot} D (z) = F \underset{˙}{\cdot} D (G)$
49	48	eqeq2d	$⊢ z = G \to (D (E) = F \underset{˙}{\cdot} D (z) \leftrightarrow D (E) = F \underset{˙}{\cdot} D (G))$
50	46 49	imbi12d	$⊢ z = G \to ((({E ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({z ↾}_{(\{w\} \times N)}) \land {E ↾}_{((N ∖ \{w\}) \times N)} = {z ↾}_{((N ∖ \{w\}) \times N)}) \to D (E) = F \underset{˙}{\cdot} D (z)) \leftrightarrow (({E ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({G ↾}_{(\{w\} \times N)}) \land {E ↾}_{((N ∖ \{w\}) \times N)} = {G ↾}_{((N ∖ \{w\}) \times N)}) \to D (E) = F \underset{˙}{\cdot} D (G)))$
51		sneq	$⊢ w = H \to \{w\} = \{H\}$
52	51	xpeq1d	$⊢ w = H \to \{w\} \times N = \{H\} \times N$
53	52	reseq2d	$⊢ w = H \to {E ↾}_{(\{w\} \times N)} = {E ↾}_{(\{H\} \times N)}$
54	52	xpeq1d	$⊢ w = H \to (\{w\} \times N) \times \{F\} = (\{H\} \times N) \times \{F\}$
55	52	reseq2d	$⊢ w = H \to {G ↾}_{(\{w\} \times N)} = {G ↾}_{(\{H\} \times N)}$
56	54 55	oveq12d	$⊢ w = H \to ((\{w\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({G ↾}_{(\{w\} \times N)}) = ((\{H\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({G ↾}_{(\{H\} \times N)})$
57	53 56	eqeq12d	$⊢ w = H \to ({E ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({G ↾}_{(\{w\} \times N)}) \leftrightarrow {E ↾}_{(\{H\} \times N)} = ((\{H\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({G ↾}_{(\{H\} \times N)}))$
58	51	difeq2d	$⊢ w = H \to N ∖ \{w\} = N ∖ \{H\}$
59	58	xpeq1d	$⊢ w = H \to (N ∖ \{w\}) \times N = (N ∖ \{H\}) \times N$
60	59	reseq2d	$⊢ w = H \to {E ↾}_{((N ∖ \{w\}) \times N)} = {E ↾}_{((N ∖ \{H\}) \times N)}$
61	59	reseq2d	$⊢ w = H \to {G ↾}_{((N ∖ \{w\}) \times N)} = {G ↾}_{((N ∖ \{H\}) \times N)}$
62	60 61	eqeq12d	$⊢ w = H \to ({E ↾}_{((N ∖ \{w\}) \times N)} = {G ↾}_{((N ∖ \{w\}) \times N)} \leftrightarrow {E ↾}_{((N ∖ \{H\}) \times N)} = {G ↾}_{((N ∖ \{H\}) \times N)})$
63	57 62	anbi12d	$⊢ w = H \to (({E ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({G ↾}_{(\{w\} \times N)}) \land {E ↾}_{((N ∖ \{w\}) \times N)} = {G ↾}_{((N ∖ \{w\}) \times N)}) \leftrightarrow ({E ↾}_{(\{H\} \times N)} = ((\{H\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({G ↾}_{(\{H\} \times N)}) \land {E ↾}_{((N ∖ \{H\}) \times N)} = {G ↾}_{((N ∖ \{H\}) \times N)}))$
64	63	imbi1d	$⊢ w = H \to ((({E ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({G ↾}_{(\{w\} \times N)}) \land {E ↾}_{((N ∖ \{w\}) \times N)} = {G ↾}_{((N ∖ \{w\}) \times N)}) \to D (E) = F \underset{˙}{\cdot} D (G)) \leftrightarrow (({E ↾}_{(\{H\} \times N)} = ((\{H\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({G ↾}_{(\{H\} \times N)}) \land {E ↾}_{((N ∖ \{H\}) \times N)} = {G ↾}_{((N ∖ \{H\}) \times N)}) \to D (E) = F \underset{˙}{\cdot} D (G)))$
65	50 64	rspc2va	$⊢ ((G \in B \land H \in N) \land \forall z \in B \forall w \in N (({E ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({z ↾}_{(\{w\} \times N)}) \land {E ↾}_{((N ∖ \{w\}) \times N)} = {z ↾}_{((N ∖ \{w\}) \times N)}) \to D (E) = F \underset{˙}{\cdot} D (z))) \to (({E ↾}_{(\{H\} \times N)} = ((\{H\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({G ↾}_{(\{H\} \times N)}) \land {E ↾}_{((N ∖ \{H\}) \times N)} = {G ↾}_{((N ∖ \{H\}) \times N)}) \to D (E) = F \underset{˙}{\cdot} D (G))$
66	17 18 40 65	syl21anc	$⊢ (φ \land (E \in B \land F \in K \land G \in B) \land H \in N) \to (({E ↾}_{(\{H\} \times N)} = ((\{H\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({G ↾}_{(\{H\} \times N)}) \land {E ↾}_{((N ∖ \{H\}) \times N)} = {G ↾}_{((N ∖ \{H\}) \times N)}) \to D (E) = F \underset{˙}{\cdot} D (G))$
67	16 66	syl3an3	$⊢ (φ \land (E \in B \land F \in K \land G \in B) \land (H \in N \land {E ↾}_{(\{H\} \times N)} = ((\{H\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({G ↾}_{(\{H\} \times N)}) \land {E ↾}_{((N ∖ \{H\}) \times N)} = {G ↾}_{((N ∖ \{H\}) \times N)})) \to (({E ↾}_{(\{H\} \times N)} = ((\{H\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({G ↾}_{(\{H\} \times N)}) \land {E ↾}_{((N ∖ \{H\}) \times N)} = {G ↾}_{((N ∖ \{H\}) \times N)}) \to D (E) = F \underset{˙}{\cdot} D (G))$
68	14 15 67	mp2and	$⊢ (φ \land (E \in B \land F \in K \land G \in B) \land (H \in N \land {E ↾}_{(\{H\} \times N)} = ((\{H\} \times N) \times \{F\}) {\underset{˙}{\cdot}}_{f} ({G ↾}_{(\{H\} \times N)}) \land {E ↾}_{((N ∖ \{H\}) \times N)} = {G ↾}_{((N ∖ \{H\}) \times N)})) \to D (E) = F \underset{˙}{\cdot} D (G)$

Metamath Proof Explorer

Theorem mdetunilem4

Proof