pmatcollpwscmatlem2

Description: Lemma 2 for pmatcollpwscmat . (Contributed by AV, 2-Nov-2019) (Revised by AV, 4-Dec-2019)

	Ref	Expression
Hypotheses	pmatcollpwscmat.p	\|- P = ( Poly1 ` R )
	pmatcollpwscmat.c	\|- C = ( N Mat P )
	pmatcollpwscmat.b	\|- B = ( Base ` C )
	pmatcollpwscmat.m1	\|- .* = ( .s ` C )
	pmatcollpwscmat.e1	\|- .^ = ( .g ` ( mulGrp ` P ) )
	pmatcollpwscmat.x	\|- X = ( var1 ` R )
	pmatcollpwscmat.t	\|- T = ( N matToPolyMat R )
	pmatcollpwscmat.a	\|- A = ( N Mat R )
	pmatcollpwscmat.d	\|- D = ( Base ` A )
	pmatcollpwscmat.u	\|- U = ( algSc ` P )
	pmatcollpwscmat.k	\|- K = ( Base ` R )
	pmatcollpwscmat.e2	\|- E = ( Base ` P )
	pmatcollpwscmat.s	\|- S = ( algSc ` P )
	pmatcollpwscmat.1	\|- .1. = ( 1r ` C )
	pmatcollpwscmat.m2	\|- M = ( Q .* .1. )
Assertion	pmatcollpwscmatlem2	\|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( T ` ( M decompPMat L ) ) = ( ( U ` ( ( coe1 ` Q ) ` L ) ) .* .1. ) )

Proof

