Theorem mdetuni0 19208

Description: Lemma for mdetuni 19209. (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 17316	. . . . . . . . 9 |- ( R e. Ring -> R e. Grp )
11	9, 10	syl 16	. . . . . . . 8 |- ( ph -> R e. Grp )
12	11	adantr 463	. . . . . . 7 |- ( ( ph /\ a e. B ) -> R e. Grp )
13		mdetuni.ff	. . . . . . . 8 |- ( ph -> D : B --> K )
14	13	ffvelrnda 5933	. . . . . . 7 |- ( ( ph /\ a e. B ) -> ( D ` a ) e. K )
15	9	adantr 463	. . . . . . . 8 |- ( ( ph /\ a e. B ) -> R e. Ring )
16	8, 9	jca 530	. . . . . . . . . . 11 |- ( ph -> ( N e. Fin /\ R e. Ring ) )
17	1	matring 19030	. . . . . . . . . . 11 |- ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
18		eqid 2382	. . . . . . . . . . . 12 |- ( 1r ` A ) = ( 1r ` A )
19	2, 18	ringidcl 17332	. . . . . . . . . . 11 |- ( A e. Ring -> ( 1r ` A ) e. B )
20	16, 17, 19	3syl 20	. . . . . . . . . 10 |- ( ph -> ( 1r ` A ) e. B )
21	13, 20	ffvelrnd 5934	. . . . . . . . 9 |- ( ph -> ( D ` ( 1r ` A ) ) e. K )
22	21	adantr 463	. . . . . . . 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 19182	. . . . . . . . . 10 |- ( R e. CRing -> E : B --> K )
26	23, 25	syl 16	. . . . . . . . 9 |- ( ph -> E : B --> K )
27	26	ffvelrnda 5933	. . . . . . . 8 |- ( ( ph /\ a e. B ) -> ( E ` a ) e. K )
28	3, 7	ringcl 17325	. . . . . . . 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 1226	. . . . . . 7 |- ( ( ph /\ a e. B ) -> ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) e. K )
30		eqid 2382	. . . . . . . 8 |- ( -g ` R ) = ( -g ` R )
31	3, 30	grpsubcl 16235	. . . . . . 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 1226	. . . . . 6 |- ( ( ph /\ a e. B ) -> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) e. K )
33		eqid 2382	. . . . . 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 5957	. . . . 5 |- ( ph -> ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) : B --> K )
35		simpr1 1000	. . . . . . . . . 10 |- ( ( ph /\ ( b e. B /\ c e. N /\ d e. N ) ) -> b e. B )
36		fveq2 5774	. . . . . . . . . . . 12 |- ( a = b -> ( D ` a ) = ( D ` b ) )
37		fveq2 5774	. . . . . . . . . . . . 13 |- ( a = b -> ( E ` a ) = ( E ` b ) )
38	37	oveq2d 6212	. . . . . . . . . . . 12 |- ( a = b -> ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) = ( ( D ` ( 1r ` A ) ) .x. ( E ` b ) ) )
39	36, 38	oveq12d 6214	. . . . . . . . . . 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 6224	. . . . . . . . . . 11 |- ( ( D ` b ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` b ) ) ) e. _V
41	39, 33, 40	fvmpt 5857	. . . . . . . . . 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 16	. . . . . . . . 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 1014	. . . . . . . 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 994	. . . . . . . . . 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 1027	. . . . . . . . . 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 1023	. . . . . . . . . . 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 6204	. . . . . . . . . . . . 13 |- ( e = w -> ( c b e ) = ( c b w ) )
48		oveq2 6204	. . . . . . . . . . . . 13 |- ( e = w -> ( d b e ) = ( d b w ) )
49	47, 48	eqeq12d 2404	. . . . . . . . . . . 12 |- ( e = w -> ( ( c b e ) = ( d b e ) <-> ( c b w ) = ( d b w ) ) )
50	49	cbvralv 3009	. . . . . . . . . . 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 196	. . . . . . . . . 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 1028	. . . . . . . . . 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 1029	. . . . . . . . . 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 1022	. . . . . . . . . 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 19199	. . . . . . . . . 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 1241	. . . . . . . . 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 1015	. . . . . . . . . . 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 19195	. . . . . . . . . 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 6212	. . . . . . . . 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 6214	. . . . . . . 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 17349	. . . . . . . . . . . 12 |- ( ( R e. Ring /\ ( D ` ( 1r ` A ) ) e. K ) -> ( ( D ` ( 1r ` A ) ) .x. .0. ) = .0. )
65	9, 21, 64	syl2anc 659	. . . . . . . . . . 11 |- ( ph -> ( ( D ` ( 1r ` A ) ) .x. .0. ) = .0. )
66	65	oveq2d 6212	. . . . . . . . . 10 |- ( ph -> ( .0. ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. .0. ) ) = ( .0. ( -g ` R ) .0. ) )
67	3, 4	grpidcl 16195	. . . . . . . . . . . 12 |- ( R e. Grp -> .0. e. K )
68	11, 67	syl 16	. . . . . . . . . . 11 |- ( ph -> .0. e. K )
69	3, 4, 30	grpsubid 16239	. . . . . . . . . . 11 |- ( ( R e. Grp /\ .0. e. K ) -> ( .0. ( -g ` R ) .0. ) = .0. )
70	11, 68, 69	syl2anc 659	. . . . . . . . . 10 |- ( ph -> ( .0. ( -g ` R ) .0. ) = .0. )
71	66, 70	eqtrd 2423	. . . . . . . . 9 |- ( ph -> ( .0. ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. .0. ) ) = .0. )
72	71	3ad2ant1 1015	. . . . . . . 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 2427	. . . . . . 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 1196	. . . . . 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 2804	. . . . 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 994	. . . . . . . . . . . 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 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 ) ) ) ) -> b e. B )
78		simp2lr 1062	. . . . . . . . . . . 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 1063	. . . . . . . . . . . 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 1064	. . . . . . . . . . . 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 1030	. . . . . . . . . . . 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 1031	. . . . . . . . . . . 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 1032	. . . . . . . . . . . 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 19201	. . . . . . . . . . . 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 1257	. . . . . . . . . . 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 1015	. . . . . . . . . . . . 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 19189	. . . . . . . . . . . 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 6212	. . . . . . . . . . 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 6214	. . . . . . . . . 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 761	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> b e. B )
91	90, 41	syl 16	. . . . . . . . . . 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 1014	. . . . . . . . . 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 762	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> c e. B )
94		fveq2 5774	. . . . . . . . . . . . . . . 16 |- ( a = c -> ( D ` a ) = ( D ` c ) )
95		fveq2 5774	. . . . . . . . . . . . . . . . 17 |- ( a = c -> ( E ` a ) = ( E ` c ) )
96	95	oveq2d 6212	. . . . . . . . . . . . . . . 16 |- ( a = c -> ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) = ( ( D ` ( 1r ` A ) ) .x. ( E ` c ) ) )
97	94, 96	oveq12d 6214	. . . . . . . . . . . . . . 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 6224	. . . . . . . . . . . . . . 15 |- ( ( D ` c ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` c ) ) ) e. _V
99	97, 33, 98	fvmpt 5857	. . . . . . . . . . . . . 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 16	. . . . . . . . . . . . 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 763	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> d e. B )
102		fveq2 5774	. . . . . . . . . . . . . . . 16 |- ( a = d -> ( D ` a ) = ( D ` d ) )
103		fveq2 5774	. . . . . . . . . . . . . . . . 17 |- ( a = d -> ( E ` a ) = ( E ` d ) )
104	103	oveq2d 6212	. . . . . . . . . . . . . . . 16 |- ( a = d -> ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) = ( ( D ` ( 1r ` A ) ) .x. ( E ` d ) ) )
105	102, 104	oveq12d 6214	. . . . . . . . . . . . . . 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 6224	. . . . . . . . . . . . . . 15 |- ( ( D ` d ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` d ) ) ) e. _V
107	105, 33, 106	fvmpt 5857	. . . . . . . . . . . . . 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 16	. . . . . . . . . . . . 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 6214	. . . . . . . . . . . 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 17341	. . . . . . . . . . . . . . 15 |- ( R e. Ring -> R e. Abel )
111	9, 110	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> R e. Abel )
112	111	adantr 463	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> R e. Abel )
113	13	adantr 463	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> D : B --> K )
114	113, 93	ffvelrnd 5934	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( D ` c ) e. K )
115	113, 101	ffvelrnd 5934	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( D ` d ) e. K )
116	9	adantr 463	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> R e. Ring )
117	21	adantr 463	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( D ` ( 1r ` A ) ) e. K )
118	26	adantr 463	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> E : B --> K )
119	118, 93	ffvelrnd 5934	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( E ` c ) e. K )
120	3, 7	ringcl 17325	. . . . . . . . . . . . . 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 1226	. . . . . . . . . . . . 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 5934	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( E ` d ) e. K )
123	3, 7	ringcl 17325	. . . . . . . . . . . . . 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 1226	. . . . . . . . . . . . 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 16940	. . . . . . . . . . . . 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 1235	. . . . . . . . . . . 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 17330	. . . . . . . . . . . . . . 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 1228	. . . . . . . . . . . . . 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 2390	. . . . . . . . . . . . 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 6212	. . . . . . . . . . . 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 2429	. . . . . . . . . . 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 1014	. . . . . . . . . 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 2433	. . . . . . . . 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 1196	. . . . . . . 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 646	. . . . . . 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 2803	. . . . . 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 2803	. . . . 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 994	. . . . . . . . . . . 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 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 ) ) ) ) -> b e. B )
140		simp2lr 1062	. . . . . . . . . . . 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 1063	. . . . . . . . . . . 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 1064	. . . . . . . . . . . 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 1022	. . . . . . . . . . . 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 1023	. . . . . . . . . . . 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 19202	. . . . . . . . . . . 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 1249	. . . . . . . . . . 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 1015	. . . . . . . . . . . . 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 19190	. . . . . . . . . . . 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 6212	. . . . . . . . . . 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 6214	. . . . . . . . . 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 761	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> b e. B )
152	151, 41	syl 16	. . . . . . . . . . 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 1014	. . . . . . . . . 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 763	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> d e. B )
155	154, 107	syl 16	. . . . . . . . . . . . 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 6212	. . . . . . . . . . . 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 463	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> R e. Ring )
158		simprlr 762	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> c e. K )
159	13	adantr 463	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> D : B --> K )
160	159, 154	ffvelrnd 5934	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> ( D ` d ) e. K )
161	21	adantr 463	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> ( D ` ( 1r ` A ) ) e. K )
162	26	adantr 463	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> E : B --> K )
163	162, 154	ffvelrnd 5934	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> ( E ` d ) e. K )
164	157, 161, 163, 123	syl3anc 1226	. . . . . . . . . . . . 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 17358	. . . . . . . . . . . 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 2382	. . . . . . . . . . . . . . . . 17 |- (mulGrp ` R ) = (mulGrp ` R )
167	166	crngmgp 17319	. . . . . . . . . . . . . . . 16 |- ( R e. CRing -> (mulGrp ` R ) e. CMnd )
168	23, 167	syl 16	. . . . . . . . . . . . . . 15 |- ( ph -> (mulGrp ` R ) e. CMnd )
169	168	adantr 463	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> (mulGrp ` R ) e. CMnd )
170	166, 3	mgpbas 17260	. . . . . . . . . . . . . . 15 |- K = ( Base ` (mulGrp ` R ) )
171	166, 7	mgpplusg 17258	. . . . . . . . . . . . . . 15 |- .x. = ( +g ` (mulGrp ` R ) )
172	170, 171	cmn12 16935	. . . . . . . . . . . . . 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 1228	. . . . . . . . . . . . 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 6212	. . . . . . . . . . . 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 2427	. . . . . . . . . . 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 1014	. . . . . . . . . 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 2433	. . . . . . . . 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 1196	. . . . . . . 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 646	. . . . . . 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 2803	. . . . . 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 2803	. . . . 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 2383	. . . . . 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 5774	. . . . . . . 8 |- ( a = ( 1r ` A ) -> ( D ` a ) = ( D ` ( 1r ` A ) ) )
184		fveq2 5774	. . . . . . . . 9 |- ( a = ( 1r ` A ) -> ( E ` a ) = ( E ` ( 1r ` A ) ) )
185	184	oveq2d 6212	. . . . . . . 8 |- ( a = ( 1r ` A ) -> ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) = ( ( D ` ( 1r ` A ) ) .x. ( E ` ( 1r ` A ) ) ) )
186	183, 185	oveq12d 6214	. . . . . . 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 19188	. . . . . . . . . . . 12 |- ( ( R e. CRing /\ N e. Fin ) -> ( E ` ( 1r ` A ) ) = .1. )
188	23, 8, 187	syl2anc 659	. . . . . . . . . . 11 |- ( ph -> ( E ` ( 1r ` A ) ) = .1. )
189	188	oveq2d 6212	. . . . . . . . . 10 |- ( ph -> ( ( D ` ( 1r ` A ) ) .x. ( E ` ( 1r ` A ) ) ) = ( ( D ` ( 1r ` A ) ) .x. .1. ) )
190	3, 7, 5	ringridm 17336	. . . . . . . . . . 11 |- ( ( R e. Ring /\ ( D ` ( 1r ` A ) ) e. K ) -> ( ( D ` ( 1r ` A ) ) .x. .1. ) = ( D ` ( 1r ` A ) ) )
191	9, 21, 190	syl2anc 659	. . . . . . . . . 10 |- ( ph -> ( ( D ` ( 1r ` A ) ) .x. .1. ) = ( D ` ( 1r ` A ) ) )
192	189, 191	eqtrd 2423	. . . . . . . . 9 |- ( ph -> ( ( D ` ( 1r ` A ) ) .x. ( E ` ( 1r ` A ) ) ) = ( D ` ( 1r ` A ) ) )
193	192	oveq2d 6212	. . . . . . . 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 16239	. . . . . . . . 9 |- ( ( R e. Grp /\ ( D ` ( 1r ` A ) ) e. K ) -> ( ( D ` ( 1r ` A ) ) ( -g ` R ) ( D ` ( 1r ` A ) ) ) = .0. )
195	11, 21, 194	syl2anc 659	. . . . . . . 8 |- ( ph -> ( ( D ` ( 1r ` A ) ) ( -g ` R ) ( D ` ( 1r ` A ) ) ) = .0. )
196	193, 195	eqtrd 2423	. . . . . . 7 |- ( ph -> ( ( D ` ( 1r ` A ) ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` ( 1r ` A ) ) ) ) = .0. )
197	186, 196	sylan9eqr 2445	. . . . . 6 |- ( ( ph /\ a = ( 1r ` A ) ) -> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) = .0. )
198		fvex 5784	. . . . . . . 8 |- ( 0g ` R ) e. _V
199	4, 198	eqeltri 2466	. . . . . . 7 |- .0. e. _V
200	199	a1i 11	. . . . . 6 |- ( ph -> .0. e. _V )
201	182, 197, 20, 200	fvmptd 5862	. . . . 5 |- ( ph -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` ( 1r ` A ) ) = .0. )
202		eqid 2382	. . . . 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 19207	. . . 4 |- ( ph -> ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) = ( B X. { .0. } ) )
204	203	fveq1d 5776	. . 3 |- ( ph -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` F ) = ( ( B X. { .0. } ) ` F ) )
205		fveq2 5774	. . . . . 6 |- ( a = F -> ( D ` a ) = ( D ` F ) )
206		fveq2 5774	. . . . . . 7 |- ( a = F -> ( E ` a ) = ( E ` F ) )
207	206	oveq2d 6212	. . . . . 6 |- ( a = F -> ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) = ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) )
208	205, 207	oveq12d 6214	. . . . 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 464	. . . 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 6224	. . . . 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 5862	. . 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 6029	. . . 4 |- ( F e. B -> ( ( B X. { .0. } ) ` F ) = .0. )
215	210, 214	syl 16	. . 3 |- ( ph -> ( ( B X. { .0. } ) ` F ) = .0. )
216	204, 213, 215	3eqtr3d 2431	. 2 |- ( ph -> ( ( D ` F ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) ) = .0. )
217	13, 210	ffvelrnd 5934	. . 3 |- ( ph -> ( D ` F ) e. K )
218	26, 210	ffvelrnd 5934	. . . 4 |- ( ph -> ( E ` F ) e. K )
219	3, 7	ringcl 17325	. . . 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 1226	. . 3 |- ( ph -> ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) e. K )
221	3, 4, 30	grpsubeq0 16241	. . 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 1226	. 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 210	1 |- ( ph -> ( D ` F ) = ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 367   /\ w3a 971   = wceq 1399   e. wcel 1826   {cab 2367   =/= wne 2577   A.wral 2732   _Vcvv 3034   \ cdif 3386   ifcif 3857   {csn 3944   |-> cmpt 4425   X. cxp 4911   |` cres 4915   -->wf 5492   ` cfv 5496  (class class class)co 6196   oFcof 6437   ^m cmap 7338   Fincfn 7435   Basecbs 14634   +g cplusg 14702   .rcmulr 14703   0gc0g 14847   Grpcgrp 16170   -gcsg 16172  CMndccmn 16915   Abelcabl 16916  mulGrpcmgp 17254   1rcur 17266   Ringcrg 17311   CRingccrg 17312   Mat cmat 18994   maDet cmdat 19171

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-rep 4478  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491  ax-inf2 7972  ax-cnex 9459  ax-resscn 9460  ax-1cn 9461  ax-icn 9462  ax-addcl 9463  ax-addrcl 9464  ax-mulcl 9465  ax-mulrcl 9466  ax-mulcom 9467  ax-addass 9468  ax-mulass 9469  ax-distr 9470  ax-i2m1 9471  ax-1ne0 9472  ax-1rid 9473  ax-rnegex 9474  ax-rrecex 9475  ax-cnre 9476  ax-pre-lttri 9477  ax-pre-lttrn 9478  ax-pre-ltadd 9479  ax-pre-mulgt0 9480  ax-addf 9482  ax-mulf 9483

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-xor 1363  df-tru 1402  df-fal 1405  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-nel 2580  df-ral 2737  df-rex 2738  df-reu 2739  df-rmo 2740  df-rab 2741  df-v 3036  df-sbc 3253  df-csb 3349  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-pss 3405  df-nul 3712  df-if 3858  df-pw 3929  df-sn 3945  df-pr 3947  df-tp 3949  df-op 3951  df-ot 3953  df-uni 4164  df-int 4200  df-iun 4245  df-iin 4246  df-br 4368  df-opab 4426  df-mpt 4427  df-tr 4461  df-eprel 4705  df-id 4709  df-po 4714  df-so 4715  df-fr 4752  df-se 4753  df-we 4754  df-ord 4795  df-on 4796  df-lim 4797  df-suc 4798  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fn 5499  df-f 5500  df-f1 5501  df-fo 5502  df-f1o 5503  df-fv 5504  df-isom 5505  df-riota 6158  df-ov 6199  df-oprab 6200  df-mpt2 6201  df-of 6439  df-om 6600  df-1st 6699  df-2nd 6700  df-supp 6818  df-tpos 6873  df-recs 6960  df-rdg 6994  df-1o 7048  df-2o 7049  df-oadd 7052  df-er 7229  df-map 7340  df-pm 7341  df-ixp 7389  df-en 7436  df-dom 7437  df-sdom 7438  df-fin 7439  df-fsupp 7745  df-sup 7816  df-oi 7850  df-card 8233  df-cda 8461  df-pnf 9541  df-mnf 9542  df-xr 9543  df-ltxr 9544  df-le 9545  df-sub 9720  df-neg 9721  df-div 10124  df-nn 10453  df-2 10511  df-3 10512  df-4 10513  df-5 10514  df-6 10515  df-7 10516  df-8 10517  df-9 10518  df-10 10519  df-n0 10713  df-z 10782  df-dec 10896  df-uz 11002  df-rp 11140  df-fz 11594  df-fzo 11718  df-seq 12011  df-exp 12070  df-hash 12308  df-word 12446  df-lsw 12447  df-concat 12448  df-s1 12449  df-substr 12450  df-splice 12451  df-reverse 12452  df-s2 12724  df-struct 14636  df-ndx 14637  df-slot 14638  df-base 14639  df-sets 14640  df-ress 14641  df-plusg 14715  df-mulr 14716  df-starv 14717  df-sca 14718  df-vsca 14719  df-ip 14720  df-tset 14721  df-ple 14722  df-ds 14724  df-unif 14725  df-hom 14726  df-cco 14727  df-0g 14849  df-gsum 14850  df-prds 14855  df-pws 14857  df-mre 14993  df-mrc 14994  df-acs 14996  df-mgm 15989  df-sgrp 16028  df-mnd 16038  df-mhm 16083  df-submnd 16084  df-grp 16174  df-minusg 16175  df-sbg 16176  df-mulg 16177  df-subg 16315  df-ghm 16382  df-gim 16424  df-cntz 16472  df-oppg 16498  df-symg 16520  df-pmtr 16584  df-psgn 16633  df-evpm 16634  df-cmn 16917  df-abl 16918  df-mgp 17255  df-ur 17267  df-srg 17271  df-ring 17313  df-cring 17314  df-oppr 17385  df-dvdsr 17403  df-unit 17404  df-invr 17434  df-dvr 17445  df-rnghom 17477  df-drng 17511  df-subrg 17540  df-lmod 17627  df-lss 17692  df-sra 17931  df-rgmod 17932  df-cnfld 18534  df-zring 18602  df-zrh 18634  df-dsmm 18854  df-frlm 18869  df-mamu 18971  df-mat 18995  df-mdet 19172

This theorem is referenced by:  mdetuni  19209  mdetmul  19210