cpmatinvcl

Description: The set of all constant polynomial matrices over a ring R is closed under inversion. (Contributed by AV, 17-Nov-2019) (Proof shortened by AV, 28-Nov-2019)

	Ref	Expression
Hypotheses	cpmatsrngpmat.s	$⊢ S = N ConstPolyMat R$
	cpmatsrngpmat.p	$⊢ P = {Poly}_{1} (R)$
	cpmatsrngpmat.c	$⊢ C = N Mat P$
Assertion	cpmatinvcl	$⊢ (N \in Fin \land R \in Ring) \to \forall x \in S {inv}_{g} (C) (x) \in S$

Proof

Step	Hyp	Ref	Expression
1		cpmatsrngpmat.s	$⊢ S = N ConstPolyMat R$
2		cpmatsrngpmat.p	$⊢ P = {Poly}_{1} (R)$
3		cpmatsrngpmat.c	$⊢ C = N Mat P$
4		eqid	$⊢ {Base}_{C} = {Base}_{C}$
5		eqid	$⊢ {Base}_{R} = {Base}_{R}$
6		eqid	$⊢ algSc (P) = algSc (P)$
7	1 2 3 4 5 6	cpmatelimp2	$⊢ (N \in Fin \land R \in Ring) \to (x \in S \to (x \in {Base}_{C} \land \forall i \in N \forall j \in N \exists a \in {Base}_{R} i x j = algSc (P) (a)))$
8	2	ply1sca	$⊢ R \in Ring \to R = Scalar (P)$
9	8	adantl	$⊢ (N \in Fin \land R \in Ring) \to R = Scalar (P)$
10	9	adantr	$⊢ ((N \in Fin \land R \in Ring) \land a \in {Base}_{R}) \to R = Scalar (P)$
11	10	eqcomd	$⊢ ((N \in Fin \land R \in Ring) \land a \in {Base}_{R}) \to Scalar (P) = R$
12	11	fveq2d	$⊢ ((N \in Fin \land R \in Ring) \land a \in {Base}_{R}) \to {inv}_{g} (Scalar (P)) = {inv}_{g} (R)$
13	12	fveq1d	$⊢ ((N \in Fin \land R \in Ring) \land a \in {Base}_{R}) \to {inv}_{g} (Scalar (P)) (a) = {inv}_{g} (R) (a)$
14		ringgrp	$⊢ R \in Ring \to R \in Grp$
15	14	adantl	$⊢ (N \in Fin \land R \in Ring) \to R \in Grp$
16		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
17	5 16	grpinvcl	$⊢ (R \in Grp \land a \in {Base}_{R}) \to {inv}_{g} (R) (a) \in {Base}_{R}$
18	15 17	sylan	$⊢ ((N \in Fin \land R \in Ring) \land a \in {Base}_{R}) \to {inv}_{g} (R) (a) \in {Base}_{R}$
19	13 18	eqeltrd	$⊢ ((N \in Fin \land R \in Ring) \land a \in {Base}_{R}) \to {inv}_{g} (Scalar (P)) (a) \in {Base}_{R}$
20	19	ad5ant14	$⊢ (((((N \in Fin \land R \in Ring) \land x \in {Base}_{C}) \land (i \in N \land j \in N)) \land a \in {Base}_{R}) \land i x j = algSc (P) (a)) \to {inv}_{g} (Scalar (P)) (a) \in {Base}_{R}$
21		fveq2	$⊢ c = {inv}_{g} (Scalar (P)) (a) \to algSc (P) (c) = algSc (P) ({inv}_{g} (Scalar (P)) (a))$
22	21	eqeq2d	$⊢ c = {inv}_{g} (Scalar (P)) (a) \to (i {inv}_{g} (C) (x) j = algSc (P) (c) \leftrightarrow i {inv}_{g} (C) (x) j = algSc (P) ({inv}_{g} (Scalar (P)) (a)))$
23	22	adantl	$⊢ ((((((N \in Fin \land R \in Ring) \land x \in {Base}_{C}) \land (i \in N \land j \in N)) \land a \in {Base}_{R}) \land i x j = algSc (P) (a)) \land c = {inv}_{g} (Scalar (P)) (a)) \to (i {inv}_{g} (C) (x) j = algSc (P) (c) \leftrightarrow i {inv}_{g} (C) (x) j = algSc (P) ({inv}_{g} (Scalar (P)) (a)))$
24	2	ply1ring	$⊢ R \in Ring \to P \in Ring$
25	24	ad3antlr	$⊢ (((N \in Fin \land R \in Ring) \land x \in {Base}_{C}) \land (i \in N \land j \in N)) \to P \in Ring$
26		simplr	$⊢ (((N \in Fin \land R \in Ring) \land x \in {Base}_{C}) \land (i \in N \land j \in N)) \to x \in {Base}_{C}$
27		simpr	$⊢ (((N \in Fin \land R \in Ring) \land x \in {Base}_{C}) \land (i \in N \land j \in N)) \to (i \in N \land j \in N)$
28	25 26 27	3jca	$⊢ (((N \in Fin \land R \in Ring) \land x \in {Base}_{C}) \land (i \in N \land j \in N)) \to (P \in Ring \land x \in {Base}_{C} \land (i \in N \land j \in N))$
29	28	ad2antrr	$⊢ (((((N \in Fin \land R \in Ring) \land x \in {Base}_{C}) \land (i \in N \land j \in N)) \land a \in {Base}_{R}) \land i x j = algSc (P) (a)) \to (P \in Ring \land x \in {Base}_{C} \land (i \in N \land j \in N))$
30		eqid	$⊢ {inv}_{g} (P) = {inv}_{g} (P)$
31		eqid	$⊢ {inv}_{g} (C) = {inv}_{g} (C)$
32	3 4 30 31	matinvgcell	$⊢ (P \in Ring \land x \in {Base}_{C} \land (i \in N \land j \in N)) \to i {inv}_{g} (C) (x) j = {inv}_{g} (P) (i x j)$
33	29 32	syl	$⊢ (((((N \in Fin \land R \in Ring) \land x \in {Base}_{C}) \land (i \in N \land j \in N)) \land a \in {Base}_{R}) \land i x j = algSc (P) (a)) \to i {inv}_{g} (C) (x) j = {inv}_{g} (P) (i x j)$
34		fveq2	$⊢ i x j = algSc (P) (a) \to {inv}_{g} (P) (i x j) = {inv}_{g} (P) (algSc (P) (a))$
35		eqid	$⊢ Scalar (P) = Scalar (P)$
36	25	adantr	$⊢ ((((N \in Fin \land R \in Ring) \land x \in {Base}_{C}) \land (i \in N \land j \in N)) \land a \in {Base}_{R}) \to P \in Ring$
37	2	ply1lmod	$⊢ R \in Ring \to P \in LMod$
38	37	ad3antlr	$⊢ (((N \in Fin \land R \in Ring) \land x \in {Base}_{C}) \land (i \in N \land j \in N)) \to P \in LMod$
39	38	adantr	$⊢ ((((N \in Fin \land R \in Ring) \land x \in {Base}_{C}) \land (i \in N \land j \in N)) \land a \in {Base}_{R}) \to P \in LMod$
40	6 35 36 39	asclghm	$⊢ ((((N \in Fin \land R \in Ring) \land x \in {Base}_{C}) \land (i \in N \land j \in N)) \land a \in {Base}_{R}) \to algSc (P) \in (Scalar (P) GrpHom P)$
41	9	fveq2d	$⊢ (N \in Fin \land R \in Ring) \to {Base}_{R} = {Base}_{Scalar (P)}$
42	41	eleq2d	$⊢ (N \in Fin \land R \in Ring) \to (a \in {Base}_{R} \leftrightarrow a \in {Base}_{Scalar (P)})$
43	42	biimpd	$⊢ (N \in Fin \land R \in Ring) \to (a \in {Base}_{R} \to a \in {Base}_{Scalar (P)})$
44	43	ad2antrr	$⊢ (((N \in Fin \land R \in Ring) \land x \in {Base}_{C}) \land (i \in N \land j \in N)) \to (a \in {Base}_{R} \to a \in {Base}_{Scalar (P)})$
45	44	imp	$⊢ ((((N \in Fin \land R \in Ring) \land x \in {Base}_{C}) \land (i \in N \land j \in N)) \land a \in {Base}_{R}) \to a \in {Base}_{Scalar (P)}$
46		eqid	$⊢ {Base}_{Scalar (P)} = {Base}_{Scalar (P)}$
47		eqid	$⊢ {inv}_{g} (Scalar (P)) = {inv}_{g} (Scalar (P))$
48	46 47 30	ghminv	$⊢ (algSc (P) \in (Scalar (P) GrpHom P) \land a \in {Base}_{Scalar (P)}) \to algSc (P) ({inv}_{g} (Scalar (P)) (a)) = {inv}_{g} (P) (algSc (P) (a))$
49	40 45 48	syl2anc	$⊢ ((((N \in Fin \land R \in Ring) \land x \in {Base}_{C}) \land (i \in N \land j \in N)) \land a \in {Base}_{R}) \to algSc (P) ({inv}_{g} (Scalar (P)) (a)) = {inv}_{g} (P) (algSc (P) (a))$
50	49	eqcomd	$⊢ ((((N \in Fin \land R \in Ring) \land x \in {Base}_{C}) \land (i \in N \land j \in N)) \land a \in {Base}_{R}) \to {inv}_{g} (P) (algSc (P) (a)) = algSc (P) ({inv}_{g} (Scalar (P)) (a))$
51	34 50	sylan9eqr	$⊢ (((((N \in Fin \land R \in Ring) \land x \in {Base}_{C}) \land (i \in N \land j \in N)) \land a \in {Base}_{R}) \land i x j = algSc (P) (a)) \to {inv}_{g} (P) (i x j) = algSc (P) ({inv}_{g} (Scalar (P)) (a))$
52	33 51	eqtrd	$⊢ (((((N \in Fin \land R \in Ring) \land x \in {Base}_{C}) \land (i \in N \land j \in N)) \land a \in {Base}_{R}) \land i x j = algSc (P) (a)) \to i {inv}_{g} (C) (x) j = algSc (P) ({inv}_{g} (Scalar (P)) (a))$
53	20 23 52	rspcedvd	$⊢ (((((N \in Fin \land R \in Ring) \land x \in {Base}_{C}) \land (i \in N \land j \in N)) \land a \in {Base}_{R}) \land i x j = algSc (P) (a)) \to \exists c \in {Base}_{R} i {inv}_{g} (C) (x) j = algSc (P) (c)$
54	53	rexlimdva2	$⊢ (((N \in Fin \land R \in Ring) \land x \in {Base}_{C}) \land (i \in N \land j \in N)) \to (\exists a \in {Base}_{R} i x j = algSc (P) (a) \to \exists c \in {Base}_{R} i {inv}_{g} (C) (x) j = algSc (P) (c))$
55	54	ralimdvva	$⊢ ((N \in Fin \land R \in Ring) \land x \in {Base}_{C}) \to (\forall i \in N \forall j \in N \exists a \in {Base}_{R} i x j = algSc (P) (a) \to \forall i \in N \forall j \in N \exists c \in {Base}_{R} i {inv}_{g} (C) (x) j = algSc (P) (c))$
56	55	expimpd	$⊢ (N \in Fin \land R \in Ring) \to ((x \in {Base}_{C} \land \forall i \in N \forall j \in N \exists a \in {Base}_{R} i x j = algSc (P) (a)) \to \forall i \in N \forall j \in N \exists c \in {Base}_{R} i {inv}_{g} (C) (x) j = algSc (P) (c))$
57	7 56	syld	$⊢ (N \in Fin \land R \in Ring) \to (x \in S \to \forall i \in N \forall j \in N \exists c \in {Base}_{R} i {inv}_{g} (C) (x) j = algSc (P) (c))$
58	57	imp	$⊢ ((N \in Fin \land R \in Ring) \land x \in S) \to \forall i \in N \forall j \in N \exists c \in {Base}_{R} i {inv}_{g} (C) (x) j = algSc (P) (c)$
59		simpll	$⊢ ((N \in Fin \land R \in Ring) \land x \in S) \to N \in Fin$
60		simplr	$⊢ ((N \in Fin \land R \in Ring) \land x \in S) \to R \in Ring$
61	2 3	pmatring	$⊢ (N \in Fin \land R \in Ring) \to C \in Ring$
62		ringgrp	$⊢ C \in Ring \to C \in Grp$
63	61 62	syl	$⊢ (N \in Fin \land R \in Ring) \to C \in Grp$
64	63	adantr	$⊢ ((N \in Fin \land R \in Ring) \land x \in S) \to C \in Grp$
65	1 2 3 4	cpmatpmat	$⊢ (N \in Fin \land R \in Ring \land x \in S) \to x \in {Base}_{C}$
66	65	3expa	$⊢ ((N \in Fin \land R \in Ring) \land x \in S) \to x \in {Base}_{C}$
67	4 31	grpinvcl	$⊢ (C \in Grp \land x \in {Base}_{C}) \to {inv}_{g} (C) (x) \in {Base}_{C}$
68	64 66 67	syl2anc	$⊢ ((N \in Fin \land R \in Ring) \land x \in S) \to {inv}_{g} (C) (x) \in {Base}_{C}$
69	1 2 3 4 5 6	cpmatel2	$⊢ (N \in Fin \land R \in Ring \land {inv}_{g} (C) (x) \in {Base}_{C}) \to ({inv}_{g} (C) (x) \in S \leftrightarrow \forall i \in N \forall j \in N \exists c \in {Base}_{R} i {inv}_{g} (C) (x) j = algSc (P) (c))$
70	59 60 68 69	syl3anc	$⊢ ((N \in Fin \land R \in Ring) \land x \in S) \to ({inv}_{g} (C) (x) \in S \leftrightarrow \forall i \in N \forall j \in N \exists c \in {Base}_{R} i {inv}_{g} (C) (x) j = algSc (P) (c))$
71	58 70	mpbird	$⊢ ((N \in Fin \land R \in Ring) \land x \in S) \to {inv}_{g} (C) (x) \in S$
72	71	ralrimiva	$⊢ (N \in Fin \land R \in Ring) \to \forall x \in S {inv}_{g} (C) (x) \in S$

Metamath Proof Explorer

Theorem cpmatinvcl

Proof