mdetunilem1

	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	mdetunilem1	$⊢ ((φ \land E \in B \land \forall w \in N F E w = G E w) \land (F \in N \land G \in N \land F \neq G)) \to D (E) = \underset{˙}{0}$

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		simpr3	$⊢ ((φ \land E \in B \land \forall w \in N F E w = G E w) \land (F \in N \land G \in N \land F \neq G)) \to F \neq G$
15		simpl3	$⊢ ((φ \land E \in B \land \forall w \in N F E w = G E w) \land (F \in N \land G \in N \land F \neq G)) \to \forall w \in N F E w = G E w$
16		neeq2	$⊢ z = G \to (F \neq z \leftrightarrow F \neq G)$
17		oveq1	$⊢ z = G \to z E w = G E w$
18	17	eqeq2d	$⊢ z = G \to (F E w = z E w \leftrightarrow F E w = G E w)$
19	18	ralbidv	$⊢ z = G \to (\forall w \in N F E w = z E w \leftrightarrow \forall w \in N F E w = G E w)$
20	16 19	anbi12d	$⊢ z = G \to ((F \neq z \land \forall w \in N F E w = z E w) \leftrightarrow (F \neq G \land \forall w \in N F E w = G E w))$
21	20	imbi1d	$⊢ z = G \to (((F \neq z \land \forall w \in N F E w = z E w) \to D (E) = \underset{˙}{0}) \leftrightarrow ((F \neq G \land \forall w \in N F E w = G E w) \to D (E) = \underset{˙}{0}))$
22		simpl2	$⊢ ((φ \land E \in B \land \forall w \in N F E w = G E w) \land (F \in N \land G \in N \land F \neq G)) \to E \in B$
23		simpr1	$⊢ ((φ \land E \in B \land \forall w \in N F E w = G E w) \land (F \in N \land G \in N \land F \neq G)) \to F \in N$
24		simpl1	$⊢ ((φ \land E \in B \land \forall w \in N F E w = G E w) \land (F \in N \land G \in N \land F \neq G)) \to φ$
25	24 11	syl	$⊢ ((φ \land E \in B \land \forall w \in N F E w = G E w) \land (F \in N \land G \in N \land F \neq G)) \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})$
26		oveq	$⊢ x = E \to y x w = y E w$
27		oveq	$⊢ x = E \to z x w = z E w$
28	26 27	eqeq12d	$⊢ x = E \to (y x w = z x w \leftrightarrow y E w = z E w)$
29	28	ralbidv	$⊢ x = E \to (\forall w \in N y x w = z x w \leftrightarrow \forall w \in N y E w = z E w)$
30	29	anbi2d	$⊢ x = E \to ((y \neq z \land \forall w \in N y x w = z x w) \leftrightarrow (y \neq z \land \forall w \in N y E w = z E w))$
31		fveqeq2	$⊢ x = E \to (D (x) = \underset{˙}{0} \leftrightarrow D (E) = \underset{˙}{0})$
32	30 31	imbi12d	$⊢ x = E \to (((y \neq z \land \forall w \in N y x w = z x w) \to D (x) = \underset{˙}{0}) \leftrightarrow ((y \neq z \land \forall w \in N y E w = z E w) \to D (E) = \underset{˙}{0}))$
33	32	ralbidv	$⊢ x = E \to (\forall z \in N ((y \neq z \land \forall w \in N y x w = z x w) \to D (x) = \underset{˙}{0}) \leftrightarrow \forall z \in N ((y \neq z \land \forall w \in N y E w = z E w) \to D (E) = \underset{˙}{0}))$
34		neeq1	$⊢ y = F \to (y \neq z \leftrightarrow F \neq z)$
35		oveq1	$⊢ y = F \to y E w = F E w$
36	35	eqeq1d	$⊢ y = F \to (y E w = z E w \leftrightarrow F E w = z E w)$
37	36	ralbidv	$⊢ y = F \to (\forall w \in N y E w = z E w \leftrightarrow \forall w \in N F E w = z E w)$
38	34 37	anbi12d	$⊢ y = F \to ((y \neq z \land \forall w \in N y E w = z E w) \leftrightarrow (F \neq z \land \forall w \in N F E w = z E w))$
39	38	imbi1d	$⊢ y = F \to (((y \neq z \land \forall w \in N y E w = z E w) \to D (E) = \underset{˙}{0}) \leftrightarrow ((F \neq z \land \forall w \in N F E w = z E w) \to D (E) = \underset{˙}{0}))$
40	39	ralbidv	$⊢ y = F \to (\forall z \in N ((y \neq z \land \forall w \in N y E w = z E w) \to D (E) = \underset{˙}{0}) \leftrightarrow \forall z \in N ((F \neq z \land \forall w \in N F E w = z E w) \to D (E) = \underset{˙}{0}))$
41	33 40	rspc2va	$⊢ ((E \in B \land F \in N) \land \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})) \to \forall z \in N ((F \neq z \land \forall w \in N F E w = z E w) \to D (E) = \underset{˙}{0})$
42	22 23 25 41	syl21anc	$⊢ ((φ \land E \in B \land \forall w \in N F E w = G E w) \land (F \in N \land G \in N \land F \neq G)) \to \forall z \in N ((F \neq z \land \forall w \in N F E w = z E w) \to D (E) = \underset{˙}{0})$
43		simpr2	$⊢ ((φ \land E \in B \land \forall w \in N F E w = G E w) \land (F \in N \land G \in N \land F \neq G)) \to G \in N$
44	21 42 43	rspcdva	$⊢ ((φ \land E \in B \land \forall w \in N F E w = G E w) \land (F \in N \land G \in N \land F \neq G)) \to ((F \neq G \land \forall w \in N F E w = G E w) \to D (E) = \underset{˙}{0})$
45	14 15 44	mp2and	$⊢ ((φ \land E \in B \land \forall w \in N F E w = G E w) \land (F \in N \land G \in N \land F \neq G)) \to D (E) = \underset{˙}{0}$

Metamath Proof Explorer

Theorem mdetunilem1

Proof