Theorem mdetuni0 18432

Description: Lemma for mdetuni 18433. (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		rnggrp 16655	. . . . . . . . 9 |- ( R e. Ring -> R e. Grp )
11	9, 10	syl 16	. . . . . . . 8 |- ( ph -> R e. Grp )
12	11	adantr 465	. . . . . . 7 |- ( ( ph /\ a e. B ) -> R e. Grp )
13		mdetuni.ff	. . . . . . . 8 |- ( ph -> D : B --> K )
14	13	ffvelrnda 5848	. . . . . . 7 |- ( ( ph /\ a e. B ) -> ( D ` a ) e. K )
15	9	adantr 465	. . . . . . . 8 |- ( ( ph /\ a e. B ) -> R e. Ring )
16	8, 9	jca 532	. . . . . . . . . . 11 |- ( ph -> ( N e. Fin /\ R e. Ring ) )
17	1	matrng 18335	. . . . . . . . . . 11 |- ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
18		eqid 2443	. . . . . . . . . . . 12 |- ( 1r ` A ) = ( 1r ` A )
19	2, 18	rngidcl 16670	. . . . . . . . . . 11 |- ( A e. Ring -> ( 1r ` A ) e. B )
20	16, 17, 19	3syl 20	. . . . . . . . . 10 |- ( ph -> ( 1r ` A ) e. B )
21	13, 20	ffvelrnd 5849	. . . . . . . . 9 |- ( ph -> ( D ` ( 1r ` A ) ) e. K )
22	21	adantr 465	. . . . . . . 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 18411	. . . . . . . . . 10 |- ( R e. CRing -> E : B --> K )
26	23, 25	syl 16	. . . . . . . . 9 |- ( ph -> E : B --> K )
27	26	ffvelrnda 5848	. . . . . . . 8 |- ( ( ph /\ a e. B ) -> ( E ` a ) e. K )
28	3, 7	rngcl 16663	. . . . . . . 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 1218	. . . . . . 7 |- ( ( ph /\ a e. B ) -> ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) e. K )
30		eqid 2443	. . . . . . . 8 |- ( -g ` R ) = ( -g ` R )
31	3, 30	grpsubcl 15611	. . . . . . 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 1218	. . . . . 6 |- ( ( ph /\ a e. B ) -> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) e. K )
33		eqid 2443	. . . . . 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 5872	. . . . 5 |- ( ph -> ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) : B --> K )
35		simpr1 994	. . . . . . . . . 10 |- ( ( ph /\ ( b e. B /\ c e. N /\ d e. N ) ) -> b e. B )
36		fveq2 5696	. . . . . . . . . . . 12 |- ( a = b -> ( D ` a ) = ( D ` b ) )
37		fveq2 5696	. . . . . . . . . . . . 13 |- ( a = b -> ( E ` a ) = ( E ` b ) )
38	37	oveq2d 6112	. . . . . . . . . . . 12 |- ( a = b -> ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) = ( ( D ` ( 1r ` A ) ) .x. ( E ` b ) ) )
39	36, 38	oveq12d 6114	. . . . . . . . . . 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 6121	. . . . . . . . . . 11 |- ( ( D ` b ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` b ) ) ) e. _V
41	39, 33, 40	fvmpt 5779	. . . . . . . . . 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 1008	. . . . . . . 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 988	. . . . . . . . . 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 1021	. . . . . . . . . 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 1017	. . . . . . . . . . 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 6104	. . . . . . . . . . . . 13 |- ( e = w -> ( c b e ) = ( c b w ) )
48		oveq2 6104	. . . . . . . . . . . . 13 |- ( e = w -> ( d b e ) = ( d b w ) )
49	47, 48	eqeq12d 2457	. . . . . . . . . . . 12 |- ( e = w -> ( ( c b e ) = ( d b e ) <-> ( c b w ) = ( d b w ) ) )
50	49	cbvralv 2952	. . . . . . . . . . 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 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 e. N )
53		simp23 1023	. . . . . . . . . 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 1016	. . . . . . . . . 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 18423	. . . . . . . . . 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 1233	. . . . . . . . 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 1009	. . . . . . . . . . 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 18419	. . . . . . . . . 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 6112	. . . . . . . . 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 6114	. . . . . . . 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	rngrz 16687	. . . . . . . . . . . 12 |- ( ( R e. Ring /\ ( D ` ( 1r ` A ) ) e. K ) -> ( ( D ` ( 1r ` A ) ) .x. .0. ) = .0. )
65	9, 21, 64	syl2anc 661	. . . . . . . . . . 11 |- ( ph -> ( ( D ` ( 1r ` A ) ) .x. .0. ) = .0. )
66	65	oveq2d 6112	. . . . . . . . . 10 |- ( ph -> ( .0. ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. .0. ) ) = ( .0. ( -g ` R ) .0. ) )
67	3, 4	grpidcl 15571	. . . . . . . . . . . 12 |- ( R e. Grp -> .0. e. K )
68	11, 67	syl 16	. . . . . . . . . . 11 |- ( ph -> .0. e. K )
69	3, 4, 30	grpsubid 15615	. . . . . . . . . . 11 |- ( ( R e. Grp /\ .0. e. K ) -> ( .0. ( -g ` R ) .0. ) = .0. )
70	11, 68, 69	syl2anc 661	. . . . . . . . . 10 |- ( ph -> ( .0. ( -g ` R ) .0. ) = .0. )
71	66, 70	eqtrd 2475	. . . . . . . . 9 |- ( ph -> ( .0. ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. .0. ) ) = .0. )
72	71	3ad2ant1 1009	. . . . . . . 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 2479	. . . . . . 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 1189	. . . . . 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 2814	. . . . 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 988	. . . . . . . . . . . 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 1055	. . . . . . . . . . . 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 1056	. . . . . . . . . . . 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 1057	. . . . . . . . . . . 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 1058	. . . . . . . . . . . 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 1024	. . . . . . . . . . . 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 1025	. . . . . . . . . . . 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 1026	. . . . . . . . . . . 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 18425	. . . . . . . . . . . 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 1249	. . . . . . . . . . 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 1009	. . . . . . . . . . . . 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 18414	. . . . . . . . . . . 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 6112	. . . . . . . . . . 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 6114	. . . . . . . . . 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 1008	. . . . . . . . . 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 5696	. . . . . . . . . . . . . . . 16 |- ( a = c -> ( D ` a ) = ( D ` c ) )
95		fveq2 5696	. . . . . . . . . . . . . . . . 17 |- ( a = c -> ( E ` a ) = ( E ` c ) )
96	95	oveq2d 6112	. . . . . . . . . . . . . . . 16 |- ( a = c -> ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) = ( ( D ` ( 1r ` A ) ) .x. ( E ` c ) ) )
97	94, 96	oveq12d 6114	. . . . . . . . . . . . . . 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 6121	. . . . . . . . . . . . . . 15 |- ( ( D ` c ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` c ) ) ) e. _V
99	97, 33, 98	fvmpt 5779	. . . . . . . . . . . . . 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 5696	. . . . . . . . . . . . . . . 16 |- ( a = d -> ( D ` a ) = ( D ` d ) )
103		fveq2 5696	. . . . . . . . . . . . . . . . 17 |- ( a = d -> ( E ` a ) = ( E ` d ) )
104	103	oveq2d 6112	. . . . . . . . . . . . . . . 16 |- ( a = d -> ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) = ( ( D ` ( 1r ` A ) ) .x. ( E ` d ) ) )
105	102, 104	oveq12d 6114	. . . . . . . . . . . . . . 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 6121	. . . . . . . . . . . . . . 15 |- ( ( D ` d ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` d ) ) ) e. _V
107	105, 33, 106	fvmpt 5779	. . . . . . . . . . . . . 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 6114	. . . . . . . . . . . 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		rngabl 16679	. . . . . . . . . . . . . . 15 |- ( R e. Ring -> R e. Abel )
111	9, 110	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> R e. Abel )
112	111	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> R e. Abel )
113	13	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> D : B --> K )
114	113, 93	ffvelrnd 5849	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( D ` c ) e. K )
115	113, 101	ffvelrnd 5849	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( D ` d ) e. K )
116	9	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> R e. Ring )
117	21	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( D ` ( 1r ` A ) ) e. K )
118	26	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> E : B --> K )
119	118, 93	ffvelrnd 5849	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( E ` c ) e. K )
120	3, 7	rngcl 16663	. . . . . . . . . . . . . 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 1218	. . . . . . . . . . . . 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 5849	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( E ` d ) e. K )
123	3, 7	rngcl 16663	. . . . . . . . . . . . . 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 1218	. . . . . . . . . . . . 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 16307	. . . . . . . . . . . . 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 1227	. . . . . . . . . . . 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	rngdi 16668	. . . . . . . . . . . . . . 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 1220	. . . . . . . . . . . . . 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 2448	. . . . . . . . . . . . 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 6112	. . . . . . . . . . . 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 2481	. . . . . . . . . . 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 1008	. . . . . . . . . 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 2485	. . . . . . . . 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 1189	. . . . . . . 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 648	. . . . . . 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 2813	. . . . . 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 2813	. . . . 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 988	. . . . . . . . . . . 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 1055	. . . . . . . . . . . 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 1056	. . . . . . . . . . . 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 1057	. . . . . . . . . . . 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 1058	. . . . . . . . . . . 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 1016	. . . . . . . . . . . 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 1017	. . . . . . . . . . . 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 18426	. . . . . . . . . . . 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 1241	. . . . . . . . . . 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 1009	. . . . . . . . . . . . 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 18415	. . . . . . . . . . . 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 6112	. . . . . . . . . . 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 6114	. . . . . . . . . 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 1008	. . . . . . . . . 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 6112	. . . . . . . . . . . 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 465	. . . . . . . . . . . . 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 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> D : B --> K )
160	159, 154	ffvelrnd 5849	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> ( D ` d ) e. K )
161	21	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> ( D ` ( 1r ` A ) ) e. K )
162	26	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> E : B --> K )
163	162, 154	ffvelrnd 5849	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> ( E ` d ) e. K )
164	157, 161, 163, 123	syl3anc 1218	. . . . . . . . . . . . 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	rngsubdi 16695	. . . . . . . . . . . 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 2443	. . . . . . . . . . . . . . . . 17 |- (mulGrp ` R ) = (mulGrp ` R )
167	166	crngmgp 16658	. . . . . . . . . . . . . . . 16 |- ( R e. CRing -> (mulGrp ` R ) e. CMnd )
168	23, 167	syl 16	. . . . . . . . . . . . . . 15 |- ( ph -> (mulGrp ` R ) e. CMnd )
169	168	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> (mulGrp ` R ) e. CMnd )
170	166, 3	mgpbas 16602	. . . . . . . . . . . . . . 15 |- K = ( Base ` (mulGrp ` R ) )
171	166, 7	mgpplusg 16600	. . . . . . . . . . . . . . 15 |- .x. = ( +g ` (mulGrp ` R ) )
172	170, 171	cmn12 16302	. . . . . . . . . . . . . 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 1220	. . . . . . . . . . . . 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 6112	. . . . . . . . . . . 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 2479	. . . . . . . . . . 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 1008	. . . . . . . . . 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 2485	. . . . . . . . 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 1189	. . . . . . . 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 648	. . . . . . 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 2813	. . . . . 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 2813	. . . . 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 2444	. . . . . 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 5696	. . . . . . . 8 |- ( a = ( 1r ` A ) -> ( D ` a ) = ( D ` ( 1r ` A ) ) )
184		fveq2 5696	. . . . . . . . 9 |- ( a = ( 1r ` A ) -> ( E ` a ) = ( E ` ( 1r ` A ) ) )
185	184	oveq2d 6112	. . . . . . . 8 |- ( a = ( 1r ` A ) -> ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) = ( ( D ` ( 1r ` A ) ) .x. ( E ` ( 1r ` A ) ) ) )
186	183, 185	oveq12d 6114	. . . . . . 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 18413	. . . . . . . . . . . 12 |- ( ( R e. CRing /\ N e. Fin ) -> ( E ` ( 1r ` A ) ) = .1. )
188	23, 8, 187	syl2anc 661	. . . . . . . . . . 11 |- ( ph -> ( E ` ( 1r ` A ) ) = .1. )
189	188	oveq2d 6112	. . . . . . . . . 10 |- ( ph -> ( ( D ` ( 1r ` A ) ) .x. ( E ` ( 1r ` A ) ) ) = ( ( D ` ( 1r ` A ) ) .x. .1. ) )
190	3, 7, 5	rngridm 16674	. . . . . . . . . . 11 |- ( ( R e. Ring /\ ( D ` ( 1r ` A ) ) e. K ) -> ( ( D ` ( 1r ` A ) ) .x. .1. ) = ( D ` ( 1r ` A ) ) )
191	9, 21, 190	syl2anc 661	. . . . . . . . . 10 |- ( ph -> ( ( D ` ( 1r ` A ) ) .x. .1. ) = ( D ` ( 1r ` A ) ) )
192	189, 191	eqtrd 2475	. . . . . . . . 9 |- ( ph -> ( ( D ` ( 1r ` A ) ) .x. ( E ` ( 1r ` A ) ) ) = ( D ` ( 1r ` A ) ) )
193	192	oveq2d 6112	. . . . . . . 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 15615	. . . . . . . . 9 |- ( ( R e. Grp /\ ( D ` ( 1r ` A ) ) e. K ) -> ( ( D ` ( 1r ` A ) ) ( -g ` R ) ( D ` ( 1r ` A ) ) ) = .0. )
195	11, 21, 194	syl2anc 661	. . . . . . . 8 |- ( ph -> ( ( D ` ( 1r ` A ) ) ( -g ` R ) ( D ` ( 1r ` A ) ) ) = .0. )
196	193, 195	eqtrd 2475	. . . . . . 7 |- ( ph -> ( ( D ` ( 1r ` A ) ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` ( 1r ` A ) ) ) ) = .0. )
197	186, 196	sylan9eqr 2497	. . . . . 6 |- ( ( ph /\ a = ( 1r ` A ) ) -> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) = .0. )
198		fvex 5706	. . . . . . . 8 |- ( 0g ` R ) e. _V
199	4, 198	eqeltri 2513	. . . . . . 7 |- .0. e. _V
200	199	a1i 11	. . . . . 6 |- ( ph -> .0. e. _V )
201	182, 197, 20, 200	fvmptd 5784	. . . . 5 |- ( ph -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` ( 1r ` A ) ) = .0. )
202		eqid 2443	. . . . 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 18431	. . . 4 |- ( ph -> ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) = ( B X. { .0. } ) )
204	203	fveq1d 5698	. . 3 |- ( ph -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` F ) = ( ( B X. { .0. } ) ` F ) )
205		fveq2 5696	. . . . . 6 |- ( a = F -> ( D ` a ) = ( D ` F ) )
206		fveq2 5696	. . . . . . 7 |- ( a = F -> ( E ` a ) = ( E ` F ) )
207	206	oveq2d 6112	. . . . . 6 |- ( a = F -> ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) = ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) )
208	205, 207	oveq12d 6114	. . . . 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 466	. . . 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 6121	. . . . 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 5784	. . 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 5938	. . . 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 2483	. 2 |- ( ph -> ( ( D ` F ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) ) = .0. )
217	13, 210	ffvelrnd 5849	. . 3 |- ( ph -> ( D ` F ) e. K )
218	26, 210	ffvelrnd 5849	. . . 4 |- ( ph -> ( E ` F ) e. K )
219	3, 7	rngcl 16663	. . . 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 1218	. . 3 |- ( ph -> ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) e. K )
221	3, 4, 30	grpsubeq0 15617	. . 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 1218	. 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 369   /\ w3a 965   = wceq 1369   e. wcel 1756   {cab 2429   =/= wne 2611   A.wral 2720   _Vcvv 2977   \ cdif 3330   ifcif 3796   {csn 3882   e. cmpt 4355   X. cxp 4843   |` cres 4847   -->wf 5419   ` cfv 5423  (class class class)co 6096   oFcof 6323   ^m cmap 7219   Fincfn 7315   Basecbs 14179   +g cplusg 14243   .rcmulr 14244   0gc0g 14383   Grpcgrp 15415   -gcsg 15418  CMndccmn 16282   Abelcabel 16283  mulGrpcmgp 16596   1rcur 16608   Ringcrg 16650   CRingccrg 16651   Mat cmat 18285   maDet cmdat 18400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4408  ax-sep 4418  ax-nul 4426  ax-pow 4475  ax-pr 4536  ax-un 6377  ax-inf2 7852  ax-cnex 9343  ax-resscn 9344  ax-1cn 9345  ax-icn 9346  ax-addcl 9347  ax-addrcl 9348  ax-mulcl 9349  ax-mulrcl 9350  ax-mulcom 9351  ax-addass 9352  ax-mulass 9353  ax-distr 9354  ax-i2m1 9355  ax-1ne0 9356  ax-1rid 9357  ax-rnegex 9358  ax-rrecex 9359  ax-cnre 9360  ax-pre-lttri 9361  ax-pre-lttrn 9362  ax-pre-ltadd 9363  ax-pre-mulgt0 9364  ax-addf 9366  ax-mulf 9367

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-xor 1351  df-tru 1372  df-fal 1375  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-nel 2614  df-ral 2725  df-rex 2726  df-reu 2727  df-rmo 2728  df-rab 2729  df-v 2979  df-sbc 3192  df-csb 3294  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-pss 3349  df-nul 3643  df-if 3797  df-pw 3867  df-sn 3883  df-pr 3885  df-tp 3887  df-op 3889  df-ot 3891  df-uni 4097  df-int 4134  df-iun 4178  df-iin 4179  df-br 4298  df-opab 4356  df-mpt 4357  df-tr 4391  df-eprel 4637  df-id 4641  df-po 4646  df-so 4647  df-fr 4684  df-se 4685  df-we 4686  df-ord 4727  df-on 4728  df-lim 4729  df-suc 4730  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5386  df-fun 5425  df-fn 5426  df-f 5427  df-f1 5428  df-fo 5429  df-f1o 5430  df-fv 5431  df-isom 5432  df-riota 6057  df-ov 6099  df-oprab 6100  df-mpt2 6101  df-of 6325  df-om 6482  df-1st 6582  df-2nd 6583  df-supp 6696  df-tpos 6750  df-recs 6837  df-rdg 6871  df-1o 6925  df-2o 6926  df-oadd 6929  df-er 7106  df-map 7221  df-pm 7222  df-ixp 7269  df-en 7316  df-dom 7317  df-sdom 7318  df-fin 7319  df-fsupp 7626  df-sup 7696  df-oi 7729  df-card 8114  df-pnf 9425  df-mnf 9426  df-xr 9427  df-ltxr 9428  df-le 9429  df-sub 9602  df-neg 9603  df-div 9999  df-nn 10328  df-2 10385  df-3 10386  df-4 10387  df-5 10388  df-6 10389  df-7 10390  df-8 10391  df-9 10392  df-10 10393  df-n0 10585  df-z 10652  df-dec 10761  df-uz 10867  df-rp 10997  df-fz 11443  df-fzo 11554  df-seq 11812  df-exp 11871  df-hash 12109  df-word 12234  df-concat 12236  df-s1 12237  df-substr 12238  df-splice 12239  df-reverse 12240  df-s2 12480  df-struct 14181  df-ndx 14182  df-slot 14183  df-base 14184  df-sets 14185  df-ress 14186  df-plusg 14256  df-mulr 14257  df-starv 14258  df-sca 14259  df-vsca 14260  df-ip 14261  df-tset 14262  df-ple 14263  df-ds 14265  df-unif 14266  df-hom 14267  df-cco 14268  df-0g 14385  df-gsum 14386  df-prds 14391  df-pws 14393  df-mre 14529  df-mrc 14530  df-acs 14532  df-mnd 15420  df-mhm 15469  df-submnd 15470  df-grp 15550  df-minusg 15551  df-sbg 15552  df-mulg 15553  df-subg 15683  df-ghm 15750  df-gim 15792  df-cntz 15840  df-oppg 15866  df-symg 15888  df-pmtr 15953  df-psgn 16002  df-evpm 16003  df-cmn 16284  df-abl 16285  df-mgp 16597  df-ur 16609  df-rng 16652  df-cring 16653  df-oppr 16720  df-dvdsr 16738  df-unit 16739  df-invr 16769  df-dvr 16780  df-rnghom 16811  df-drng 16839  df-subrg 16868  df-lmod 16955  df-lss 17019  df-sra 17258  df-rgmod 17259  df-cnfld 17824  df-zring 17889  df-zrh 17940  df-dsmm 18162  df-frlm 18177  df-mamu 18286  df-mat 18287  df-mdet 18401

This theorem is referenced by:  mdetuni  18433  mdetmul  18434