Theorem mdetuni0 18990

Description: Lemma for mdetuni 18991. (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 17071	. . . . . . . . 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 6012	. . . . . . 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	matring 18812	. . . . . . . . . . 11 |- ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
18		eqid 2441	. . . . . . . . . . . 12 |- ( 1r ` A ) = ( 1r ` A )
19	2, 18	ringidcl 17087	. . . . . . . . . . 11 |- ( A e. Ring -> ( 1r ` A ) e. B )
20	16, 17, 19	3syl 20	. . . . . . . . . 10 |- ( ph -> ( 1r ` A ) e. B )
21	13, 20	ffvelrnd 6013	. . . . . . . . 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 18964	. . . . . . . . . 10 |- ( R e. CRing -> E : B --> K )
26	23, 25	syl 16	. . . . . . . . 9 |- ( ph -> E : B --> K )
27	26	ffvelrnda 6012	. . . . . . . 8 |- ( ( ph /\ a e. B ) -> ( E ` a ) e. K )
28	3, 7	ringcl 17080	. . . . . . . 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 1227	. . . . . . 7 |- ( ( ph /\ a e. B ) -> ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) e. K )
30		eqid 2441	. . . . . . . 8 |- ( -g ` R ) = ( -g ` R )
31	3, 30	grpsubcl 15987	. . . . . . 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 1227	. . . . . 6 |- ( ( ph /\ a e. B ) -> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) e. K )
33		eqid 2441	. . . . . 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 6036	. . . . 5 |- ( ph -> ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) : B --> K )
35		simpr1 1001	. . . . . . . . . 10 |- ( ( ph /\ ( b e. B /\ c e. N /\ d e. N ) ) -> b e. B )
36		fveq2 5852	. . . . . . . . . . . 12 |- ( a = b -> ( D ` a ) = ( D ` b ) )
37		fveq2 5852	. . . . . . . . . . . . 13 |- ( a = b -> ( E ` a ) = ( E ` b ) )
38	37	oveq2d 6293	. . . . . . . . . . . 12 |- ( a = b -> ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) = ( ( D ` ( 1r ` A ) ) .x. ( E ` b ) ) )
39	36, 38	oveq12d 6295	. . . . . . . . . . 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 6305	. . . . . . . . . . 11 |- ( ( D ` b ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` b ) ) ) e. _V
41	39, 33, 40	fvmpt 5937	. . . . . . . . . 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 1015	. . . . . . . 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 995	. . . . . . . . . 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 1028	. . . . . . . . . 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 1024	. . . . . . . . . . 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 6285	. . . . . . . . . . . . 13 |- ( e = w -> ( c b e ) = ( c b w ) )
48		oveq2 6285	. . . . . . . . . . . . 13 |- ( e = w -> ( d b e ) = ( d b w ) )
49	47, 48	eqeq12d 2463	. . . . . . . . . . . 12 |- ( e = w -> ( ( c b e ) = ( d b e ) <-> ( c b w ) = ( d b w ) ) )
50	49	cbvralv 3068	. . . . . . . . . . 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 1029	. . . . . . . . . 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 1030	. . . . . . . . . 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 1023	. . . . . . . . . 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 18981	. . . . . . . . . 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 1242	. . . . . . . . 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 1016	. . . . . . . . . . 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 18977	. . . . . . . . . 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 6293	. . . . . . . . 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 6295	. . . . . . . 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 17104	. . . . . . . . . . . 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 6293	. . . . . . . . . 10 |- ( ph -> ( .0. ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. .0. ) ) = ( .0. ( -g ` R ) .0. ) )
67	3, 4	grpidcl 15947	. . . . . . . . . . . 12 |- ( R e. Grp -> .0. e. K )
68	11, 67	syl 16	. . . . . . . . . . 11 |- ( ph -> .0. e. K )
69	3, 4, 30	grpsubid 15991	. . . . . . . . . . 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 2482	. . . . . . . . 9 |- ( ph -> ( .0. ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. .0. ) ) = .0. )
72	71	3ad2ant1 1016	. . . . . . . 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 2486	. . . . . . 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 1197	. . . . . 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 2863	. . . . 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 995	. . . . . . . . . . . 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 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 ) ) ) ) -> b e. B )
78		simp2lr 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 ) ) ) ) -> c e. B )
79		simp2rl 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 ) ) ) ) -> d e. B )
80		simp2rr 1065	. . . . . . . . . . . 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 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 |` ( { e } X. N ) ) = ( ( c |` ( { e } X. N ) ) oF .+ ( d |` ( { e } X. N ) ) ) )
82		simp32 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 ) ) = ( c |` ( ( N \ { e } ) X. N ) ) )
83		simp33 1033	. . . . . . . . . . . 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 18983	. . . . . . . . . . . 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 1258	. . . . . . . . . . 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 1016	. . . . . . . . . . . . 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 18971	. . . . . . . . . . . 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 6293	. . . . . . . . . . 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 6295	. . . . . . . . . 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 1015	. . . . . . . . . 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 5852	. . . . . . . . . . . . . . . 16 |- ( a = c -> ( D ` a ) = ( D ` c ) )
95		fveq2 5852	. . . . . . . . . . . . . . . . 17 |- ( a = c -> ( E ` a ) = ( E ` c ) )
96	95	oveq2d 6293	. . . . . . . . . . . . . . . 16 |- ( a = c -> ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) = ( ( D ` ( 1r ` A ) ) .x. ( E ` c ) ) )
97	94, 96	oveq12d 6295	. . . . . . . . . . . . . . 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 6305	. . . . . . . . . . . . . . 15 |- ( ( D ` c ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` c ) ) ) e. _V
99	97, 33, 98	fvmpt 5937	. . . . . . . . . . . . . 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 5852	. . . . . . . . . . . . . . . 16 |- ( a = d -> ( D ` a ) = ( D ` d ) )
103		fveq2 5852	. . . . . . . . . . . . . . . . 17 |- ( a = d -> ( E ` a ) = ( E ` d ) )
104	103	oveq2d 6293	. . . . . . . . . . . . . . . 16 |- ( a = d -> ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) = ( ( D ` ( 1r ` A ) ) .x. ( E ` d ) ) )
105	102, 104	oveq12d 6295	. . . . . . . . . . . . . . 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 6305	. . . . . . . . . . . . . . 15 |- ( ( D ` d ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` d ) ) ) e. _V
107	105, 33, 106	fvmpt 5937	. . . . . . . . . . . . . 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 6295	. . . . . . . . . . . 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 17096	. . . . . . . . . . . . . . 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 6013	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( D ` c ) e. K )
115	113, 101	ffvelrnd 6013	. . . . . . . . . . . . 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 6013	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( E ` c ) e. K )
120	3, 7	ringcl 17080	. . . . . . . . . . . . . 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 1227	. . . . . . . . . . . . 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 6013	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. B ) /\ ( d e. B /\ e e. N ) ) ) -> ( E ` d ) e. K )
123	3, 7	ringcl 17080	. . . . . . . . . . . . . 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 1227	. . . . . . . . . . . . 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 16692	. . . . . . . . . . . . 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 1236	. . . . . . . . . . . 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 17085	. . . . . . . . . . . . . . 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 1229	. . . . . . . . . . . . . 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 2449	. . . . . . . . . . . . 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 6293	. . . . . . . . . . . 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 2488	. . . . . . . . . . 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 1015	. . . . . . . . . 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 2492	. . . . . . . . 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 1197	. . . . . . . 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 2862	. . . . . 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 2862	. . . . 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 995	. . . . . . . . . . . 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 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 ) ) ) ) -> b e. B )
140		simp2lr 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 ) ) ) ) -> c e. K )
141		simp2rl 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 ) ) ) ) -> d e. B )
142		simp2rr 1065	. . . . . . . . . . . 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 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 |` ( { e } X. N ) ) = ( ( ( { e } X. N ) X. { c } ) oF .x. ( d |` ( { e } X. N ) ) ) )
144		simp3r 1024	. . . . . . . . . . . 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 18984	. . . . . . . . . . . 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 1250	. . . . . . . . . . 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 1016	. . . . . . . . . . . . 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 18972	. . . . . . . . . . . 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 6293	. . . . . . . . . . 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 6295	. . . . . . . . . 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 1015	. . . . . . . . . 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 6293	. . . . . . . . . . . 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 6013	. . . . . . . . . . . . 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 6013	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( b e. B /\ c e. K ) /\ ( d e. B /\ e e. N ) ) ) -> ( E ` d ) e. K )
164	157, 161, 163, 123	syl3anc 1227	. . . . . . . . . . . . 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 17113	. . . . . . . . . . . 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 2441	. . . . . . . . . . . . . . . . 17 |- (mulGrp ` R ) = (mulGrp ` R )
167	166	crngmgp 17074	. . . . . . . . . . . . . . . 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 17015	. . . . . . . . . . . . . . 15 |- K = ( Base ` (mulGrp ` R ) )
171	166, 7	mgpplusg 17013	. . . . . . . . . . . . . . 15 |- .x. = ( +g ` (mulGrp ` R ) )
172	170, 171	cmn12 16687	. . . . . . . . . . . . . 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 1229	. . . . . . . . . . . . 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 6293	. . . . . . . . . . . 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 2486	. . . . . . . . . . 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 1015	. . . . . . . . . 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 2492	. . . . . . . . 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 1197	. . . . . . . 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 2862	. . . . . 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 2862	. . . . 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 2442	. . . . . 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 5852	. . . . . . . 8 |- ( a = ( 1r ` A ) -> ( D ` a ) = ( D ` ( 1r ` A ) ) )
184		fveq2 5852	. . . . . . . . 9 |- ( a = ( 1r ` A ) -> ( E ` a ) = ( E ` ( 1r ` A ) ) )
185	184	oveq2d 6293	. . . . . . . 8 |- ( a = ( 1r ` A ) -> ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) = ( ( D ` ( 1r ` A ) ) .x. ( E ` ( 1r ` A ) ) ) )
186	183, 185	oveq12d 6295	. . . . . . 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 18970	. . . . . . . . . . . 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 6293	. . . . . . . . . 10 |- ( ph -> ( ( D ` ( 1r ` A ) ) .x. ( E ` ( 1r ` A ) ) ) = ( ( D ` ( 1r ` A ) ) .x. .1. ) )
190	3, 7, 5	ringridm 17091	. . . . . . . . . . 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 2482	. . . . . . . . 9 |- ( ph -> ( ( D ` ( 1r ` A ) ) .x. ( E ` ( 1r ` A ) ) ) = ( D ` ( 1r ` A ) ) )
193	192	oveq2d 6293	. . . . . . . 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 15991	. . . . . . . . 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 2482	. . . . . . 7 |- ( ph -> ( ( D ` ( 1r ` A ) ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` ( 1r ` A ) ) ) ) = .0. )
197	186, 196	sylan9eqr 2504	. . . . . 6 |- ( ( ph /\ a = ( 1r ` A ) ) -> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) = .0. )
198		fvex 5862	. . . . . . . 8 |- ( 0g ` R ) e. _V
199	4, 198	eqeltri 2525	. . . . . . 7 |- .0. e. _V
200	199	a1i 11	. . . . . 6 |- ( ph -> .0. e. _V )
201	182, 197, 20, 200	fvmptd 5942	. . . . 5 |- ( ph -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` ( 1r ` A ) ) = .0. )
202		eqid 2441	. . . . 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 18989	. . . 4 |- ( ph -> ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) = ( B X. { .0. } ) )
204	203	fveq1d 5854	. . 3 |- ( ph -> ( ( a e. B |-> ( ( D ` a ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) ) ) ` F ) = ( ( B X. { .0. } ) ` F ) )
205		fveq2 5852	. . . . . 6 |- ( a = F -> ( D ` a ) = ( D ` F ) )
206		fveq2 5852	. . . . . . 7 |- ( a = F -> ( E ` a ) = ( E ` F ) )
207	206	oveq2d 6293	. . . . . 6 |- ( a = F -> ( ( D ` ( 1r ` A ) ) .x. ( E ` a ) ) = ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) )
208	205, 207	oveq12d 6295	. . . . 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 6305	. . . . 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 5942	. . 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 6107	. . . 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 2490	. 2 |- ( ph -> ( ( D ` F ) ( -g ` R ) ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) ) = .0. )
217	13, 210	ffvelrnd 6013	. . 3 |- ( ph -> ( D ` F ) e. K )
218	26, 210	ffvelrnd 6013	. . . 4 |- ( ph -> ( E ` F ) e. K )
219	3, 7	ringcl 17080	. . . 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 1227	. . 3 |- ( ph -> ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) e. K )
221	3, 4, 30	grpsubeq0 15993	. . 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 1227	. 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 972   = wceq 1381   e. wcel 1802   {cab 2426   =/= wne 2636   A.wral 2791   _Vcvv 3093   \ cdif 3455   ifcif 3922   {csn 4010   |-> cmpt 4491   X. cxp 4983   |` cres 4987   -->wf 5570   ` cfv 5574  (class class class)co 6277   oFcof 6519   ^m cmap 7418   Fincfn 7514   Basecbs 14504   +g cplusg 14569   .rcmulr 14570   0gc0g 14709   Grpcgrp 15922   -gcsg 15924  CMndccmn 16667   Abelcabl 16668  mulGrpcmgp 17009   1rcur 17021   Ringcrg 17066   CRingccrg 17067   Mat cmat 18776   maDet cmdat 18953

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-rep 4544  ax-sep 4554  ax-nul 4562  ax-pow 4611  ax-pr 4672  ax-un 6573  ax-inf2 8056  ax-cnex 9546  ax-resscn 9547  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-mulcom 9554  ax-addass 9555  ax-mulass 9556  ax-distr 9557  ax-i2m1 9558  ax-1ne0 9559  ax-1rid 9560  ax-rnegex 9561  ax-rrecex 9562  ax-cnre 9563  ax-pre-lttri 9564  ax-pre-lttrn 9565  ax-pre-ltadd 9566  ax-pre-mulgt0 9567  ax-addf 9569  ax-mulf 9570

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-xor 1363  df-tru 1384  df-fal 1387  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-nel 2639  df-ral 2796  df-rex 2797  df-reu 2798  df-rmo 2799  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3418  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-pss 3474  df-nul 3768  df-if 3923  df-pw 3995  df-sn 4011  df-pr 4013  df-tp 4015  df-op 4017  df-ot 4019  df-uni 4231  df-int 4268  df-iun 4313  df-iin 4314  df-br 4434  df-opab 4492  df-mpt 4493  df-tr 4527  df-eprel 4777  df-id 4781  df-po 4786  df-so 4787  df-fr 4824  df-se 4825  df-we 4826  df-ord 4867  df-on 4868  df-lim 4869  df-suc 4870  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fun 5576  df-fn 5577  df-f 5578  df-f1 5579  df-fo 5580  df-f1o 5581  df-fv 5582  df-isom 5583  df-riota 6238  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-of 6521  df-om 6682  df-1st 6781  df-2nd 6782  df-supp 6900  df-tpos 6953  df-recs 7040  df-rdg 7074  df-1o 7128  df-2o 7129  df-oadd 7132  df-er 7309  df-map 7420  df-pm 7421  df-ixp 7468  df-en 7515  df-dom 7516  df-sdom 7517  df-fin 7518  df-fsupp 7828  df-sup 7899  df-oi 7933  df-card 8318  df-cda 8546  df-pnf 9628  df-mnf 9629  df-xr 9630  df-ltxr 9631  df-le 9632  df-sub 9807  df-neg 9808  df-div 10208  df-nn 10538  df-2 10595  df-3 10596  df-4 10597  df-5 10598  df-6 10599  df-7 10600  df-8 10601  df-9 10602  df-10 10603  df-n0 10797  df-z 10866  df-dec 10980  df-uz 11086  df-rp 11225  df-fz 11677  df-fzo 11799  df-seq 12082  df-exp 12141  df-hash 12380  df-word 12516  df-concat 12518  df-s1 12519  df-substr 12520  df-splice 12521  df-reverse 12522  df-s2 12787  df-struct 14506  df-ndx 14507  df-slot 14508  df-base 14509  df-sets 14510  df-ress 14511  df-plusg 14582  df-mulr 14583  df-starv 14584  df-sca 14585  df-vsca 14586  df-ip 14587  df-tset 14588  df-ple 14589  df-ds 14591  df-unif 14592  df-hom 14593  df-cco 14594  df-0g 14711  df-gsum 14712  df-prds 14717  df-pws 14719  df-mre 14855  df-mrc 14856  df-acs 14858  df-mgm 15741  df-sgrp 15780  df-mnd 15790  df-mhm 15835  df-submnd 15836  df-grp 15926  df-minusg 15927  df-sbg 15928  df-mulg 15929  df-subg 16067  df-ghm 16134  df-gim 16176  df-cntz 16224  df-oppg 16250  df-symg 16272  df-pmtr 16336  df-psgn 16385  df-evpm 16386  df-cmn 16669  df-abl 16670  df-mgp 17010  df-ur 17022  df-srg 17026  df-ring 17068  df-cring 17069  df-oppr 17140  df-dvdsr 17158  df-unit 17159  df-invr 17189  df-dvr 17200  df-rnghom 17232  df-drng 17266  df-subrg 17295  df-lmod 17382  df-lss 17447  df-sra 17686  df-rgmod 17687  df-cnfld 18289  df-zring 18357  df-zrh 18408  df-dsmm 18630  df-frlm 18645  df-mamu 18753  df-mat 18777  df-mdet 18954

This theorem is referenced by:  mdetuni  18991  mdetmul  18992