Theorem mdetuni0 20427

Description: Lemma for mdetuni 20428. (Contributed by SO, 15-Jul-2018.)

Hypotheses

Ref	Expression
mdetuni.a	|- A = ( N Mat R )
mdetuni.b	|- B = ( Base ` A )
mdetuni.k	|- K = ( Base ` R )
mdetuni.0g	|- .0. = ( 0g ` R )
mdetuni.1r	|- .1. = ( 1r ` R )
mdetuni.pg	|- .+ = ( +g ` R )
mdetuni.tg	|- .x. = ( .r ` R )
mdetuni.n	|- ( ph -> N e. Fin )
mdetuni.r	|- ( ph -> R e. Ring )
mdetuni.ff	|- ( ph -> D : B --> K )
mdetuni.al	|- ( ph -> A. x e. B A. y e. N A. z e. N ( ( y =/= z /\ A. w e. N ( y x w ) = ( z x w ) ) -> ( D ` x ) = .0. ) )
mdetuni.li	|- ( ph -> A. x e. B A. y e. B A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( ( D ` y ) .+ ( D ` z ) ) ) )
mdetuni.sc	|- ( ph -> A. x e. B A. y e. K A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( y .x. ( D ` z ) ) ) )
mdetuni.e	|- E = ( N maDet R )
mdetuni.cr	|- ( ph -> R e. CRing )
mdetuni.f	|- ( ph -> F e. B )

Assertion