Step	Hyp	Ref	Expression
1		pmatcollpwscmat.p	\|- P = ( Poly1 ` R )
2		pmatcollpwscmat.c	\|- C = ( N Mat P )
3		pmatcollpwscmat.b	\|- B = ( Base ` C )
4		pmatcollpwscmat.m1	\|- .* = ( .s ` C )
5		pmatcollpwscmat.e1	\|- .^ = ( .g ` ( mulGrp ` P ) )
6		pmatcollpwscmat.x	\|- X = ( var1 ` R )
7		pmatcollpwscmat.t	\|- T = ( N matToPolyMat R )
8		pmatcollpwscmat.a	\|- A = ( N Mat R )
9		pmatcollpwscmat.d	\|- D = ( Base ` A )
10		pmatcollpwscmat.u	\|- U = ( algSc ` P )
11		pmatcollpwscmat.k	\|- K = ( Base ` R )
12		pmatcollpwscmat.e2	\|- E = ( Base ` P )
13		pmatcollpwscmat.s	\|- S = ( algSc ` P )
14		pmatcollpwscmat.1	\|- .1. = ( 1r ` C )
15		pmatcollpwscmat.m2	\|- M = ( Q .* .1. )
16		simpl	\|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( N e. Fin /\ R e. Ring ) )
17		simpr	\|- ( ( N e. Fin /\ R e. Ring ) -> R e. Ring )
18	17	adantr	\|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> R e. Ring )
19		simpr	\|- ( ( L e. NN0 /\ Q e. E ) -> Q e. E )
20	19	anim2i	\|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( ( N e. Fin /\ R e. Ring ) /\ Q e. E ) )
21		df-3an	\|- ( ( N e. Fin /\ R e. Ring /\ Q e. E ) <-> ( ( N e. Fin /\ R e. Ring ) /\ Q e. E ) )
22	20 21	sylibr	\|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( N e. Fin /\ R e. Ring /\ Q e. E ) )
23	1 2 3 12 4 14	1pmatscmul	\|- ( ( N e. Fin /\ R e. Ring /\ Q e. E ) -> ( Q .* .1. ) e. B )
24	15 23	eqeltrid	\|- ( ( N e. Fin /\ R e. Ring /\ Q e. E ) -> M e. B )
25	22 24	syl	\|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> M e. B )
26		simprl	\|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> L e. NN0 )
27	1 2 3 8 9	decpmatcl	\|- ( ( R e. Ring /\ M e. B /\ L e. NN0 ) -> ( M decompPMat L ) e. D )
28	18 25 26 27	syl3anc	\|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( M decompPMat L ) e. D )
29		df-3an	\|- ( ( N e. Fin /\ R e. Ring /\ ( M decompPMat L ) e. D ) <-> ( ( N e. Fin /\ R e. Ring ) /\ ( M decompPMat L ) e. D ) )
30	16 28 29	sylanbrc	\|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( N e. Fin /\ R e. Ring /\ ( M decompPMat L ) e. D ) )
31		eqid	\|- ( algSc ` P ) = ( algSc ` P )
32	7 8 9 1 31	mat2pmatval	\|- ( ( N e. Fin /\ R e. Ring /\ ( M decompPMat L ) e. D ) -> ( T ` ( M decompPMat L ) ) = ( i e. N , j e. N \|-> ( ( algSc ` P ) ` ( i ( M decompPMat L ) j ) ) ) )
33	30 32	syl	\|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( T ` ( M decompPMat L ) ) = ( i e. N , j e. N \|-> ( ( algSc ` P ) ` ( i ( M decompPMat L ) j ) ) ) )
34	18 25 26	3jca	\|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( R e. Ring /\ M e. B /\ L e. NN0 ) )
35	34	3ad2ant1	\|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ i e. N /\ j e. N ) -> ( R e. Ring /\ M e. B /\ L e. NN0 ) )
36		3simpc	\|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ i e. N /\ j e. N ) -> ( i e. N /\ j e. N ) )
37	1 2 3	decpmate	\|- ( ( ( R e. Ring /\ M e. B /\ L e. NN0 ) /\ ( i e. N /\ j e. N ) ) -> ( i ( M decompPMat L ) j ) = ( ( coe1 ` ( i M j ) ) ` L ) )
38	35 36 37	syl2anc	\|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ i e. N /\ j e. N ) -> ( i ( M decompPMat L ) j ) = ( ( coe1 ` ( i M j ) ) ` L ) )
39	38	fveq2d	\|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ i e. N /\ j e. N ) -> ( ( algSc ` P ) ` ( i ( M decompPMat L ) j ) ) = ( ( algSc ` P ) ` ( ( coe1 ` ( i M j ) ) ` L ) ) )
40	39	mpoeq3dva	\|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( i e. N , j e. N \|-> ( ( algSc ` P ) ` ( i ( M decompPMat L ) j ) ) ) = ( i e. N , j e. N \|-> ( ( algSc ` P ) ` ( ( coe1 ` ( i M j ) ) ` L ) ) ) )
41		simp1lr	\|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ i e. N /\ j e. N ) -> R e. Ring )
42		simp2	\|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ i e. N /\ j e. N ) -> i e. N )
43		simp3	\|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ i e. N /\ j e. N ) -> j e. N )
44	25	3ad2ant1	\|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ i e. N /\ j e. N ) -> M e. B )
45	2 12 3 42 43 44	matecld	\|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ i e. N /\ j e. N ) -> ( i M j ) e. E )
46	26	3ad2ant1	\|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ i e. N /\ j e. N ) -> L e. NN0 )
47		eqid	\|- ( coe1 ` ( i M j ) ) = ( coe1 ` ( i M j ) )
48	47 12 1 11	coe1fvalcl	\|- ( ( ( i M j ) e. E /\ L e. NN0 ) -> ( ( coe1 ` ( i M j ) ) ` L ) e. K )
49	45 46 48	syl2anc	\|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ i e. N /\ j e. N ) -> ( ( coe1 ` ( i M j ) ) ` L ) e. K )
50		eqid	\|- ( var1 ` R ) = ( var1 ` R )
51		eqid	\|- ( .s ` P ) = ( .s ` P )
52		eqid	\|- ( mulGrp ` P ) = ( mulGrp ` P )
53		eqid	\|- ( .g ` ( mulGrp ` P ) ) = ( .g ` ( mulGrp ` P ) )
54	11 1 50 51 52 53 31	ply1scltm	\|- ( ( R e. Ring /\ ( ( coe1 ` ( i M j ) ) ` L ) e. K ) -> ( ( algSc ` P ) ` ( ( coe1 ` ( i M j ) ) ` L ) ) = ( ( ( coe1 ` ( i M j ) ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) )
55	41 49 54	syl2anc	\|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ i e. N /\ j e. N ) -> ( ( algSc ` P ) ` ( ( coe1 ` ( i M j ) ) ` L ) ) = ( ( ( coe1 ` ( i M j ) ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) )
56	55	mpoeq3dva	\|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( i e. N , j e. N \|-> ( ( algSc ` P ) ` ( ( coe1 ` ( i M j ) ) ` L ) ) ) = ( i e. N , j e. N \|-> ( ( ( coe1 ` ( i M j ) ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) )
57	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	pmatcollpwscmatlem1	\|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ ( a e. N /\ b e. N ) ) -> ( ( ( coe1 ` ( a M b ) ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = if ( a = b , ( U ` ( ( coe1 ` Q ) ` L ) ) , ( 0g ` P ) ) )
58		eqidd	\|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ ( a e. N /\ b e. N ) ) -> ( i e. N , j e. N \|-> ( ( ( coe1 ` ( i M j ) ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) = ( i e. N , j e. N \|-> ( ( ( coe1 ` ( i M j ) ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) )
59		oveq12	\|- ( ( i = a /\ j = b ) -> ( i M j ) = ( a M b ) )
60	59	fveq2d	\|- ( ( i = a /\ j = b ) -> ( coe1 ` ( i M j ) ) = ( coe1 ` ( a M b ) ) )
61	60	fveq1d	\|- ( ( i = a /\ j = b ) -> ( ( coe1 ` ( i M j ) ) ` L ) = ( ( coe1 ` ( a M b ) ) ` L ) )
62	61	oveq1d	\|- ( ( i = a /\ j = b ) -> ( ( ( coe1 ` ( i M j ) ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = ( ( ( coe1 ` ( a M b ) ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) )
63	62	adantl	\|- ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ ( a e. N /\ b e. N ) ) /\ ( i = a /\ j = b ) ) -> ( ( ( coe1 ` ( i M j ) ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = ( ( ( coe1 ` ( a M b ) ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) )
64		simprl	\|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ ( a e. N /\ b e. N ) ) -> a e. N )
65		simprr	\|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ ( a e. N /\ b e. N ) ) -> b e. N )
66		ovexd	\|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ ( a e. N /\ b e. N ) ) -> ( ( ( coe1 ` ( a M b ) ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) e. _V )
67	58 63 64 65 66	ovmpod	\|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ ( a e. N /\ b e. N ) ) -> ( a ( i e. N , j e. N \|-> ( ( ( coe1 ` ( i M j ) ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) b ) = ( ( ( coe1 ` ( a M b ) ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) )
68		simpll	\|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> N e. Fin )
69	1	ply1ring	\|- ( R e. Ring -> P e. Ring )
70	69	adantl	\|- ( ( N e. Fin /\ R e. Ring ) -> P e. Ring )
71	70	adantr	\|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> P e. Ring )
72		pm3.22	\|- ( ( L e. NN0 /\ Q e. E ) -> ( Q e. E /\ L e. NN0 ) )
73	72	adantl	\|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( Q e. E /\ L e. NN0 ) )
74		eqid	\|- ( coe1 ` Q ) = ( coe1 ` Q )
75	74 12 1 11	coe1fvalcl	\|- ( ( Q e. E /\ L e. NN0 ) -> ( ( coe1 ` Q ) ` L ) e. K )
76	73 75	syl	\|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( ( coe1 ` Q ) ` L ) e. K )
77	1 10 11 12	ply1sclcl	\|- ( ( R e. Ring /\ ( ( coe1 ` Q ) ` L ) e. K ) -> ( U ` ( ( coe1 ` Q ) ` L ) ) e. E )
78	18 76 77	syl2anc	\|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( U ` ( ( coe1 ` Q ) ` L ) ) e. E )
79	68 71 78	3jca	\|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( N e. Fin /\ P e. Ring /\ ( U ` ( ( coe1 ` Q ) ` L ) ) e. E ) )
80		eqid	\|- ( 0g ` P ) = ( 0g ` P )
81	2 12 80 14 4	scmatscmide	\|- ( ( ( N e. Fin /\ P e. Ring /\ ( U ` ( ( coe1 ` Q ) ` L ) ) e. E ) /\ ( a e. N /\ b e. N ) ) -> ( a ( ( U ` ( ( coe1 ` Q ) ` L ) ) .* .1. ) b ) = if ( a = b , ( U ` ( ( coe1 ` Q ) ` L ) ) , ( 0g ` P ) ) )
82	79 81	sylan	\|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ ( a e. N /\ b e. N ) ) -> ( a ( ( U ` ( ( coe1 ` Q ) ` L ) ) .* .1. ) b ) = if ( a = b , ( U ` ( ( coe1 ` Q ) ` L ) ) , ( 0g ` P ) ) )
83	57 67 82	3eqtr4d	\|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ ( a e. N /\ b e. N ) ) -> ( a ( i e. N , j e. N \|-> ( ( ( coe1 ` ( i M j ) ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) b ) = ( a ( ( U ` ( ( coe1 ` Q ) ` L ) ) .* .1. ) b ) )
84	83	ralrimivva	\|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> A. a e. N A. b e. N ( a ( i e. N , j e. N \|-> ( ( ( coe1 ` ( i M j ) ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) b ) = ( a ( ( U ` ( ( coe1 ` Q ) ` L ) ) .* .1. ) b ) )
85		0nn0	\|- 0 e. NN0
86	85	a1i	\|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ i e. N /\ j e. N ) -> 0 e. NN0 )
87	11 1 50 51 52 53 12	ply1tmcl	\|- ( ( R e. Ring /\ ( ( coe1 ` ( i M j ) ) ` L ) e. K /\ 0 e. NN0 ) -> ( ( ( coe1 ` ( i M j ) ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) e. E )
88	41 49 86 87	syl3anc	\|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ i e. N /\ j e. N ) -> ( ( ( coe1 ` ( i M j ) ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) e. E )
89	2 12 3 68 71 88	matbas2d	\|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( i e. N , j e. N \|-> ( ( ( coe1 ` ( i M j ) ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) e. B )
90	1 2 3 12 4 14	1pmatscmul	\|- ( ( N e. Fin /\ R e. Ring /\ ( U ` ( ( coe1 ` Q ) ` L ) ) e. E ) -> ( ( U ` ( ( coe1 ` Q ) ` L ) ) .* .1. ) e. B )
91	68 18 78 90	syl3anc	\|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( ( U ` ( ( coe1 ` Q ) ` L ) ) .* .1. ) e. B )
92	2 3	eqmat	\|- ( ( ( i e. N , j e. N \|-> ( ( ( coe1 ` ( i M j ) ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) e. B /\ ( ( U ` ( ( coe1 ` Q ) ` L ) ) .* .1. ) e. B ) -> ( ( i e. N , j e. N \|-> ( ( ( coe1 ` ( i M j ) ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) = ( ( U ` ( ( coe1 ` Q ) ` L ) ) .* .1. ) <-> A. a e. N A. b e. N ( a ( i e. N , j e. N \|-> ( ( ( coe1 ` ( i M j ) ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) b ) = ( a ( ( U ` ( ( coe1 ` Q ) ` L ) ) .* .1. ) b ) ) )
93	89 91 92	syl2anc	\|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( ( i e. N , j e. N \|-> ( ( ( coe1 ` ( i M j ) ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) = ( ( U ` ( ( coe1 ` Q ) ` L ) ) .* .1. ) <-> A. a e. N A. b e. N ( a ( i e. N , j e. N \|-> ( ( ( coe1 ` ( i M j ) ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) b ) = ( a ( ( U ` ( ( coe1 ` Q ) ` L ) ) .* .1. ) b ) ) )
94	84 93	mpbird	\|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( i e. N , j e. N \|-> ( ( ( coe1 ` ( i M j ) ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) = ( ( U ` ( ( coe1 ` Q ) ` L ) ) .* .1. ) )
95	56 94	eqtrd	\|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( i e. N , j e. N \|-> ( ( algSc ` P ) ` ( ( coe1 ` ( i M j ) ) ` L ) ) ) = ( ( U ` ( ( coe1 ` Q ) ` L ) ) .* .1. ) )
96	33 40 95	3eqtrd	\|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( T ` ( M decompPMat L ) ) = ( ( U ` ( ( coe1 ` Q ) ` L ) ) .* .1. ) )

Metamath Proof Explorer

Theorem pmatcollpwscmatlem2

Proof