ma1repveval

Description: An entry of an identity matrix with a replaced column. (Contributed by AV, 16-Feb-2019) (Revised by AV, 26-Feb-2019)

	Ref	Expression
Hypotheses	marepvcl.a	$⊢ A = N Mat R$
	marepvcl.b	$⊢ B = {Base}_{A}$
	marepvcl.v	$⊢ V = {Base}_{R}^{N}$
	ma1repvcl.1	$⊢ \underset{˙}{1} = 1_{A}$
	mulmarep1el.0	$⊢ \underset{˙}{0} = 0_{R}$
	mulmarep1el.e	$⊢ E = (\underset{˙}{1} (N matRepV R) C) (K)$
Assertion	ma1repveval	$⊢ (R \in Ring \land (M \in B \land C \in V \land K \in N) \land (I \in N \land J \in N)) \to I E J = if (J = K, C (I), if (J = I, 1_{R}, \underset{˙}{0}))$

Proof

Step	Hyp	Ref	Expression
1		marepvcl.a	$⊢ A = N Mat R$
2		marepvcl.b	$⊢ B = {Base}_{A}$
3		marepvcl.v	$⊢ V = {Base}_{R}^{N}$
4		ma1repvcl.1	$⊢ \underset{˙}{1} = 1_{A}$
5		mulmarep1el.0	$⊢ \underset{˙}{0} = 0_{R}$
6		mulmarep1el.e	$⊢ E = (\underset{˙}{1} (N matRepV R) C) (K)$
7	1 2	matrcl	$⊢ M \in B \to (N \in Fin \land R \in V)$
8	7	simpld	$⊢ M \in B \to N \in Fin$
9	1	fveq2i	$⊢ 1_{A} = 1_{(N Mat R)}$
10	4 9	eqtri	$⊢ \underset{˙}{1} = 1_{(N Mat R)}$
11	1 2 10	mat1bas	$⊢ (R \in Ring \land N \in Fin) \to \underset{˙}{1} \in B$
12	11	expcom	$⊢ N \in Fin \to (R \in Ring \to \underset{˙}{1} \in B)$
13	8 12	syl	$⊢ M \in B \to (R \in Ring \to \underset{˙}{1} \in B)$
14	13	3ad2ant1	$⊢ (M \in B \land C \in V \land K \in N) \to (R \in Ring \to \underset{˙}{1} \in B)$
15	14	impcom	$⊢ (R \in Ring \land (M \in B \land C \in V \land K \in N)) \to \underset{˙}{1} \in B$
16		simpr2	$⊢ (R \in Ring \land (M \in B \land C \in V \land K \in N)) \to C \in V$
17		simpr3	$⊢ (R \in Ring \land (M \in B \land C \in V \land K \in N)) \to K \in N$
18	15 16 17	3jca	$⊢ (R \in Ring \land (M \in B \land C \in V \land K \in N)) \to (\underset{˙}{1} \in B \land C \in V \land K \in N)$
19	6	a1i	$⊢ ((\underset{˙}{1} \in B \land C \in V \land K \in N) \land (I \in N \land J \in N)) \to E = (\underset{˙}{1} (N matRepV R) C) (K)$
20	19	oveqd	$⊢ ((\underset{˙}{1} \in B \land C \in V \land K \in N) \land (I \in N \land J \in N)) \to I E J = I (\underset{˙}{1} (N matRepV R) C) (K) J$
21		eqid	$⊢ N matRepV R = N matRepV R$
22	1 2 21 3	marepveval	$⊢ ((\underset{˙}{1} \in B \land C \in V \land K \in N) \land (I \in N \land J \in N)) \to I (\underset{˙}{1} (N matRepV R) C) (K) J = if (J = K, C (I), I \underset{˙}{1} J)$
23	20 22	eqtrd	$⊢ ((\underset{˙}{1} \in B \land C \in V \land K \in N) \land (I \in N \land J \in N)) \to I E J = if (J = K, C (I), I \underset{˙}{1} J)$
24	18 23	stoic3	$⊢ (R \in Ring \land (M \in B \land C \in V \land K \in N) \land (I \in N \land J \in N)) \to I E J = if (J = K, C (I), I \underset{˙}{1} J)$
25		eqid	$⊢ 1_{R} = 1_{R}$
26	8	3ad2ant1	$⊢ (M \in B \land C \in V \land K \in N) \to N \in Fin$
27	26	3ad2ant2	$⊢ (R \in Ring \land (M \in B \land C \in V \land K \in N) \land (I \in N \land J \in N)) \to N \in Fin$
28		simp1	$⊢ (R \in Ring \land (M \in B \land C \in V \land K \in N) \land (I \in N \land J \in N)) \to R \in Ring$
29		simp3l	$⊢ (R \in Ring \land (M \in B \land C \in V \land K \in N) \land (I \in N \land J \in N)) \to I \in N$
30		simp3r	$⊢ (R \in Ring \land (M \in B \land C \in V \land K \in N) \land (I \in N \land J \in N)) \to J \in N$
31	1 25 5 27 28 29 30 4	mat1ov	$⊢ (R \in Ring \land (M \in B \land C \in V \land K \in N) \land (I \in N \land J \in N)) \to I \underset{˙}{1} J = if (I = J, 1_{R}, \underset{˙}{0})$
32		eqcom	$⊢ I = J \leftrightarrow J = I$
33	32	a1i	$⊢ (R \in Ring \land (M \in B \land C \in V \land K \in N) \land (I \in N \land J \in N)) \to (I = J \leftrightarrow J = I)$
34	33	ifbid	$⊢ (R \in Ring \land (M \in B \land C \in V \land K \in N) \land (I \in N \land J \in N)) \to if (I = J, 1_{R}, \underset{˙}{0}) = if (J = I, 1_{R}, \underset{˙}{0})$
35	31 34	eqtrd	$⊢ (R \in Ring \land (M \in B \land C \in V \land K \in N) \land (I \in N \land J \in N)) \to I \underset{˙}{1} J = if (J = I, 1_{R}, \underset{˙}{0})$
36	35	ifeq2d	$⊢ (R \in Ring \land (M \in B \land C \in V \land K \in N) \land (I \in N \land J \in N)) \to if (J = K, C (I), I \underset{˙}{1} J) = if (J = K, C (I), if (J = I, 1_{R}, \underset{˙}{0}))$
37	24 36	eqtrd	$⊢ (R \in Ring \land (M \in B \land C \in V \land K \in N) \land (I \in N \land J \in N)) \to I E J = if (J = K, C (I), if (J = I, 1_{R}, \underset{˙}{0}))$

Metamath Proof Explorer

Theorem ma1repveval

Proof