Theorem mdetuni0 19657

Description: Lemma for mdetuni 19658. (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 17796	. . . . . . . . 9 |- ( R e. Ring -> R e. Grp )
11	9, 10	syl 17	. . . . . . . 8 |- ( ph -> R e. Grp )
12	11	adantr 471	. . . . . . 7 |- ( ( ph /\ a e. B ) -> R e. Grp )
13		mdetuni.ff	. . . . . . . 8 |- ( ph -> D : B --> K )
14	13	ffvelrnda 6006	. . . . . . 7 |- ( ( ph /\ a e. B ) -> ( D ` a ) e. K )
15	9	adantr 471	. . . . . . . 8 |- ( ( ph /\ a e. B ) -> R e. Ring )
16	8, 9	jca 539	. . . . . . . . . . 11 |- ( ph -> ( N e. Fin /\ R e. Ring ) )
17	1	matring 19479	. . . . . . . . . . 11 |- ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
18		eqid 2452	. . . . . . . . . . . 12 |- ( 1r ` A ) = ( 1r ` A )
19	2, 18	ringidcl 17812	. . . . . . . . . . 11 |- ( A e. Ring -> ( 1r ` A ) e. B )
20	16, 17, 19	3syl 18	. . . . . . . . . 10 |- ( ph -> ( 1r ` A ) e. B )
21	13, 20	ffvelrnd 6007	. . . . . . . . 9 |- ( ph -> ( D ` ( 1r ` A ) ) e. K )
22	21	adantr 471	. . . . . . . 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 19631	. . . . . . . . . 10 |- ( R e. CRing -> E : B --> K )
26	23, 25	syl 17	. . . . . . . . 9 |- ( ph -> E : B --> K )
27	26	ffvelrnda 6006	. . . . . . . 8 |- ( ( ph /\ a e. B ) -> ( E ` a ) e. K )
28	3, 7	ringcl 17805	. . . . . . . 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 1271	. . . . . . 7 |- ( ( ph /\ a e. B ) -> ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) e. K )
30		eqid 2452	. . . . . . . 8 |- ( -g ` R ) = ( -g ` R )
31	3, 30	grpsubcl 16745	. . . . . . 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 1271	. . . . . 6 |- ( ( ph /\ a e. B ) -> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) e. K )
33		eqid 2452	. . . . . 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 6030	. . . . 5 |- ( ph -> ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) : B --> K )
35		simpr1 1015	. . . . . . . . . 10 |- ( ( ph /\ ( b e. B /\ c e. N /\ d e. N ) ) -> b e. B )
36		fveq2 5848	. . . . . . . . . . . 12 |- ( a = b -> ( D ` a ) = ( D ` b ) )
37		fveq2 5848	. . . . . . . . . . . . 13 |- ( a = b -> ( E ` a ) = ( E ` b ) )
38	37	oveq2d 6292	. . . . . . . . . . . 12 |- ( a = b -> ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) = ( ( D ` ( 1r ` A ) ) .x. ( E ` b ) ) )
39	36, 38	oveq12d 6294	. . . . . . . . . . 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 6304	. . . . . . . . . . 11 |- ( ( D ` b ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` b ) ) ) e. _V
41	39, 33, 40	fvmpt 5932	. . . . . . . . . 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 1029	. . . . . . . 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 1009	. . . . . . . . . 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 1042	. . . . . . . . . 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 1038	. . . . . . . . . . 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 6284	. . . . . . . . . . . . 13 |- ( e = w -> ( c b e ) = ( c b w ) )
48		oveq2 6284	. . . . . . . . . . . . 13 |- ( e = w -> ( d b e ) = ( d b w ) )
49	47, 48	eqeq12d 2467	. . . . . . . . . . . 12 |- ( e = w -> ( ( c b e ) = ( d b e ) <-> ( c b w ) = ( d b w ) ) )
50	49	cbvralv 2987	. . . . . . . . . . 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 201	. . . . . . . . . 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 1043	. . . . . . . . . 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 1044	. . . . . . . . . 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 1037	. . . . . . . . . 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 19648	. . . . . . . . . 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 1286	. . . . . . . . 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 1030	. . . . . . . . . . 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 19644	. . . . . . . . . 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 6292	. . . . . . . . 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 6294	. . . . . . . 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 17829	. . . . . . . . . . . 12 |- ( ( R e. Ring /\ ( D ` ( 1r ` A ) ) e. K ) -> ( ( D ` ( 1r ` A ) ) .x. .0. ) = .0. )
65	9, 21, 64	syl2anc 671	. . . . . . . . . . 11 |- ( ph -> ( ( D ` ( 1r ` A ) ) .x. .0. ) = .0. )
66	65	oveq2d 6292	. . . . . . . . . 10 |- ( ph -> ( .0. ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. .0. ) ) = ( .0. ( -g ` R ) .0. ) )
67	3, 4	grpidcl 16705	. . . . . . . . . . . 12 |- ( R e. Grp -> .0. e. K )
68	11, 67	syl 17	. . . . . . . . . . 11 |- ( ph -> .0. e. K )
69	3, 4, 30	grpsubid 16749	. . . . . . . . . . 11 |- ( ( R e. Grp /\ .0. e. K ) -> ( .0. ( -g ` R ) .0. ) = .0. )
70	11, 68, 69	syl2anc 671	. . . . . . . . . 10 |- ( ph -> ( .0. ( -g ` R ) .0. ) = .0. )
71	66, 70	eqtrd 2486	. . . . . . . . 9 |- ( ph -> ( .0. ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. .0. ) ) = .0. )
72	71	3ad2ant1 1030	. . . . . . . 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 2490	. . . . . . 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 1212	. . . . . 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 2796	. . . . 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 1009	. . . . . . . . . . . 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 1076	. . . . . . . . . . . 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 1077	. . . . . . . . . . . 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 1078	. . . . . . . . . . . 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 1079	. . . . . . . . . . . 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 1045	. . . . . . . . . . . 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 1046	. . . . . . . . . . . 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 1047	. . . . . . . . . . . 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 19650	. . . . . . . . . . . 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 1302	. . . . . . . . . . 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 1030	. . . . . . . . . . . . 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 19638	. . . . . . . . . . . 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 6292	. . . . . . . . . . 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 6294	. . . . . . . . . 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 777	. . . . . . . . . . . 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 1029	. . . . . . . . . 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 778	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> c e. B )
94		fveq2 5848	. . . . . . . . . . . . . . . 16 |- ( a = c -> ( D ` a ) = ( D ` c ) )
95		fveq2 5848	. . . . . . . . . . . . . . . . 17 |- ( a = c -> ( E ` a ) = ( E ` c ) )
96	95	oveq2d 6292	. . . . . . . . . . . . . . . 16 |- ( a = c -> ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) = ( ( D ` ( 1r ` A ) ) .x. ( E ` c ) ) )
97	94, 96	oveq12d 6294	. . . . . . . . . . . . . . 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 6304	. . . . . . . . . . . . . . 15 |- ( ( D ` c ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` c ) ) ) e. _V
99	97, 33, 98	fvmpt 5932	. . . . . . . . . . . . . 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 779	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> d e. B )
102		fveq2 5848	. . . . . . . . . . . . . . . 16 |- ( a = d -> ( D ` a ) = ( D ` d ) )
103		fveq2 5848	. . . . . . . . . . . . . . . . 17 |- ( a = d -> ( E ` a ) = ( E ` d ) )
104	103	oveq2d 6292	. . . . . . . . . . . . . . . 16 |- ( a = d -> ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) = ( ( D ` ( 1r ` A ) ) .x. ( E ` d ) ) )
105	102, 104	oveq12d 6294	. . . . . . . . . . . . . . 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 6304	. . . . . . . . . . . . . . 15 |- ( ( D ` d ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` d ) ) ) e. _V
107	105, 33, 106	fvmpt 5932	. . . . . . . . . . . . . 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 6294	. . . . . . . . . . . 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 17821	. . . . . . . . . . . . . . 15 |- ( R e. Ring -> R e. Abel )
111	9, 110	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> R e. Abel )
112	111	adantr 471	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> R e. Abel )
113	13	adantr 471	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> D : B --> K )
114	113, 93	ffvelrnd 6007	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( D ` c ) e. K )
115	113, 101	ffvelrnd 6007	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( D ` d ) e. K )
116	9	adantr 471	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> R e. Ring )
117	21	adantr 471	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( D ` ( 1r ` A ) ) e. K )
118	26	adantr 471	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> E : B --> K )
119	118, 93	ffvelrnd 6007	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( E ` c ) e. K )
120	3, 7	ringcl 17805	. . . . . . . . . . . . . 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 1271	. . . . . . . . . . . . 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 6007	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( E ` d ) e. K )
123	3, 7	ringcl 17805	. . . . . . . . . . . . . 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 1271	. . . . . . . . . . . . 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 17466	. . . . . . . . . . . . 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 1280	. . . . . . . . . . . 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 17810	. . . . . . . . . . . . . . 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 1273	. . . . . . . . . . . . . 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 2458	. . . . . . . . . . . . 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 6292	. . . . . . . . . . . 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 2492	. . . . . . . . . . 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 1029	. . . . . . . . . 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 2496	. . . . . . . . 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 1212	. . . . . . . 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 658	. . . . . . 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 2795	. . . . . 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 2795	. . . . 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 1009	. . . . . . . . . . . 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 1076	. . . . . . . . . . . 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 1077	. . . . . . . . . . . 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 1078	. . . . . . . . . . . 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 1079	. . . . . . . . . . . 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 1037	. . . . . . . . . . . 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 1038	. . . . . . . . . . . 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 19651	. . . . . . . . . . . 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 1294	. . . . . . . . . . 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 1030	. . . . . . . . . . . . 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 19639	. . . . . . . . . . . 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 6292	. . . . . . . . . . 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 6294	. . . . . . . . . 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 777	. . . . . . . . . . . 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 1029	. . . . . . . . . 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 779	. . . . . . . . . . . . . 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 6292	. . . . . . . . . . . 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 471	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> R e. Ring )
158		simprlr 778	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> c e. K )
159	13	adantr 471	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> D : B --> K )
160	159, 154	ffvelrnd 6007	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> ( D ` d ) e. K )
161	21	adantr 471	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> ( D ` ( 1r ` A ) ) e. K )
162	26	adantr 471	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> E : B --> K )
163	162, 154	ffvelrnd 6007	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> ( E ` d ) e. K )
164	157, 161, 163, 123	syl3anc 1271	. . . . . . . . . . . . 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 17838	. . . . . . . . . . . 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 2452	. . . . . . . . . . . . . . . . 17 |- (mulGrp ` R ) = (mulGrp ` R )
167	166	crngmgp 17799	. . . . . . . . . . . . . . . 16 |- ( R e. CRing -> (mulGrp ` R ) e. CMnd )
168	23, 167	syl 17	. . . . . . . . . . . . . . 15 |- ( ph -> (mulGrp ` R ) e. CMnd )
169	168	adantr 471	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> (mulGrp ` R ) e. CMnd )
170	166, 3	mgpbas 17740	. . . . . . . . . . . . . . 15 |- K = ( Base ` (mulGrp ` R ) )
171	166, 7	mgpplusg 17738	. . . . . . . . . . . . . . 15 |- .x. = ( +g ` (mulGrp ` R ) )
172	170, 171	cmn12 17461	. . . . . . . . . . . . . 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 1273	. . . . . . . . . . . . 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 6292	. . . . . . . . . . . 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 2490	. . . . . . . . . . 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 1029	. . . . . . . . . 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 2496	. . . . . . . . 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 1212	. . . . . . . 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 658	. . . . . . 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 2795	. . . . . 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 2795	. . . . 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 2453	. . . . . 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 5848	. . . . . . . 8 |- ( a = ( 1r ` A ) -> ( D ` a ) = ( D ` ( 1r ` A ) ) )
184		fveq2 5848	. . . . . . . . 9 |- ( a = ( 1r ` A ) -> ( E ` a ) = ( E ` ( 1r ` A ) ) )
185	184	oveq2d 6292	. . . . . . . 8 |- ( a = ( 1r ` A ) -> ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) = ( ( D ` ( 1r ` A ) ) .x. ( E ` ( 1r ` A ) ) ) )
186	183, 185	oveq12d 6294	. . . . . . 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 19637	. . . . . . . . . . . 12 |- ( ( R e. CRing /\ N e. Fin ) -> ( E ` ( 1r ` A ) ) = .1. )
188	23, 8, 187	syl2anc 671	. . . . . . . . . . 11 |- ( ph -> ( E ` ( 1r ` A ) ) = .1. )
189	188	oveq2d 6292	. . . . . . . . . 10 |- ( ph -> ( ( D ` ( 1r ` A ) ) .x. ( E ` ( 1r ` A ) ) ) = ( ( D ` ( 1r ` A ) ) .x. .1. ) )
190	3, 7, 5	ringridm 17816	. . . . . . . . . . 11 |- ( ( R e. Ring /\ ( D ` ( 1r ` A ) ) e. K ) -> ( ( D ` ( 1r ` A ) ) .x. .1. ) = ( D ` ( 1r ` A ) ) )
191	9, 21, 190	syl2anc 671	. . . . . . . . . 10 |- ( ph -> ( ( D ` ( 1r ` A ) ) .x. .1. ) = ( D ` ( 1r ` A ) ) )
192	189, 191	eqtrd 2486	. . . . . . . . 9 |- ( ph -> ( ( D ` ( 1r ` A ) ) .x. ( E ` ( 1r ` A ) ) ) = ( D ` ( 1r ` A ) ) )
193	192	oveq2d 6292	. . . . . . . 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 16749	. . . . . . . . 9 |- ( ( R e. Grp /\ ( D ` ( 1r ` A ) ) e. K ) -> ( ( D ` ( 1r ` A ) ) ( -g ` R ) ( D ` ( 1r ` A ) ) ) = .0. )
195	11, 21, 194	syl2anc 671	. . . . . . . 8 |- ( ph -> ( ( D ` ( 1r ` A ) ) ( -g ` R ) ( D ` ( 1r ` A ) ) ) = .0. )
196	193, 195	eqtrd 2486	. . . . . . 7 |- ( ph -> ( ( D ` ( 1r ` A ) ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` ( 1r ` A ) ) ) ) = .0. )
197	186, 196	sylan9eqr 2508	. . . . . 6 |- ( ( ph /\ a = ( 1r ` A ) ) -> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) = .0. )
198		fvex 5858	. . . . . . . 8 |- ( 0g ` R ) e. _V
199	4, 198	eqeltri 2526	. . . . . . 7 |- .0. e. _V
200	199	a1i 11	. . . . . 6 |- ( ph -> .0. e. _V )
201	182, 197, 20, 200	fvmptd 5938	. . . . 5 |- ( ph -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` ( 1r ` A ) ) = .0. )
202		eqid 2452	. . . . 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 19656	. . . 4 |- ( ph -> ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) = ( B X. { .0. } ) )
204	203	fveq1d 5850	. . 3 |- ( ph -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` F ) = ( ( B X. { .0. } ) ` F ) )
205		fveq2 5848	. . . . . 6 |- ( a = F -> ( D ` a ) = ( D ` F ) )
206		fveq2 5848	. . . . . . 7 |- ( a = F -> ( E ` a ) = ( E ` F ) )
207	206	oveq2d 6292	. . . . . 6 |- ( a = F -> ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) = ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) )
208	205, 207	oveq12d 6294	. . . . 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 472	. . . 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		ovex 6304	. . . . 5 |- ( ( D ` F ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) ) e. _V
212	211	a1i 11	. . . 4 |- ( ph -> ( ( D ` F ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) ) e. _V )
213	182, 209, 210, 212	fvmptd 5938	. . 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 ) ) ) )
214	199	fvconst2 6105	. . . 4 |- ( F e. B -> ( ( B X. { .0. } ) ` F ) = .0. )
215	210, 214	syl 17	. . 3 |- ( ph -> ( ( B X. { .0. } ) ` F ) = .0. )
216	204, 213, 215	3eqtr3d 2494	. 2 |- ( ph -> ( ( D ` F ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) ) = .0. )
217	13, 210	ffvelrnd 6007	. . 3 |- ( ph -> ( D ` F ) e. K )
218	26, 210	ffvelrnd 6007	. . . 4 |- ( ph -> ( E ` F ) e. K )
219	3, 7	ringcl 17805	. . . 4 |- ( ( R e. Ring /\ ( D ` ( 1r ` A ) ) e. K /\ ( E ` F ) e. K ) -> ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) e. K )
220	9, 21, 218, 219	syl3anc 1271	. . 3 |- ( ph -> ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) e. K )
221	3, 4, 30	grpsubeq0 16751	. . 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 ) ) ) )
222	11, 217, 220, 221	syl3anc 1271	. 2 |- ( ph -> ( ( ( D ` F ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) ) = .0. <-> ( D ` F ) = ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) ) )
223	216, 222	mpbid 215	1 |- ( ph -> ( D ` F ) = ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   /\ w3a 986   = wceq 1448   e. wcel 1891   {cab 2438   =/= wne 2622   A.wral 2737   _Vcvv 3013   \ cdif 3369   ifcif 3849   {csn 3936   |-> cmpt 4433   X. cxp 4810   |` cres 4814   -->wf 5557   ` cfv 5561  (class class class)co 6276   oFcof 6517   ^m cmap 7459   Fincfn 7556   Basecbs 15132   +g cplusg 15201   .rcmulr 15202   0gc0g 15349   Grpcgrp 16680   -gcsg 16682  CMndccmn 17441   Abelcabl 17442  mulGrpcmgp 17734   1rcur 17746   Ringcrg 17791   CRingccrg 17792   Mat cmat 19443   maDet cmdat 19620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-8 1893  ax-9 1900  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432  ax-rep 4487  ax-sep 4497  ax-nul 4506  ax-pow 4554  ax-pr 4612  ax-un 6571  ax-inf2 8133  ax-cnex 9582  ax-resscn 9583  ax-1cn 9584  ax-icn 9585  ax-addcl 9586  ax-addrcl 9587  ax-mulcl 9588  ax-mulrcl 9589  ax-mulcom 9590  ax-addass 9591  ax-mulass 9592  ax-distr 9593  ax-i2m1 9594  ax-1ne0 9595  ax-1rid 9596  ax-rnegex 9597  ax-rrecex 9598  ax-cnre 9599  ax-pre-lttri 9600  ax-pre-lttrn 9601  ax-pre-ltadd 9602  ax-pre-mulgt0 9603  ax-addf 9605  ax-mulf 9606

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-xor 1409  df-tru 1451  df-fal 1454  df-ex 1668  df-nf 1672  df-sb 1802  df-eu 2304  df-mo 2305  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-reu 2744  df-rmo 2745  df-rab 2746  df-v 3015  df-sbc 3236  df-csb 3332  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-pss 3388  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-ot 3945  df-uni 4169  df-int 4205  df-iun 4250  df-iin 4251  df-br 4375  df-opab 4434  df-mpt 4435  df-tr 4470  df-eprel 4723  df-id 4727  df-po 4733  df-so 4734  df-fr 4771  df-se 4772  df-we 4773  df-xp 4818  df-rel 4819  df-cnv 4820  df-co 4821  df-dm 4822  df-rn 4823  df-res 4824  df-ima 4825  df-pred 5359  df-ord 5405  df-on 5406  df-lim 5407  df-suc 5408  df-iota 5525  df-fun 5563  df-fn 5564  df-f 5565  df-f1 5566  df-fo 5567  df-f1o 5568  df-fv 5569  df-isom 5570  df-riota 6238  df-ov 6279  df-oprab 6280  df-mpt2 6281  df-of 6519  df-om 6681  df-1st 6781  df-2nd 6782  df-supp 6903  df-tpos 6960  df-wrecs 7015  df-recs 7077  df-rdg 7115  df-1o 7169  df-2o 7170  df-oadd 7173  df-er 7350  df-map 7461  df-pm 7462  df-ixp 7510  df-en 7557  df-dom 7558  df-sdom 7559  df-fin 7560  df-fsupp 7871  df-sup 7943  df-oi 8012  df-card 8360  df-cda 8585  df-pnf 9664  df-mnf 9665  df-xr 9666  df-ltxr 9667  df-le 9668  df-sub 9849  df-neg 9850  df-div 10259  df-nn 10599  df-2 10657  df-3 10658  df-4 10659  df-5 10660  df-6 10661  df-7 10662  df-8 10663  df-9 10664  df-10 10665  df-n0 10860  df-z 10928  df-dec 11042  df-uz 11150  df-rp 11293  df-fz 11776  df-fzo 11909  df-seq 12208  df-exp 12267  df-hash 12510  df-word 12659  df-lsw 12660  df-concat 12661  df-s1 12662  df-substr 12663  df-splice 12664  df-reverse 12665  df-s2 12943  df-struct 15134  df-ndx 15135  df-slot 15136  df-base 15137  df-sets 15138  df-ress 15139  df-plusg 15214  df-mulr 15215  df-starv 15216  df-sca 15217  df-vsca 15218  df-ip 15219  df-tset 15220  df-ple 15221  df-ds 15223  df-unif 15224  df-hom 15225  df-cco 15226  df-0g 15351  df-gsum 15352  df-prds 15357  df-pws 15359  df-mre 15503  df-mrc 15504  df-acs 15506  df-mgm 16499  df-sgrp 16538  df-mnd 16548  df-mhm 16593  df-submnd 16594  df-grp 16684  df-minusg 16685  df-sbg 16686  df-mulg 16687  df-subg 16825  df-ghm 16892  df-gim 16934  df-cntz 16982  df-oppg 17008  df-symg 17030  df-pmtr 17094  df-psgn 17143  df-evpm 17144  df-cmn 17443  df-abl 17444  df-mgp 17735  df-ur 17747  df-srg 17751  df-ring 17793  df-cring 17794  df-oppr 17862  df-dvdsr 17880  df-unit 17881  df-invr 17911  df-dvr 17922  df-rnghom 17954  df-drng 17988  df-subrg 18017  df-lmod 18104  df-lss 18167  df-sra 18406  df-rgmod 18407  df-cnfld 18982  df-zring 19051  df-zrh 19086  df-dsmm 19306  df-frlm 19321  df-mamu 19420  df-mat 19444  df-mdet 19621

This theorem is referenced by:  mdetuni  19658  mdetmul  19659