Ref	Expression
mdetuni0	|- ( ph -> ( D ` F ) = ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) )

Distinct variable groups:   ph, x, y, z, w   x, B, y, z, w   x, K, y, z, w   x, N, y, z, w   x, D, y, z, w   x, .x. , y, z, w   x, .+ , y, z, w   x, .0. , y, z, w   x, .1. , y, z, w   x, R, y, z, w   x, A, y, z, w   x, E, y, z, w   x, F, y, z, w

Proof of Theorem mdetuni0

Dummy variables a b c d e are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mdetuni.a	. . . . 5 |- A = ( N Mat R )
2		mdetuni.b	. . . . 5 |- B = ( Base ` A )
3		mdetuni.k	. . . . 5 |- K = ( Base ` R )
4		mdetuni.0g	. . . . 5 |- .0. = ( 0g ` R )
5		mdetuni.1r	. . . . 5 |- .1. = ( 1r ` R )
6		mdetuni.pg	. . . . 5 |- .+ = ( +g ` R )
7		mdetuni.tg	. . . . 5 |- .x. = ( .r ` R )
8		mdetuni.n	. . . . 5 |- ( ph -> N e. Fin )
9		mdetuni.r	. . . . 5 |- ( ph -> R e. Ring )
10		ringgrp 18552	. . . . . . . . 9 |- ( R e. Ring -> R e. Grp )
11	9, 10	syl 17	. . . . . . . 8 |- ( ph -> R e. Grp )
12	11	adantr 481	. . . . . . 7 |- ( ( ph /\ a e. B ) -> R e. Grp )
13		mdetuni.ff	. . . . . . . 8 |- ( ph -> D : B --> K )
14	13	ffvelrnda 6359	. . . . . . 7 |- ( ( ph /\ a e. B ) -> ( D ` a ) e. K )
15	9	adantr 481	. . . . . . . 8 |- ( ( ph /\ a e. B ) -> R e. Ring )
16	8, 9	jca 554	. . . . . . . . . . 11 |- ( ph -> ( N e. Fin /\ R e. Ring ) )
17	1	matring 20249	. . . . . . . . . . 11 |- ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
18		eqid 2622	. . . . . . . . . . . 12 |- ( 1r ` A ) = ( 1r ` A )
19	2, 18	ringidcl 18568	. . . . . . . . . . 11 |- ( A e. Ring -> ( 1r ` A ) e. B )
20	16, 17, 19	3syl 18	. . . . . . . . . 10 |- ( ph -> ( 1r ` A ) e. B )
21	13, 20	ffvelrnd 6360	. . . . . . . . 9 |- ( ph -> ( D ` ( 1r ` A ) ) e. K )
22	21	adantr 481	. . . . . . . 8 |- ( ( ph /\ a e. B ) -> ( D ` ( 1r ` A ) ) e. K )
23		mdetuni.cr	. . . . . . . . . 10 |- ( ph -> R e. CRing )
24		mdetuni.e	. . . . . . . . . . 11 |- E = ( N maDet R )
25	24, 1, 2, 3	mdetf 20401	. . . . . . . . . 10 |- ( R e. CRing -> E : B --> K )
26	23, 25	syl 17	. . . . . . . . 9 |- ( ph -> E : B --> K )
27	26	ffvelrnda 6359	. . . . . . . 8 |- ( ( ph /\ a e. B ) -> ( E ` a ) e. K )
28	3, 7	ringcl 18561	. . . . . . . 8 |- ( ( R e. Ring /\ ( D ` ( 1r ` A ) ) e. K /\ ( E ` a ) e. K ) -> ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) e. K )
29	15, 22, 27, 28	syl3anc 1326	. . . . . . 7 |- ( ( ph /\ a e. B ) -> ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) e. K )
30		eqid 2622	. . . . . . . 8 |- ( -g ` R ) = ( -g ` R )
31	3, 30	grpsubcl 17495	. . . . . . 7 |- ( ( R e. Grp /\ ( D ` a ) e. K /\ ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) e. K ) -> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) e. K )
32	12, 14, 29, 31	syl3anc 1326	. . . . . 6 |- ( ( ph /\ a e. B ) -> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) e. K )
33		eqid 2622	. . . . . 6 |- ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) = ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) )
34	32, 33	fmptd 6385	. . . . 5 |- ( ph -> ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) : B --> K )
35		simpr1 1067	. . . . . . . . . 10 |- ( ( ph /\ ( b e. B /\ c e. N /\ d e. N ) ) -> b e. B )
36		fveq2 6191	. . . . . . . . . . . 12 |- ( a = b -> ( D ` a ) = ( D ` b ) )
37		fveq2 6191	. . . . . . . . . . . . 13 |- ( a = b -> ( E ` a ) = ( E ` b ) )
38	37	oveq2d 6666	. . . . . . . . . . . 12 |- ( a = b -> ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) = ( ( D ` ( 1r ` A ) ) .x. ( E ` b ) ) )
39	36, 38	oveq12d 6668	. . . . . . . . . . 11 |- ( a = b -> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) = ( ( D ` b ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` b ) ) ) )
40		ovex 6678	. . . . . . . . . . 11 |- ( ( D ` b ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` b ) ) ) e. _V
41	39, 33, 40	fvmpt 6282	. . . . . . . . . 10 |- ( b e. B -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` b ) = ( ( D ` b ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` b ) ) ) )
42	35, 41	syl 17	. . . . . . . . 9 |- ( ( ph /\ ( b e. B /\ c e. N /\ d e. N ) ) -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` b ) = ( ( D ` b ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` b ) ) ) )
43	42	3adant3 1081	. . . . . . . 8 |- ( ( ph /\ ( b e. B /\ c e. N /\ d e. N ) /\ ( c =/= d /\ A. e e. N ( c b e ) = ( d b e ) ) ) -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` b ) = ( ( D ` b ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` b ) ) ) )
44		simp1 1061	. . . . . . . . . 10 |- ( ( ph /\ ( b e. B /\ c e. N /\ d e. N ) /\ ( c =/= d /\ A. e e. N ( c b e ) = ( d b e ) ) ) -> ph )
45		simp21 1094	. . . . . . . . . 10 |- ( ( ph /\ ( b e. B /\ c e. N /\ d e. N ) /\ ( c =/= d /\ A. e e. N ( c b e ) = ( d b e ) ) ) -> b e. B )
46		simp3r 1090	. . . . . . . . . . 11 |- ( ( ph /\ ( b e. B /\ c e. N /\ d e. N ) /\ ( c =/= d /\ A. e e. N ( c b e ) = ( d b e ) ) ) -> A. e e. N ( c b e ) = ( d b e ) )
47		oveq2 6658	. . . . . . . . . . . . 13 |- ( e = w -> ( c b e ) = ( c b w ) )
48		oveq2 6658	. . . . . . . . . . . . 13 |- ( e = w -> ( d b e ) = ( d b w ) )
49	47, 48	eqeq12d 2637	. . . . . . . . . . . 12 |- ( e = w -> ( ( c b e ) = ( d b e ) <-> ( c b w ) = ( d b w ) ) )
50	49	cbvralv 3171	. . . . . . . . . . 11 |- ( A. e e. N ( c b e ) = ( d b e ) <-> A. w e. N ( c b w ) = ( d b w ) )
51	46, 50	sylib 208	. . . . . . . . . 10 |- ( ( ph /\ ( b e. B /\ c e. N /\ d e. N ) /\ ( c =/= d /\ A. e e. N ( c b e ) = ( d b e ) ) ) -> A. w e. N ( c b w ) = ( d b w ) )
52		simp22 1095	. . . . . . . . . 10 |- ( ( ph /\ ( b e. B /\ c e. N /\ d e. N ) /\ ( c =/= d /\ A. e e. N ( c b e ) = ( d b e ) ) ) -> c e. N )
53		simp23 1096	. . . . . . . . . 10 |- ( ( ph /\ ( b e. B /\ c e. N /\ d e. N ) /\ ( c =/= d /\ A. e e. N ( c b e ) = ( d b e ) ) ) -> d e. N )
54		simp3l 1089	. . . . . . . . . 10 |- ( ( ph /\ ( b e. B /\ c e. N /\ d e. N ) /\ ( c =/= d /\ A. e e. N ( c b e ) = ( d b e ) ) ) -> c =/= d )
55		mdetuni.al	. . . . . . . . . . 11 |- ( ph -> A. x e. B A. y e. N A. z e. N ( ( y =/= z /\ A. w e. N ( y x w ) = ( z x w ) ) -> ( D ` x ) = .0. ) )
56		mdetuni.li	. . . . . . . . . . 11 |- ( ph -> A. x e. B A. y e. B A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( ( D ` y ) .+ ( D ` z ) ) ) )
57		mdetuni.sc	. . . . . . . . . . 11 |- ( ph -> A. x e. B A. y e. K A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( y .x. ( D ` z ) ) ) )
58	1, 2, 3, 4, 5, 6, 7, 8, 9, 13, 55, 56, 57	mdetunilem1 20418	. . . . . . . . . 10 |- ( ( ( ph /\ b e. B /\ A. w e. N ( c b w ) = ( d b w ) ) /\ ( c e. N /\ d e. N /\ c =/= d ) ) -> ( D ` b ) = .0. )
59	44, 45, 51, 52, 53, 54, 58	syl33anc 1341	. . . . . . . . 9 |- ( ( ph /\ ( b e. B /\ c e. N /\ d e. N ) /\ ( c =/= d /\ A. e e. N ( c b e ) = ( d b e ) ) ) -> ( D ` b ) = .0. )
60	23	3ad2ant1 1082	. . . . . . . . . . 11 |- ( ( ph /\ ( b e. B /\ c e. N /\ d e. N ) /\ ( c =/= d /\ A. e e. N ( c b e ) = ( d b e ) ) ) -> R e. CRing )
61	24, 1, 2, 4, 60, 45, 52, 53, 54, 46	mdetralt 20414	. . . . . . . . . 10 |- ( ( ph /\ ( b e. B /\ c e. N /\ d e. N ) /\ ( c =/= d /\ A. e e. N ( c b e ) = ( d b e ) ) ) -> ( E ` b ) = .0. )
62	61	oveq2d 6666	. . . . . . . . 9 |- ( ( ph /\ ( b e. B /\ c e. N /\ d e. N ) /\ ( c =/= d /\ A. e e. N ( c b e ) = ( d b e ) ) ) -> ( ( D ` ( 1r ` A ) ) .x. ( E ` b ) ) = ( ( D ` ( 1r ` A ) ) .x. .0. ) )
63	59, 62	oveq12d 6668	. . . . . . . 8 |- ( ( ph /\ ( b e. B /\ c e. N /\ d e. N ) /\ ( c =/= d /\ A. e e. N ( c b e ) = ( d b e ) ) ) -> ( ( D ` b ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` b ) ) ) = ( .0. ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. .0. ) ) )
64	3, 7, 4	ringrz 18588	. . . . . . . . . . . 12 |- ( ( R e. Ring /\ ( D ` ( 1r ` A ) ) e. K ) -> ( ( D ` ( 1r ` A ) ) .x. .0. ) = .0. )
65	9, 21, 64	syl2anc 693	. . . . . . . . . . 11 |- ( ph -> ( ( D ` ( 1r ` A ) ) .x. .0. ) = .0. )
66	65	oveq2d 6666	. . . . . . . . . 10 |- ( ph -> ( .0. ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. .0. ) ) = ( .0. ( -g ` R ) .0. ) )
67	3, 4	grpidcl 17450	. . . . . . . . . . . 12 |- ( R e. Grp -> .0. e. K )
68	11, 67	syl 17	. . . . . . . . . . 11 |- ( ph -> .0. e. K )
69	3, 4, 30	grpsubid 17499	. . . . . . . . . . 11 |- ( ( R e. Grp /\ .0. e. K ) -> ( .0. ( -g ` R ) .0. ) = .0. )
70	11, 68, 69	syl2anc 693	. . . . . . . . . 10 |- ( ph -> ( .0. ( -g ` R ) .0. ) = .0. )
71	66, 70	eqtrd 2656	. . . . . . . . 9 |- ( ph -> ( .0. ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. .0. ) ) = .0. )
72	71	3ad2ant1 1082	. . . . . . . 8 |- ( ( ph /\ ( b e. B /\ c e. N /\ d e. N ) /\ ( c =/= d /\ A. e e. N ( c b e ) = ( d b e ) ) ) -> ( .0. ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. .0. ) ) = .0. )
73	43, 63, 72	3eqtrd 2660	. . . . . . 7 |- ( ( ph /\ ( b e. B /\ c e. N /\ d e. N ) /\ ( c =/= d /\ A. e e. N ( c b e ) = ( d b e ) ) ) -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` b ) = .0. )
74	73	3expia 1267	. . . . . 6 |- ( ( ph /\ ( b e. B /\ c e. N /\ d e. N ) ) -> ( ( c =/= d /\ A. e e. N ( c b e ) = ( d b e ) ) -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` b ) = .0. ) )
75	74	ralrimivvva 2972	. . . . 5 |- ( ph -> A. b e. B A. c e. N A. d e. N ( ( c =/= d /\ A. e e. N ( c b e ) = ( d b e ) ) -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` b ) = .0. ) )
76		simp1 1061	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF .+ ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ph )
77		simp2ll 1128	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF .+ ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> b e. B )
78		simp2lr 1129	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF .+ ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> c e. B )
79		simp2rl 1130	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF .+ ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> d e. B )
80		simp2rr 1131	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF .+ ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> e e. N )
81		simp31 1097	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF .+ ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF .+ ( d |` ( { e } X. N ) ) ) )
82		simp32 1098	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF .+ ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) )
83		simp33 1099	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF .+ ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) )
84	1, 2, 3, 4, 5, 6, 7, 8, 9, 13, 55, 56, 57	mdetunilem3 20420	. . . . . . . . . . . 12 |- ( ( ( ph /\ b e. B /\ c e. B ) /\ ( d e. B /\ e e. N /\ ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF .+ ( d |` ( { e } X. N ) ) ) ) /\ ( ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( D ` b ) = ( ( D ` c ) .+ ( D ` d ) ) )
85	76, 77, 78, 79, 80, 81, 82, 83, 84	syl332anc 1357	. . . . . . . . . . 11 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF .+ ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( D ` b ) = ( ( D ` c ) .+ ( D ` d ) ) )
86	23	3ad2ant1 1082	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF .+ ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> R e. CRing )
87	24, 1, 2, 6, 86, 77, 78, 79, 80, 81, 82, 83	mdetrlin 20408	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF .+ ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( E ` b ) = ( ( E ` c ) .+ ( E ` d ) ) )
88	87	oveq2d 6666	. . . . . . . . . . 11 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF .+ ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( D ` ( 1r ` A ) ) .x. ( E ` b ) ) = ( ( D ` ( 1r ` A ) ) .x. ( ( E ` c ) .+ ( E ` d ) ) ) )
89	85, 88	oveq12d 6668	. . . . . . . . . 10 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF .+ ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( D ` b ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` b ) ) ) = ( ( ( D ` c ) .+ ( D ` d ) ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( ( E ` c ) .+ ( E ` d ) ) ) ) )
90		simprll 802	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> b e. B )
91	90, 41	syl 17	. . . . . . . . . . 11 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` b ) = ( ( D ` b ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` b ) ) ) )
92	91	3adant3 1081	. . . . . . . . . 10 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF .+ ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` b ) = ( ( D ` b ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` b ) ) ) )
93		simprlr 803	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> c e. B )
94		fveq2 6191	. . . . . . . . . . . . . . . 16 |- ( a = c -> ( D ` a ) = ( D ` c ) )
95		fveq2 6191	. . . . . . . . . . . . . . . . 17 |- ( a = c -> ( E ` a ) = ( E ` c ) )
96	95	oveq2d 6666	. . . . . . . . . . . . . . . 16 |- ( a = c -> ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) = ( ( D ` ( 1r ` A ) ) .x. ( E ` c ) ) )
97	94, 96	oveq12d 6668	. . . . . . . . . . . . . . 15 |- ( a = c -> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) = ( ( D ` c ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` c ) ) ) )
98		ovex 6678	. . . . . . . . . . . . . . 15 |- ( ( D ` c ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` c ) ) ) e. _V
99	97, 33, 98	fvmpt 6282	. . . . . . . . . . . . . 14 |- ( c e. B -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` c ) = ( ( D ` c ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` c ) ) ) )
100	93, 99	syl 17	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` c ) = ( ( D ` c ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` c ) ) ) )
101		simprrl 804	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> d e. B )
102		fveq2 6191	. . . . . . . . . . . . . . . 16 |- ( a = d -> ( D ` a ) = ( D ` d ) )
103		fveq2 6191	. . . . . . . . . . . . . . . . 17 |- ( a = d -> ( E ` a ) = ( E ` d ) )
104	103	oveq2d 6666	. . . . . . . . . . . . . . . 16 |- ( a = d -> ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) = ( ( D ` ( 1r ` A ) ) .x. ( E ` d ) ) )
105	102, 104	oveq12d 6668	. . . . . . . . . . . . . . 15 |- ( a = d -> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) = ( ( D ` d ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` d ) ) ) )
106		ovex 6678	. . . . . . . . . . . . . . 15 |- ( ( D ` d ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` d ) ) ) e. _V
107	105, 33, 106	fvmpt 6282	. . . . . . . . . . . . . 14 |- ( d e. B -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` d ) = ( ( D ` d ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` d ) ) ) )
108	101, 107	syl 17	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` d ) = ( ( D ` d ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` d ) ) ) )
109	100, 108	oveq12d 6668	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` c ) .+ ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` d ) ) = ( ( ( D ` c ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` c ) ) ) .+ ( ( D ` d ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` d ) ) ) ) )
110		ringabl 18580	. . . . . . . . . . . . . . 15 |- ( R e. Ring -> R e. Abel )
111	9, 110	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> R e. Abel )
112	111	adantr 481	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> R e. Abel )
113	13	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> D : B --> K )
114	113, 93	ffvelrnd 6360	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( D ` c ) e. K )
115	113, 101	ffvelrnd 6360	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( D ` d ) e. K )
116	9	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> R e. Ring )
117	21	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( D ` ( 1r ` A ) ) e. K )
118	26	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> E : B --> K )
119	118, 93	ffvelrnd 6360	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( E ` c ) e. K )
120	3, 7	ringcl 18561	. . . . . . . . . . . . . 14 |- ( ( R e. Ring /\ ( D ` ( 1r ` A ) ) e. K /\ ( E ` c ) e. K ) -> ( ( D ` ( 1r ` A ) ) .x. ( E ` c ) ) e. K )
121	116, 117, 119, 120	syl3anc 1326	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( D ` ( 1r ` A ) ) .x. ( E ` c ) ) e. K )
122	118, 101	ffvelrnd 6360	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( E ` d ) e. K )
123	3, 7	ringcl 18561	. . . . . . . . . . . . . 14 |- ( ( R e. Ring /\ ( D ` ( 1r ` A ) ) e. K /\ ( E ` d ) e. K ) -> ( ( D ` ( 1r ` A ) ) .x. ( E ` d ) ) e. K )
124	116, 117, 122, 123	syl3anc 1326	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( D ` ( 1r ` A ) ) .x. ( E ` d ) ) e. K )
125	3, 6, 30	ablsub4 18218	. . . . . . . . . . . . 13 |- ( ( R e. Abel /\ ( ( D ` c ) e. K /\ ( D ` d ) e. K ) /\ ( ( ( D ` ( 1r ` A ) ) .x. ( E ` c ) ) e. K /\ ( ( D ` ( 1r ` A ) ) .x. ( E ` d ) ) e. K ) ) -> ( ( ( D ` c ) .+ ( D ` d ) ) ( -g ` R ) ( ( ( D ` ( 1r ` A ) ) .x. ( E ` c ) ) .+ ( ( D ` ( 1r ` A ) ) .x. ( E ` d ) ) ) ) = ( ( ( D ` c ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` c ) ) ) .+ ( ( D ` d ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` d ) ) ) ) )
126	112, 114, 115, 121, 124, 125	syl122anc 1335	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( ( D ` c ) .+ ( D ` d ) ) ( -g ` R ) ( ( ( D ` ( 1r ` A ) ) .x. ( E ` c ) ) .+ ( ( D ` ( 1r ` A ) ) .x. ( E ` d ) ) ) ) = ( ( ( D ` c ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` c ) ) ) .+ ( ( D ` d ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` d ) ) ) ) )
127	3, 6, 7	ringdi 18566	. . . . . . . . . . . . . . 15 |- ( ( R e. Ring /\ ( ( D ` ( 1r ` A ) ) e. K /\ ( E ` c ) e. K /\ ( E ` d ) e. K ) ) -> ( ( D ` ( 1r ` A ) ) .x. ( ( E ` c ) .+ ( E ` d ) ) ) = ( ( ( D ` ( 1r ` A ) ) .x. ( E ` c ) ) .+ ( ( D ` ( 1r ` A ) ) .x. ( E ` d ) ) ) )
128	116, 117, 119, 122, 127	syl13anc 1328	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( D ` ( 1r ` A ) ) .x. ( ( E ` c ) .+ ( E ` d ) ) ) = ( ( ( D ` ( 1r ` A ) ) .x. ( E ` c ) ) .+ ( ( D ` ( 1r ` A ) ) .x. ( E ` d ) ) ) )
129	128	eqcomd 2628	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( ( D ` ( 1r ` A ) ) .x. ( E ` c ) ) .+ ( ( D ` ( 1r ` A ) ) .x. ( E ` d ) ) ) = ( ( D ` ( 1r ` A ) ) .x. ( ( E ` c ) .+ ( E ` d ) ) ) )
130	129	oveq2d 6666	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( ( D ` c ) .+ ( D ` d ) ) ( -g ` R ) ( ( ( D ` ( 1r ` A ) ) .x. ( E ` c ) ) .+ ( ( D ` ( 1r ` A ) ) .x. ( E ` d ) ) ) ) = ( ( ( D ` c ) .+ ( D ` d ) ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( ( E ` c ) .+ ( E ` d ) ) ) ) )
131	109, 126, 130	3eqtr2d 2662	. . . . . . . . . . 11 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` c ) .+ ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` d ) ) = ( ( ( D ` c ) .+ ( D ` d ) ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( ( E ` c ) .+ ( E ` d ) ) ) ) )
132	131	3adant3 1081	. . . . . . . . . 10 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF .+ ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` c ) .+ ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` d ) ) = ( ( ( D ` c ) .+ ( D ` d ) ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( ( E ` c ) .+ ( E ` d ) ) ) ) )
133	89, 92, 132	3eqtr4d 2666	. . . . . . . . 9 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF .+ ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` b ) = ( ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` c ) .+ ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` d ) ) )
134	133	3expia 1267	. . . . . . . 8 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF .+ ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` b ) = ( ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` c ) .+ ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` d ) ) ) )
135	134	anassrs 680	. . . . . . 7 |- ( ( ( ph /\ ( b e. B /\ c e. B ) ) /\ ( d e. B /\ e e. N ) ) -> ( ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF .+ ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` b ) = ( ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` c ) .+ ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` d ) ) ) )
136	135	ralrimivva 2971	. . . . . 6 |- ( ( ph /\ ( b e. B /\ c e. B ) ) -> A. d e. B A. e e. N ( ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF .+ ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` b ) = ( ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` c ) .+ ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` d ) ) ) )
137	136	ralrimivva 2971	. . . . 5 |- ( ph -> A. b e. B A. c e. B A. d e. B A. e e. N ( ( ( b |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF .+ ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( c |` ( ( N \ { e } ) X. N ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` b ) = ( ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` c ) .+ ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` d ) ) ) )
138		simp1 1061	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ph )
139		simp2ll 1128	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> b e. B )
140		simp2lr 1129	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> c e. K )
141		simp2rl 1130	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> d e. B )
142		simp2rr 1131	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> e e. N )
143		simp3l 1089	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) )
144		simp3r 1090	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) )
145	1, 2, 3, 4, 5, 6, 7, 8, 9, 13, 55, 56, 57	mdetunilem4 20421	. . . . . . . . . . . 12 |- ( ( ph /\ ( b e. B /\ c e. K /\ d e. B ) /\ ( e e. N /\ ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( D ` b ) = ( c .x. ( D ` d ) ) )
146	138, 139, 140, 141, 142, 143, 144, 145	syl133anc 1349	. . . . . . . . . . 11 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( D ` b ) = ( c .x. ( D ` d ) ) )
147	23	3ad2ant1 1082	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> R e. CRing )
148	24, 1, 2, 3, 7, 147, 139, 140, 141, 142, 143, 144	mdetrsca 20409	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( E ` b ) = ( c .x. ( E ` d ) ) )
149	148	oveq2d 6666	. . . . . . . . . . 11 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( D ` ( 1r ` A ) ) .x. ( E ` b ) ) = ( ( D ` ( 1r ` A ) ) .x. ( c .x. ( E ` d ) ) ) )
150	146, 149	oveq12d 6668	. . . . . . . . . 10 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( D ` b ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` b ) ) ) = ( ( c .x. ( D ` d ) ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( c .x. ( E ` d ) ) ) ) )
151		simprll 802	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> b e. B )
152	151, 41	syl 17	. . . . . . . . . . 11 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` b ) = ( ( D ` b ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` b ) ) ) )
153	152	3adant3 1081	. . . . . . . . . 10 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` b ) = ( ( D ` b ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` b ) ) ) )
154		simprrl 804	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> d e. B )
155	154, 107	syl 17	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` d ) = ( ( D ` d ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` d ) ) ) )
156	155	oveq2d 6666	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> ( c .x. ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` d ) ) = ( c .x. ( ( D ` d ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` d ) ) ) ) )
157	9	adantr 481	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> R e. Ring )
158		simprlr 803	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> c e. K )
159	13	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> D : B --> K )
160	159, 154	ffvelrnd 6360	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> ( D ` d ) e. K )
161	21	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> ( D ` ( 1r ` A ) ) e. K )
162	26	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> E : B --> K )
163	162, 154	ffvelrnd 6360	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> ( E ` d ) e. K )
164	157, 161, 163, 123	syl3anc 1326	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( D ` ( 1r ` A ) ) .x. ( E ` d ) ) e. K )
165	3, 7, 30, 157, 158, 160, 164	ringsubdi 18599	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> ( c .x. ( ( D ` d ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` d ) ) ) ) = ( ( c .x. ( D ` d ) ) ( -g ` R ) ( c .x. ( ( D ` ( 1r ` A ) ) .x. ( E ` d ) ) ) ) )
166		eqid 2622	. . . . . . . . . . . . . . . . 17 |- (mulGrp ` R ) = (mulGrp ` R )
167	166	crngmgp 18555	. . . . . . . . . . . . . . . 16 |- ( R e. CRing -> (mulGrp ` R ) e. CMnd )
168	23, 167	syl 17	. . . . . . . . . . . . . . 15 |- ( ph -> (mulGrp ` R ) e. CMnd )
169	168	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> (mulGrp ` R ) e. CMnd )
170	166, 3	mgpbas 18495	. . . . . . . . . . . . . . 15 |- K = ( Base ` (mulGrp ` R ) )
171	166, 7	mgpplusg 18493	. . . . . . . . . . . . . . 15 |- .x. = ( +g ` (mulGrp ` R ) )
172	170, 171	cmn12 18213	. . . . . . . . . . . . . 14 |- ( ( (mulGrp ` R ) e. CMnd /\ ( c e. K /\ ( D ` ( 1r ` A ) ) e. K /\ ( E ` d ) e. K ) ) -> ( c .x. ( ( D ` ( 1r ` A ) ) .x. ( E ` d ) ) ) = ( ( D ` ( 1r ` A ) ) .x. ( c .x. ( E ` d ) ) ) )
173	169, 158, 161, 163, 172	syl13anc 1328	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> ( c .x. ( ( D ` ( 1r ` A ) ) .x. ( E ` d ) ) ) = ( ( D ` ( 1r ` A ) ) .x. ( c .x. ( E ` d ) ) ) )
174	173	oveq2d 6666	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( c .x. ( D ` d ) ) ( -g ` R ) ( c .x. ( ( D ` ( 1r ` A ) ) .x. ( E ` d ) ) ) ) = ( ( c .x. ( D ` d ) ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( c .x. ( E ` d ) ) ) ) )
175	156, 165, 174	3eqtrd 2660	. . . . . . . . . . 11 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> ( c .x. ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` d ) ) = ( ( c .x. ( D ` d ) ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( c .x. ( E ` d ) ) ) ) )
176	175	3adant3 1081	. . . . . . . . . 10 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( c .x. ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` d ) ) = ( ( c .x. ( D ` d ) ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( c .x. ( E ` d ) ) ) ) )
177	150, 153, 176	3eqtr4d 2666	. . . . . . . . 9 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) /\ ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) ) -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` b ) = ( c .x. ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` d ) ) )
178	177	3expia 1267	. . . . . . . 8 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> ( ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` b ) = ( c .x. ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` d ) ) ) )
179	178	anassrs 680	. . . . . . 7 |- ( ( ( ph /\ ( b e. B /\ c e. K ) ) /\ ( d e. B /\ e e. N ) ) -> ( ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` b ) = ( c .x. ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` d ) ) ) )
180	179	ralrimivva 2971	. . . . . 6 |- ( ( ph /\ ( b e. B /\ c e. K ) ) -> A. d e. B A. e e. N ( ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` b ) = ( c .x. ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` d ) ) ) )
181	180	ralrimivva 2971	. . . . 5 |- ( ph -> A. b e. B A. c e. K A. d e. B A. e e. N ( ( ( b |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) /\ ( b |` ( ( N \ { e } ) X. N ) ) = ( d |` ( ( N \ { e } ) X. N ) ) ) -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` b ) = ( c .x. ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` d ) ) ) )
182		eqidd 2623	. . . . . 6 |- ( ph -> ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) = ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) )
183		fveq2 6191	. . . . . . . 8 |- ( a = ( 1r ` A ) -> ( D ` a ) = ( D ` ( 1r ` A ) ) )
184		fveq2 6191	. . . . . . . . 9 |- ( a = ( 1r ` A ) -> ( E ` a ) = ( E ` ( 1r ` A ) ) )
185	184	oveq2d 6666	. . . . . . . 8 |- ( a = ( 1r ` A ) -> ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) = ( ( D ` ( 1r ` A ) ) .x. ( E ` ( 1r ` A ) ) ) )
186	183, 185	oveq12d 6668	. . . . . . 7 |- ( a = ( 1r ` A ) -> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) = ( ( D ` ( 1r ` A ) ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` ( 1r ` A ) ) ) ) )
187	24, 1, 18, 5	mdet1 20407	. . . . . . . . . . . 12 |- ( ( R e. CRing /\ N e. Fin ) -> ( E ` ( 1r ` A ) ) = .1. )
188	23, 8, 187	syl2anc 693	. . . . . . . . . . 11 |- ( ph -> ( E ` ( 1r ` A ) ) = .1. )
189	188	oveq2d 6666	. . . . . . . . . 10 |- ( ph -> ( ( D ` ( 1r ` A ) ) .x. ( E ` ( 1r ` A ) ) ) = ( ( D ` ( 1r ` A ) ) .x. .1. ) )
190	3, 7, 5	ringridm 18572	. . . . . . . . . . 11 |- ( ( R e. Ring /\ ( D ` ( 1r ` A ) ) e. K ) -> ( ( D ` ( 1r ` A ) ) .x. .1. ) = ( D ` ( 1r ` A ) ) )
191	9, 21, 190	syl2anc 693	. . . . . . . . . 10 |- ( ph -> ( ( D ` ( 1r ` A ) ) .x. .1. ) = ( D ` ( 1r ` A ) ) )
192	189, 191	eqtrd 2656	. . . . . . . . 9 |- ( ph -> ( ( D ` ( 1r ` A ) ) .x. ( E ` ( 1r ` A ) ) ) = ( D ` ( 1r ` A ) ) )
193	192	oveq2d 6666	. . . . . . . 8 |- ( ph -> ( ( D ` ( 1r ` A ) ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` ( 1r ` A ) ) ) ) = ( ( D ` ( 1r ` A ) ) ( -g ` R ) ( D ` ( 1r ` A ) ) ) )
194	3, 4, 30	grpsubid 17499	. . . . . . . . 9 |- ( ( R e. Grp /\ ( D ` ( 1r ` A ) ) e. K ) -> ( ( D ` ( 1r ` A ) ) ( -g ` R ) ( D ` ( 1r ` A ) ) ) = .0. )
195	11, 21, 194	syl2anc 693	. . . . . . . 8 |- ( ph -> ( ( D ` ( 1r ` A ) ) ( -g ` R ) ( D ` ( 1r ` A ) ) ) = .0. )
196	193, 195	eqtrd 2656	. . . . . . 7 |- ( ph -> ( ( D ` ( 1r ` A ) ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` ( 1r ` A ) ) ) ) = .0. )
197	186, 196	sylan9eqr 2678	. . . . . 6 |- ( ( ph /\ a = ( 1r ` A ) ) -> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) = .0. )
198		fvex 6201	. . . . . . . 8 |- ( 0g ` R ) e. _V
199	4, 198	eqeltri 2697	. . . . . . 7 |- .0. e. _V
200	199	a1i 11	. . . . . 6 |- ( ph -> .0. e. _V )
201	182, 197, 20, 200	fvmptd 6288	. . . . 5 |- ( ph -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` ( 1r ` A ) ) = .0. )
202		eqid 2622	. . . . 5 |- { b | A. c e. B A. d e. ( N ^m N ) ( A. e e. b ( c ` e ) = if ( e e. d , .1. , .0. ) -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` c ) = .0. ) } = { b | A. c e. B A. d e. ( N ^m N ) ( A. e e. b ( c ` e ) = if ( e e. d , .1. , .0. ) -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` c ) = .0. ) }
203	1, 2, 3, 4, 5, 6, 7, 8, 9, 34, 75, 137, 181, 201, 202	mdetunilem9 20426	. . . 4 |- ( ph -> ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) = ( B X. { .0. } ) )
204	203	fveq1d 6193	. . 3 |- ( ph -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` F ) = ( ( B X. { .0. } ) ` F ) )
205		fveq2 6191	. . . . . 6 |- ( a = F -> ( D ` a ) = ( D ` F ) )
206		fveq2 6191	. . . . . . 7 |- ( a = F -> ( E ` a ) = ( E ` F ) )
207	206	oveq2d 6666	. . . . . 6 |- ( a = F -> ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) = ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) )
208	205, 207	oveq12d 6668	. . . . 5 |- ( a = F -> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) = ( ( D ` F ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) ) )
209	208	adantl 482	. . . 4 |- ( ( ph /\ a = F ) -> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) = ( ( D ` F ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) ) )
210		mdetuni.f	. . . 4 |- ( ph -> F e. B )
211		ovexd 6680	. . . 4 |- ( ph -> ( ( D ` F ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) ) e. _V )
212	182, 209, 210, 211	fvmptd 6288	. . 3 |- ( ph -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` F ) = ( ( D ` F ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) ) )
213	199	fvconst2 6469	. . . 4 |- ( F e. B -> ( ( B X. { .0. } ) ` F ) = .0. )
214	210, 213	syl 17	. . 3 |- ( ph -> ( ( B X. { .0. } ) ` F ) = .0. )
215	204, 212, 214	3eqtr3d 2664	. 2 |- ( ph -> ( ( D ` F ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) ) = .0. )
216	13, 210	ffvelrnd 6360	. . 3 |- ( ph -> ( D ` F ) e. K )
217	26, 210	ffvelrnd 6360	. . . 4 |- ( ph -> ( E ` F ) e. K )
218	3, 7	ringcl 18561	. . . 4 |- ( ( R e. Ring /\ ( D ` ( 1r ` A ) ) e. K /\ ( E ` F ) e. K ) -> ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) e. K )
219	9, 21, 217, 218	syl3anc 1326	. . 3 |- ( ph -> ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) e. K )
220	3, 4, 30	grpsubeq0 17501	. . 3 |- ( ( R e. Grp /\ ( D ` F ) e. K /\ ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) e. K ) -> ( ( ( D ` F ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) ) = .0. <-> ( D ` F ) = ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) ) )
221	11, 216, 219, 220	syl3anc 1326	. 2 |- ( ph -> ( ( ( D ` F ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) ) = .0. <-> ( D ` F ) = ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) ) )
222	215, 221	mpbid 222	1 |- ( ph -> ( D ` F ) = ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   {cab 2608   =/= wne 2794   A.wral 2912   _Vcvv 3200   \ cdif 3571   ifcif 4086   {csn 4177   |-> cmpt 4729   X. cxp 5112   |` cres 5116   -->wf 5884   ` cfv 5888  (class class class)co 6650   oFcof 6895   ^m cmap 7857   Fincfn 7955   Basecbs 15857   +g cplusg 15941   .rcmulr 15942   0gc0g 16100   Grpcgrp 17422   -gcsg 17424  CMndccmn 18193   Abelcabl 18194  mulGrpcmgp 18489   1rcur 18501   Ringcrg 18547   CRingccrg 18548   Mat cmat 20213   maDet cmdat 20390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-addf 10015  ax-mulf 10016

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-xor 1465  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-ot 4186  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-om 7066  df-1st 7168  df-2nd 7169  df-supp 7296  df-tpos 7352  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-er 7742  df-map 7859  df-pm 7860  df-ixp 7909  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fsupp 8276  df-sup 8348  df-oi 8415  df-card 8765  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-xnn0 11364  df-z 11378  df-dec 11494  df-uz 11688  df-rp 11833  df-fz 12327  df-fzo 12466  df-seq 12802  df-exp 12861  df-hash 13118  df-word 13299  df-lsw 13300  df-concat 13301  df-s1 13302  df-substr 13303  df-splice 13304  df-reverse 13305  df-s2 13593  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-ress 15865  df-plusg 15954  df-mulr 15955  df-starv 15956  df-sca 15957  df-vsca 15958  df-ip 15959  df-tset 15960  df-ple 15961  df-ds 15964  df-unif 15965  df-hom 15966  df-cco 15967  df-0g 16102  df-gsum 16103  df-prds 16108  df-pws 16110  df-mre 16246  df-mrc 16247  df-acs 16249  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-mhm 17335  df-submnd 17336  df-grp 17425  df-minusg 17426  df-sbg 17427  df-mulg 17541  df-subg 17591  df-ghm 17658  df-gim 17701  df-cntz 17750  df-oppg 17776  df-symg 17798  df-pmtr 17862  df-psgn 17911  df-evpm 17912  df-cmn 18195  df-abl 18196  df-mgp 18490  df-ur 18502  df-srg 18506  df-ring 18549  df-cring 18550  df-oppr 18623  df-dvdsr 18641  df-unit 18642  df-invr 18672  df-dvr 18683  df-rnghom 18715  df-drng 18749  df-subrg 18778  df-lmod 18865  df-lss 18933  df-sra 19172  df-rgmod 19173  df-cnfld 19747  df-zring 19819  df-zrh 19852  df-dsmm 20076  df-frlm 20091  df-mamu 20190  df-mat 20214  df-mdet 20391

This theorem is referenced by:  mdetuni  20428  mdetmul  20429