Metamath Proof Explorer

Theorem matepm2cl

Description: Each entry of a matrix with an index as permutation of the other is an element of the underlying ring. (Contributed by AV, 1-Jan-2019)

		Ref	Expression
	Hypotheses	matepmcl.a	$⊢ A = N Mat R$
		matepmcl.b	$⊢ B = {Base}_{A}$
		matepmcl.p	$⊢ P = {Base}_{SymGrp (N)}$
	Assertion	matepm2cl	$⊢ (R \in Ring \land Q \in P \land M \in B) \to \forall n \in N n M Q (n) \in {Base}_{R}$

Proof

Step	Hyp	Ref	Expression
1		matepmcl.a	$⊢ A = N Mat R$
2		matepmcl.b	$⊢ B = {Base}_{A}$
3		matepmcl.p	$⊢ P = {Base}_{SymGrp (N)}$
4		simpr	$⊢ ((R \in Ring \land Q \in P \land M \in B) \land n \in N) \to n \in N$
5		eqid	$⊢ SymGrp (N) = SymGrp (N)$
6	5 3	symgfv	$⊢ (Q \in P \land n \in N) \to Q (n) \in N$
7	6	3ad2antl2	$⊢ ((R \in Ring \land Q \in P \land M \in B) \land n \in N) \to Q (n) \in N$
8	2	eleq2i	$⊢ M \in B \leftrightarrow M \in {Base}_{A}$
9	8	biimpi	$⊢ M \in B \to M \in {Base}_{A}$
10	9	3ad2ant3	$⊢ (R \in Ring \land Q \in P \land M \in B) \to M \in {Base}_{A}$
11	10	adantr	$⊢ ((R \in Ring \land Q \in P \land M \in B) \land n \in N) \to M \in {Base}_{A}$
12		eqid	$⊢ {Base}_{R} = {Base}_{R}$
13	1 12	matecl	$⊢ (n \in N \land Q (n) \in N \land M \in {Base}_{A}) \to n M Q (n) \in {Base}_{R}$
14	4 7 11 13	syl3anc	$⊢ ((R \in Ring \land Q \in P \land M \in B) \land n \in N) \to n M Q (n) \in {Base}_{R}$
15	14	ralrimiva	$⊢ (R \in Ring \land Q \in P \land M \in B) \to \forall n \in N n M Q (n) \in {Base}_{R}$