Theorem svli2 14826

Description: If a finite sequence of vectors U(k) are linearly independant, two combinations of those vectors are equal iff the scalars are equal.

Hypotheses

Ref	Expression
svli2.1	|- X = ran +t
svli2.2	|- 0t = (Id` +t )
svli2.7	|- +t = (1st` (1st` R))
svli2.3	|- .t = (2nd` (1st` R))
svli2.4	|- 0w = (Id` +w )
svli2.5	|- +w = (1st` (2nd` R))
svli2.6	|- W = ran +w
svli2.8	|- .w = (2nd` (2nd` R))

Assertion

Ref	Expression
svli2	|- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) /\ A.s e. (X ^m (1...N))(prod_k e. (1...N)+w ((s` k).w U) = 0w -> A.k e. (1...N)(s` k) = 0t )) -> (prod_k e. (1...N)+w (S1.w U) = prod_k e. (1...N)+w (S2.w U) <-> A.k e. (1...N)S1 = S2))

Distinct variable groups:   k,+_t ,s   k,+_w ,s   k,._t   s,._w   s,0_t   k,0_w ,s   k,N,s   R,k   s,S₁   s,S₂   U,s   k,W   k,X,s

Proof of Theorem svli2

Step	Hyp	Ref	Expression
1		simp11 906	. . 3 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) /\ A.s e. (X ^m (1...N))(prod_k e. (1...N)+w ((s` k).w U) = 0w -> A.k e. (1...N)(s` k) = 0t )) -> R e. Vec)
2		elnnuz 7609	. . . . . . . . 9 |- (N e. NN <-> N e. (ZZ>=` 1))
3	2	biimpi 168	. . . . . . . 8 |- (N e. NN -> N e. (ZZ>=` 1))
4	3	3ad2ant3 899	. . . . . . 7 |- ((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) -> N e. (ZZ>=` 1))
5	4	adantr 425	. . . . . 6 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X)) -> N e. (ZZ>=` 1))
6		svli2.5	. . . . . . . . 9 |- +w = (1st` (2nd` R))
7	6	vecax1 14796	. . . . . . . 8 |- (R e. Vec -> +w e. Abel)
8	7	3ad2ant1 897	. . . . . . 7 |- ((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) -> +w e. Abel)
9	8	adantr 425	. . . . . 6 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X)) -> +w e. Abel)
10		r19.26 2219	. . . . . . . . . . 11 |- (A.k e. (1...N)(U e. W /\ S1 e. X) <-> (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X))
11		svli2.8	. . . . . . . . . . . . . . . . . 18 |- .w = (2nd` (2nd` R))
12		svli2.6	. . . . . . . . . . . . . . . . . 18 |- W = ran +w
13		svli2.1	. . . . . . . . . . . . . . . . . 18 |- X = ran +t
14		svli2.7	. . . . . . . . . . . . . . . . . 18 |- +t = (1st` (1st` R))
15	6, 11, 12, 13, 14	prodvs 14811	. . . . . . . . . . . . . . . . 17 |- ((R e. Vec /\ S1 e. X /\ U e. W) -> (S1.w U) e. W)
16	15	3exp 1066	. . . . . . . . . . . . . . . 16 |- (R e. Vec -> (S1 e. X -> (U e. W -> (S1.w U) e. W)))
17	16	com13 37	. . . . . . . . . . . . . . 15 |- (U e. W -> (S1 e. X -> (R e. Vec -> (S1.w U) e. W)))
18	17	imp 377	. . . . . . . . . . . . . 14 |- ((U e. W /\ S1 e. X) -> (R e. Vec -> (S1.w U) e. W))
19	18	com12 14	. . . . . . . . . . . . 13 |- (R e. Vec -> ((U e. W /\ S1 e. X) -> (S1.w U) e. W))
20	19	ralimdv 2172	. . . . . . . . . . . 12 |- (R e. Vec -> (A.k e. (1...N)(U e. W /\ S1 e. X) -> A.k e. (1...N)(S1.w U) e. W))
21	20	com12 14	. . . . . . . . . . 11 |- (A.k e. (1...N)(U e. W /\ S1 e. X) -> (R e. Vec -> A.k e. (1...N)(S1.w U) e. W))
22	10, 21	sylbir 218	. . . . . . . . . 10 |- ((A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X) -> (R e. Vec -> A.k e. (1...N)(S1.w U) e. W))
23	22	3adant3 896	. . . . . . . . 9 |- ((A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) -> (R e. Vec -> A.k e. (1...N)(S1.w U) e. W))
24	23	com12 14	. . . . . . . 8 |- (R e. Vec -> ((A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) -> A.k e. (1...N)(S1.w U) e. W))
25	24	3ad2ant1 897	. . . . . . 7 |- ((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) -> ((A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) -> A.k e. (1...N)(S1.w U) e. W))
26	25	imp 377	. . . . . 6 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X)) -> A.k e. (1...N)(S1.w U) e. W)
27	12	clfsebs5 14745	. . . . . 6 |- ((N e. (ZZ>=` 1) /\ +w e. Abel /\ A.k e. (1...N)(S1.w U) e. W) -> prod_k e. (1...N)+w (S1.w U) e. W)
28	5, 9, 26, 27	syl111anc 1100	. . . . 5 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X)) -> prod_k e. (1...N)+w (S1.w U) e. W)
29		r19.26 2219	. . . . . . . . . . 11 |- (A.k e. (1...N)(U e. W /\ S2 e. X) <-> (A.k e. (1...N)U e. W /\ A.k e. (1...N)S2 e. X))
30	6, 11, 12, 13, 14	prodvs 14811	. . . . . . . . . . . . . . . . 17 |- ((R e. Vec /\ S2 e. X /\ U e. W) -> (S2.w U) e. W)
31	30	3exp 1066	. . . . . . . . . . . . . . . 16 |- (R e. Vec -> (S2 e. X -> (U e. W -> (S2.w U) e. W)))
32	31	com13 37	. . . . . . . . . . . . . . 15 |- (U e. W -> (S2 e. X -> (R e. Vec -> (S2.w U) e. W)))
33	32	imp 377	. . . . . . . . . . . . . 14 |- ((U e. W /\ S2 e. X) -> (R e. Vec -> (S2.w U) e. W))
34	33	com12 14	. . . . . . . . . . . . 13 |- (R e. Vec -> ((U e. W /\ S2 e. X) -> (S2.w U) e. W))
35	34	ralimdv 2172	. . . . . . . . . . . 12 |- (R e. Vec -> (A.k e. (1...N)(U e. W /\ S2 e. X) -> A.k e. (1...N)(S2.w U) e. W))
36	35	com12 14	. . . . . . . . . . 11 |- (A.k e. (1...N)(U e. W /\ S2 e. X) -> (R e. Vec -> A.k e. (1...N)(S2.w U) e. W))
37	29, 36	sylbir 218	. . . . . . . . . 10 |- ((A.k e. (1...N)U e. W /\ A.k e. (1...N)S2 e. X) -> (R e. Vec -> A.k e. (1...N)(S2.w U) e. W))
38	37	3adant2 895	. . . . . . . . 9 |- ((A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) -> (R e. Vec -> A.k e. (1...N)(S2.w U) e. W))
39	38	com12 14	. . . . . . . 8 |- (R e. Vec -> ((A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) -> A.k e. (1...N)(S2.w U) e. W))
40	39	3ad2ant1 897	. . . . . . 7 |- ((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) -> ((A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) -> A.k e. (1...N)(S2.w U) e. W))
41	40	imp 377	. . . . . 6 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X)) -> A.k e. (1...N)(S2.w U) e. W)
42	12	clfsebs5 14745	. . . . . 6 |- ((N e. (ZZ>=` 1) /\ +w e. Abel /\ A.k e. (1...N)(S2.w U) e. W) -> prod_k e. (1...N)+w (S2.w U) e. W)
43	5, 9, 41, 42	syl111anc 1100	. . . . 5 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X)) -> prod_k e. (1...N)+w (S2.w U) e. W)
44	28, 43	jca 310	. . . 4 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X)) -> (prod_k e. (1...N)+w (S1.w U) e. W /\ prod_k e. (1...N)+w (S2.w U) e. W))
45	44	3adant3 896	. . 3 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) /\ A.s e. (X ^m (1...N))(prod_k e. (1...N)+w ((s` k).w U) = 0w -> A.k e. (1...N)(s` k) = 0t )) -> (prod_k e. (1...N)+w (S1.w U) e. W /\ prod_k e. (1...N)+w (S2.w U) e. W))
46		svli2.4	. . . 4 |- 0w = (Id` +w )
47		eqid 1884	. . . 4 |- ( /g ` +w ) = ( /g ` +w )
48	46, 6, 47, 12	mvecrtol 14816	. . 3 |- ((R e. Vec /\ (prod_k e. (1...N)+w (S1.w U) e. W /\ prod_k e. (1...N)+w (S2.w U) e. W)) -> (prod_k e. (1...N)+w (S1.w U) = prod_k e. (1...N)+w (S2.w U) <-> (prod_k e. (1...N)+w (S1.w U)( /g ` +w )prod_k e. (1...N)+w (S2.w U)) = 0w ))
49	1, 45, 48	syl11anc 524	. 2 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) /\ A.s e. (X ^m (1...N))(prod_k e. (1...N)+w ((s` k).w U) = 0w -> A.k e. (1...N)(s` k) = 0t )) -> (prod_k e. (1...N)+w (S1.w U) = prod_k e. (1...N)+w (S2.w U) <-> (prod_k e. (1...N)+w (S1.w U)( /g ` +w )prod_k e. (1...N)+w (S2.w U)) = 0w ))
50		r19.26 2219	. . . . . . 7 |- (A.k e. (1...N)((S1.w U) e. W /\ (S2.w U) e. W) <-> (A.k e. (1...N)(S1.w U) e. W /\ A.k e. (1...N)(S2.w U) e. W))
51	50, 26, 41	sylanbrc 527	. . . . . 6 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X)) -> A.k e. (1...N)((S1.w U) e. W /\ (S2.w U) e. W))
52	5, 51, 9	3jca 1050	. . . . 5 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X)) -> (N e. (ZZ>=` 1) /\ A.k e. (1...N)((S1.w U) e. W /\ (S2.w U) e. W) /\ +w e. Abel))
53	52	3adant3 896	. . . 4 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) /\ A.s e. (X ^m (1...N))(prod_k e. (1...N)+w ((s` k).w U) = 0w -> A.k e. (1...N)(s` k) = 0t )) -> (N e. (ZZ>=` 1) /\ A.k e. (1...N)((S1.w U) e. W /\ (S2.w U) e. W) /\ +w e. Abel))
54	12, 47	fprodsub 14742	. . . . 5 |- ((N e. (ZZ>=` 1) /\ A.k e. (1...N)((S1.w U) e. W /\ (S2.w U) e. W) /\ +w e. Abel) -> prod_k e. (1...N)+w ((S1.w U)( /g ` +w )(S2.w U)) = (prod_k e. (1...N)+w (S1.w U)( /g ` +w )prod_k e. (1...N)+w (S2.w U)))
55	54	eqcomd 1889	. . . 4 |- ((N e. (ZZ>=` 1) /\ A.k e. (1...N)((S1.w U) e. W /\ (S2.w U) e. W) /\ +w e. Abel) -> (prod_k e. (1...N)+w (S1.w U)( /g ` +w )prod_k e. (1...N)+w (S2.w U)) = prod_k e. (1...N)+w ((S1.w U)( /g ` +w )(S2.w U)))
56	53, 55	syl 12	. . 3 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) /\ A.s e. (X ^m (1...N))(prod_k e. (1...N)+w ((s` k).w U) = 0w -> A.k e. (1...N)(s` k) = 0t )) -> (prod_k e. (1...N)+w (S1.w U)( /g ` +w )prod_k e. (1...N)+w (S2.w U)) = prod_k e. (1...N)+w ((S1.w U)( /g ` +w )(S2.w U)))
57	56	eqeq1d 1892	. 2 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) /\ A.s e. (X ^m (1...N))(prod_k e. (1...N)+w ((s` k).w U) = 0w -> A.k e. (1...N)(s` k) = 0t )) -> ((prod_k e. (1...N)+w (S1.w U)( /g ` +w )prod_k e. (1...N)+w (S2.w U)) = 0w <-> prod_k e. (1...N)+w ((S1.w U)( /g ` +w )(S2.w U)) = 0w ))
58		eqid 1884	. . . . . . . . . . . . . 14 |- ( /g ` +t ) = ( /g ` +t )
59		svli2.3	. . . . . . . . . . . . . 14 |- .t = (2nd` (1st` R))
60	13, 14, 58, 6, 47, 11, 12, 59	vecax5c 14825	. . . . . . . . . . . . 13 |- ((R e. Vec /\ <.+t , .t >. e. Ring) -> ((U e. W /\ S1 e. X /\ S2 e. X) -> ((S1( /g ` +t )S2).w U) = ((S1.w U)( /g ` +w )(S2.w U))))
61	60	3adant3 896	. . . . . . . . . . . 12 |- ((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) -> ((U e. W /\ S1 e. X /\ S2 e. X) -> ((S1( /g ` +t )S2).w U) = ((S1.w U)( /g ` +w )(S2.w U))))
62	61	imp 377	. . . . . . . . . . 11 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (U e. W /\ S1 e. X /\ S2 e. X)) -> ((S1( /g ` +t )S2).w U) = ((S1.w U)( /g ` +w )(S2.w U)))
63	62	eqcomd 1889	. . . . . . . . . 10 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (U e. W /\ S1 e. X /\ S2 e. X)) -> ((S1.w U)( /g ` +w )(S2.w U)) = ((S1( /g ` +t )S2).w U))
64	63	ex 402	. . . . . . . . 9 |- ((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) -> ((U e. W /\ S1 e. X /\ S2 e. X) -> ((S1.w U)( /g ` +w )(S2.w U)) = ((S1( /g ` +t )S2).w U)))
65	64	ralimdv 2172	. . . . . . . 8 |- ((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) -> (A.k e. (1...N)(U e. W /\ S1 e. X /\ S2 e. X) -> A.k e. (1...N)((S1.w U)( /g ` +w )(S2.w U)) = ((S1( /g ` +t )S2).w U)))
66		r19.26t 14282	. . . . . . . 8 |- (A.k e. (1...N)(U e. W /\ S1 e. X /\ S2 e. X) <-> (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X))
67	65, 66	syl5ibr 224	. . . . . . 7 |- ((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) -> ((A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) -> A.k e. (1...N)((S1.w U)( /g ` +w )(S2.w U)) = ((S1( /g ` +t )S2).w U)))
68	67	imp 377	. . . . . 6 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X)) -> A.k e. (1...N)((S1.w U)( /g ` +w )(S2.w U)) = ((S1( /g ` +t )S2).w U))
69	68	3adant3 896	. . . . 5 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) /\ A.s e. (X ^m (1...N))(prod_k e. (1...N)+w ((s` k).w U) = 0w -> A.k e. (1...N)(s` k) = 0t )) -> A.k e. (1...N)((S1.w U)( /g ` +w )(S2.w U)) = ((S1( /g ` +t )S2).w U))
70		fvex 4689	. . . . . . 7 |- (1st` (2nd` R)) e. _V
71	6, 70	eqeltri 1967	. . . . . 6 |- +w e. _V
72	71	prodeq2 14661	. . . . 5 |- (A.k e. (1...N)((S1.w U)( /g ` +w )(S2.w U)) = ((S1( /g ` +t )S2).w U) -> prod_k e. (1...N)+w ((S1.w U)( /g ` +w )(S2.w U)) = prod_k e. (1...N)+w ((S1( /g ` +t )S2).w U))
73	69, 72	syl 12	. . . 4 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) /\ A.s e. (X ^m (1...N))(prod_k e. (1...N)+w ((s` k).w U) = 0w -> A.k e. (1...N)(s` k) = 0t )) -> prod_k e. (1...N)+w ((S1.w U)( /g ` +w )(S2.w U)) = prod_k e. (1...N)+w ((S1( /g ` +t )S2).w U))
74	73	eqeq1d 1892	. . 3 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) /\ A.s e. (X ^m (1...N))(prod_k e. (1...N)+w ((s` k).w U) = 0w -> A.k e. (1...N)(s` k) = 0t )) -> (prod_k e. (1...N)+w ((S1.w U)( /g ` +w )(S2.w U)) = 0w <-> prod_k e. (1...N)+w ((S1( /g ` +t )S2).w U) = 0w ))
75		r19.26 2219	. . . . . . . . . . . 12 |- (A.k e. (1...N)(S1 e. X /\ S2 e. X) <-> (A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X))
76	13, 58	grpdivcl 9371	. . . . . . . . . . . . . . 15 |- ((+t e. Grp /\ S1 e. X /\ S2 e. X) -> (S1( /g ` +t )S2) e. X)
77	76	3expib 1070	. . . . . . . . . . . . . 14 |- (+t e. Grp -> ((S1 e. X /\ S2 e. X) -> (S1( /g ` +t )S2) e. X))
78	77	ralimdv 2172	. . . . . . . . . . . . 13 |- (+t e. Grp -> (A.k e. (1...N)(S1 e. X /\ S2 e. X) -> A.k e. (1...N)(S1( /g ` +t )S2) e. X))
79	78	com12 14	. . . . . . . . . . . 12 |- (A.k e. (1...N)(S1 e. X /\ S2 e. X) -> (+t e. Grp -> A.k e. (1...N)(S1( /g ` +t )S2) e. X))
80	75, 79	sylbir 218	. . . . . . . . . . 11 |- ((A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) -> (+t e. Grp -> A.k e. (1...N)(S1( /g ` +t )S2) e. X))
81	80	3adant1 894	. . . . . . . . . 10 |- ((A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) -> (+t e. Grp -> A.k e. (1...N)(S1( /g ` +t )S2) e. X))
82		fvex 4689	. . . . . . . . . . . . . 14 |- (1st` (1st` R)) e. _V
83	14, 82	eqeltri 1967	. . . . . . . . . . . . 13 |- +t e. _V
84	83	op1st 5026	. . . . . . . . . . . 12 |- (1st` <.+t , .t >.) = +t
85	84	eqcomi 1888	. . . . . . . . . . 11 |- +t = (1st` <.+t , .t >.)
86	85	ringgrp 9476	. . . . . . . . . 10 |- (<.+t , .t >. e. Ring -> +t e. Grp)
87	81, 86	syl5com 63	. . . . . . . . 9 |- (<.+t , .t >. e. Ring -> ((A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) -> A.k e. (1...N)(S1( /g ` +t )S2) e. X))
88	87	3ad2ant2 898	. . . . . . . 8 |- ((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) -> ((A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) -> A.k e. (1...N)(S1( /g ` +t )S2) e. X))
89	88	imp 377	. . . . . . 7 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X)) -> A.k e. (1...N)(S1( /g ` +t )S2) e. X)
90		eqid 1884	. . . . . . . 8 |- {<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))} = {<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))}
91	90	fopab2 4796	. . . . . . 7 |- (A.k e. (1...N)(S1( /g ` +t )S2) e. X <-> {<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))}:(1...N)-->X)
92	89, 91	sylib 215	. . . . . 6 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X)) -> {<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))}:(1...N)-->X)
93	83	rnex 4209	. . . . . . . 8 |- ran +t e. _V
94	13, 93	eqeltri 1967	. . . . . . 7 |- X e. _V
95		oprex 4907	. . . . . . 7 |- (1...N) e. _V
96	94, 95	elmap 5393	. . . . . 6 |- ({<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))} e. (X ^m (1...N)) <-> {<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))}:(1...N)-->X)
97	92, 96	sylibr 217	. . . . 5 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X)) -> {<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))} e. (X ^m (1...N)))
98	97	3adant3 896	. . . 4 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) /\ A.s e. (X ^m (1...N))(prod_k e. (1...N)+w ((s` k).w U) = 0w -> A.k e. (1...N)(s` k) = 0t )) -> {<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))} e. (X ^m (1...N)))
99		ax-17 1317	. . . . . . . . . . . . . . 15 |- (u e. s -> A.k u e. s)
100		hbopab1 3562	. . . . . . . . . . . . . . 15 |- (u e. {<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))} -> A.k u e. {<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))})
101	99, 100	hbeq 1995	. . . . . . . . . . . . . 14 |- (s = {<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))} -> A.k s = {<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))})
102		fveq1 4680	. . . . . . . . . . . . . . . 16 |- (s = {<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))} -> (s` k) = ({<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))}` k))
103	102	opreq1d 4897	. . . . . . . . . . . . . . 15 |- (s = {<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))} -> ((s` k).w U) = (({<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))}` k).w U))
104	103	a1d 15	. . . . . . . . . . . . . 14 |- (s = {<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))} -> (k e. (1...N) -> ((s` k).w U) = (({<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))}` k).w U)))
105	101, 104	r19.21ai 2174	. . . . . . . . . . . . 13 |- (s = {<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))} -> A.k e. (1...N)((s` k).w U) = (({<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))}` k).w U))
106	71	prodeq2 14661	. . . . . . . . . . . . 13 |- (A.k e. (1...N)((s` k).w U) = (({<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))}` k).w U) -> prod_k e. (1...N)+w ((s` k).w U) = prod_k e. (1...N)+w (({<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))}` k).w U))
107	105, 106	syl 12	. . . . . . . . . . . 12 |- (s = {<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))} -> prod_k e. (1...N)+w ((s` k).w U) = prod_k e. (1...N)+w (({<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))}` k).w U))
108	107	eqeq1d 1892	. . . . . . . . . . 11 |- (s = {<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))} -> (prod_k e. (1...N)+w ((s` k).w U) = 0w <-> prod_k e. (1...N)+w (({<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))}` k).w U) = 0w ))
109	102	eqeq1d 1892	. . . . . . . . . . . 12 |- (s = {<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))} -> ((s` k) = 0t <-> ({<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))}` k) = 0t ))
110	101, 109	ralbid 2121	. . . . . . . . . . 11 |- (s = {<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))} -> (A.k e. (1...N)(s` k) = 0t <-> A.k e. (1...N)({<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))}` k) = 0t ))
111	108, 110	imbi12d 688	. . . . . . . . . 10 |- (s = {<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))} -> ((prod_k e. (1...N)+w ((s` k).w U) = 0w -> A.k e. (1...N)(s` k) = 0t ) <-> (prod_k e. (1...N)+w (({<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))}` k).w U) = 0w -> A.k e. (1...N)({<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))}` k) = 0t )))
112	71	prodeq2 14661	. . . . . . . . . . . . 13 |- (A.k e. (1...N)(({<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))}` k).w U) = ((S1( /g ` +t )S2).w U) -> prod_k e. (1...N)+w (({<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))}` k).w U) = prod_k e. (1...N)+w ((S1( /g ` +t )S2).w U))
113		oprex 4907	. . . . . . . . . . . . . . 15 |- (S1( /g ` +t )S2) e. _V
114		fvopab2 4754	. . . . . . . . . . . . . . 15 |- ((k e. (1...N) /\ (S1( /g ` +t )S2) e. _V) -> ({<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))}` k) = (S1( /g ` +t )S2))
115	113, 114	mpan2 760	. . . . . . . . . . . . . 14 |- (k e. (1...N) -> ({<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))}` k) = (S1( /g ` +t )S2))
116	115	opreq1d 4897	. . . . . . . . . . . . 13 |- (k e. (1...N) -> (({<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))}` k).w U) = ((S1( /g ` +t )S2).w U))
117	112, 116	mprg 2162	. . . . . . . . . . . 12 |- prod_k e. (1...N)+w (({<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))}` k).w U) = prod_k e. (1...N)+w ((S1( /g ` +t )S2).w U)
118	117	eqeq1i 1891	. . . . . . . . . . 11 |- (prod_k e. (1...N)+w (({<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))}` k).w U) = 0w <-> prod_k e. (1...N)+w ((S1( /g ` +t )S2).w U) = 0w )
119	115	eqeq1d 1892	. . . . . . . . . . . 12 |- (k e. (1...N) -> (({<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))}` k) = 0t <-> (S1( /g ` +t )S2) = 0t ))
120	119	ralbiia 2133	. . . . . . . . . . 11 |- (A.k e. (1...N)({<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))}` k) = 0t <-> A.k e. (1...N)(S1( /g ` +t )S2) = 0t )
121	118, 120	imbi12i 205	. . . . . . . . . 10 |- ((prod_k e. (1...N)+w (({<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))}` k).w U) = 0w -> A.k e. (1...N)({<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))}` k) = 0t ) <-> (prod_k e. (1...N)+w ((S1( /g ` +t )S2).w U) = 0w -> A.k e. (1...N)(S1( /g ` +t )S2) = 0t ))
122	111, 121	syl6bb 595	. . . . . . . . 9 |- (s = {<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))} -> ((prod_k e. (1...N)+w ((s` k).w U) = 0w -> A.k e. (1...N)(s` k) = 0t ) <-> (prod_k e. (1...N)+w ((S1( /g ` +t )S2).w U) = 0w -> A.k e. (1...N)(S1( /g ` +t )S2) = 0t )))
123	122	rcla4v 2376	. . . . . . . 8 |- ({<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))} e. (X ^m (1...N)) -> (A.s e. (X ^m (1...N))(prod_k e. (1...N)+w ((s` k).w U) = 0w -> A.k e. (1...N)(s` k) = 0t ) -> (prod_k e. (1...N)+w ((S1( /g ` +t )S2).w U) = 0w -> A.k e. (1...N)(S1( /g ` +t )S2) = 0t )))
124	123	com12 14	. . . . . . 7 |- (A.s e. (X ^m (1...N))(prod_k e. (1...N)+w ((s` k).w U) = 0w -> A.k e. (1...N)(s` k) = 0t ) -> ({<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))} e. (X ^m (1...N)) -> (prod_k e. (1...N)+w ((S1( /g ` +t )S2).w U) = 0w -> A.k e. (1...N)(S1( /g ` +t )S2) = 0t )))
125	124	3ad2ant3 899	. . . . . 6 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) /\ A.s e. (X ^m (1...N))(prod_k e. (1...N)+w ((s` k).w U) = 0w -> A.k e. (1...N)(s` k) = 0t )) -> ({<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))} e. (X ^m (1...N)) -> (prod_k e. (1...N)+w ((S1( /g ` +t )S2).w U) = 0w -> A.k e. (1...N)(S1( /g ` +t )S2) = 0t )))
126	125	imp 377	. . . . 5 |- ((((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) /\ A.s e. (X ^m (1...N))(prod_k e. (1...N)+w ((s` k).w U) = 0w -> A.k e. (1...N)(s` k) = 0t )) /\ {<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))} e. (X ^m (1...N))) -> (prod_k e. (1...N)+w ((S1( /g ` +t )S2).w U) = 0w -> A.k e. (1...N)(S1( /g ` +t )S2) = 0t ))
127		opreq1 4889	. . . . . . . . . 10 |- ((S1( /g ` +t )S2) = 0t -> ((S1( /g ` +t )S2).w U) = (0t .w U))
128	127	ralimi 2168	. . . . . . . . 9 |- (A.k e. (1...N)(S1( /g ` +t )S2) = 0t -> A.k e. (1...N)((S1( /g ` +t )S2).w U) = (0t .w U))
129	71	prodeq2 14661	. . . . . . . . 9 |- (A.k e. (1...N)((S1( /g ` +t )S2).w U) = (0t .w U) -> prod_k e. (1...N)+w ((S1( /g ` +t )S2).w U) = prod_k e. (1...N)+w (0t .w U))
130	128, 129	syl 12	. . . . . . . 8 |- (A.k e. (1...N)(S1( /g ` +t )S2) = 0t -> prod_k e. (1...N)+w ((S1( /g ` +t )S2).w U) = prod_k e. (1...N)+w (0t .w U))
131	130	adantl 424	. . . . . . 7 |- (((((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) /\ A.s e. (X ^m (1...N))(prod_k e. (1...N)+w ((s` k).w U) = 0w -> A.k e. (1...N)(s` k) = 0t )) /\ {<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))} e. (X ^m (1...N))) /\ A.k e. (1...N)(S1( /g ` +t )S2) = 0t ) -> prod_k e. (1...N)+w ((S1( /g ` +t )S2).w U) = prod_k e. (1...N)+w (0t .w U))
132	6	rneqi 4187	. . . . . . . . . . . . . . . . . . 19 |- ran +w = ran (1st` (2nd` R))
133	12, 132	eqtri 1908	. . . . . . . . . . . . . . . . . 18 |- W = ran (1st` (2nd` R))
134		svli2.2	. . . . . . . . . . . . . . . . . 18 |- 0t = (Id` +t )
135	6	fveq2i 4684	. . . . . . . . . . . . . . . . . . 19 |- (Id` +w ) = (Id` (1st` (2nd` R)))
136	46, 135	eqtri 1908	. . . . . . . . . . . . . . . . . 18 |- 0w = (Id` (1st` (2nd` R)))
137	133, 134, 14, 59, 11, 136	mulveczer 14822	. . . . . . . . . . . . . . . . 17 |- ((R e. Vec /\ <.+t , .t >. e. Ring /\ U e. W) -> (0t .w U) = 0w )
138	137	3expia 1069	. . . . . . . . . . . . . . . 16 |- ((R e. Vec /\ <.+t , .t >. e. Ring) -> (U e. W -> (0t .w U) = 0w ))
139	138	ralimdv 2172	. . . . . . . . . . . . . . 15 |- ((R e. Vec /\ <.+t , .t >. e. Ring) -> (A.k e. (1...N)U e. W -> A.k e. (1...N)(0t .w U) = 0w ))
140	139	com12 14	. . . . . . . . . . . . . 14 |- (A.k e. (1...N)U e. W -> ((R e. Vec /\ <.+t , .t >. e. Ring) -> A.k e. (1...N)(0t .w U) = 0w ))
141	140	3ad2ant1 897	. . . . . . . . . . . . 13 |- ((A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) -> ((R e. Vec /\ <.+t , .t >. e. Ring) -> A.k e. (1...N)(0t .w U) = 0w ))
142	141	com12 14	. . . . . . . . . . . 12 |- ((R e. Vec /\ <.+t , .t >. e. Ring) -> ((A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) -> A.k e. (1...N)(0t .w U) = 0w ))
143	142	3adant3 896	. . . . . . . . . . 11 |- ((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) -> ((A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) -> A.k e. (1...N)(0t .w U) = 0w ))
144	143	imp 377	. . . . . . . . . 10 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X)) -> A.k e. (1...N)(0t .w U) = 0w )
145	71	prodeq2 14661	. . . . . . . . . 10 |- (A.k e. (1...N)(0t .w U) = 0w -> prod_k e. (1...N)+w (0t .w U) = prod_k e. (1...N)+w 0w )
146	144, 145	syl 12	. . . . . . . . 9 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X)) -> prod_k e. (1...N)+w (0t .w U) = prod_k e. (1...N)+w 0w )
147	146	3adant3 896	. . . . . . . 8 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) /\ A.s e. (X ^m (1...N))(prod_k e. (1...N)+w ((s` k).w U) = 0w -> A.k e. (1...N)(s` k) = 0t )) -> prod_k e. (1...N)+w (0t .w U) = prod_k e. (1...N)+w 0w )
148	147	ad2antrr 440	. . . . . . 7 |- (((((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) /\ A.s e. (X ^m (1...N))(prod_k e. (1...N)+w ((s` k).w U) = 0w -> A.k e. (1...N)(s` k) = 0t )) /\ {<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))} e. (X ^m (1...N))) /\ A.k e. (1...N)(S1( /g ` +t )S2) = 0t ) -> prod_k e. (1...N)+w (0t .w U) = prod_k e. (1...N)+w 0w )
149		ablgrp 9410	. . . . . . . . . . . . 13 |- (+w e. Abel -> +w e. Grp)
150		grpmnd 10393	. . . . . . . . . . . . 13 |- (+w e. Grp -> +w e. Mnd)
151	149, 150	syl 12	. . . . . . . . . . . 12 |- (+w e. Abel -> +w e. Mnd)
152		mndmgmid 10389	. . . . . . . . . . . 12 |- (+w e. Mnd -> +w e. (Magma i^i ExId ))
153	7, 151, 152	3syl 24	. . . . . . . . . . 11 |- (R e. Vec -> +w e. (Magma i^i ExId ))
154	153	3ad2ant1 897	. . . . . . . . . 10 |- ((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) -> +w e. (Magma i^i ExId ))
155	46	fincmpzer 14711	. . . . . . . . . 10 |- ((N e. (ZZ>=` 1) /\ +w e. (Magma i^i ExId )) -> prod_k e. (1...N)+w 0w = 0w )
156	4, 154, 155	syl11anc 524	. . . . . . . . 9 |- ((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) -> prod_k e. (1...N)+w 0w = 0w )
157	156	3ad2ant1 897	. . . . . . . 8 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) /\ A.s e. (X ^m (1...N))(prod_k e. (1...N)+w ((s` k).w U) = 0w -> A.k e. (1...N)(s` k) = 0t )) -> prod_k e. (1...N)+w 0w = 0w )
158	157	ad2antrr 440	. . . . . . 7 |- (((((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) /\ A.s e. (X ^m (1...N))(prod_k e. (1...N)+w ((s` k).w U) = 0w -> A.k e. (1...N)(s` k) = 0t )) /\ {<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))} e. (X ^m (1...N))) /\ A.k e. (1...N)(S1( /g ` +t )S2) = 0t ) -> prod_k e. (1...N)+w 0w = 0w )
159	131, 148, 158	3eqtrd 1929	. . . . . 6 |- (((((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) /\ A.s e. (X ^m (1...N))(prod_k e. (1...N)+w ((s` k).w U) = 0w -> A.k e. (1...N)(s` k) = 0t )) /\ {<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))} e. (X ^m (1...N))) /\ A.k e. (1...N)(S1( /g ` +t )S2) = 0t ) -> prod_k e. (1...N)+w ((S1( /g ` +t )S2).w U) = 0w )
160	159	ex 402	. . . . 5 |- ((((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) /\ A.s e. (X ^m (1...N))(prod_k e. (1...N)+w ((s` k).w U) = 0w -> A.k e. (1...N)(s` k) = 0t )) /\ {<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))} e. (X ^m (1...N))) -> (A.k e. (1...N)(S1( /g ` +t )S2) = 0t -> prod_k e. (1...N)+w ((S1( /g ` +t )S2).w U) = 0w ))
161	126, 160	impbid 574	. . . 4 |- ((((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) /\ A.s e. (X ^m (1...N))(prod_k e. (1...N)+w ((s` k).w U) = 0w -> A.k e. (1...N)(s` k) = 0t )) /\ {<.k, y>. | (k e. (1...N) /\ y = (S1( /g ` +t )S2))} e. (X ^m (1...N))) -> (prod_k e. (1...N)+w ((S1( /g ` +t )S2).w U) = 0w <-> A.k e. (1...N)(S1( /g ` +t )S2) = 0t ))
162	98, 161	mpdan 768	. . 3 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) /\ A.s e. (X ^m (1...N))(prod_k e. (1...N)+w ((s` k).w U) = 0w -> A.k e. (1...N)(s` k) = 0t )) -> (prod_k e. (1...N)+w ((S1( /g ` +t )S2).w U) = 0w <-> A.k e. (1...N)(S1( /g ` +t )S2) = 0t ))
163	13, 134, 58	grpdivzer 14740	. . . . . . . . . . . . . . 15 |- ((+t e. Grp /\ S1 e. X /\ S2 e. X) -> ((S1( /g ` +t )S2) = 0t <-> S1 = S2))
164	163	3exp 1066	. . . . . . . . . . . . . 14 |- (+t e. Grp -> (S1 e. X -> (S2 e. X -> ((S1( /g ` +t )S2) = 0t <-> S1 = S2))))
165	164	com3l 38	. . . . . . . . . . . . 13 |- (S1 e. X -> (S2 e. X -> (+t e. Grp -> ((S1( /g ` +t )S2) = 0t <-> S1 = S2))))
166	165	imp 377	. . . . . . . . . . . 12 |- ((S1 e. X /\ S2 e. X) -> (+t e. Grp -> ((S1( /g ` +t )S2) = 0t <-> S1 = S2)))
167	166	3adant1 894	. . . . . . . . . . 11 |- ((U e. W /\ S1 e. X /\ S2 e. X) -> (+t e. Grp -> ((S1( /g ` +t )S2) = 0t <-> S1 = S2)))
168	167	com12 14	. . . . . . . . . 10 |- (+t e. Grp -> ((U e. W /\ S1 e. X /\ S2 e. X) -> ((S1( /g ` +t )S2) = 0t <-> S1 = S2)))
169	168	ralimdv 2172	. . . . . . . . 9 |- (+t e. Grp -> (A.k e. (1...N)(U e. W /\ S1 e. X /\ S2 e. X) -> A.k e. (1...N)((S1( /g ` +t )S2) = 0t <-> S1 = S2)))
170	86, 169	syl 12	. . . . . . . 8 |- (<.+t , .t >. e. Ring -> (A.k e. (1...N)(U e. W /\ S1 e. X /\ S2 e. X) -> A.k e. (1...N)((S1( /g ` +t )S2) = 0t <-> S1 = S2)))
171	170	3ad2ant2 898	. . . . . . 7 |- ((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) -> (A.k e. (1...N)(U e. W /\ S1 e. X /\ S2 e. X) -> A.k e. (1...N)((S1( /g ` +t )S2) = 0t <-> S1 = S2)))
172		ralbi 2223	. . . . . . 7 |- (A.k e. (1...N)((S1( /g ` +t )S2) = 0t <-> S1 = S2) -> (A.k e. (1...N)(S1( /g ` +t )S2) = 0t <-> A.k e. (1...N)S1 = S2))
173	171, 172	syl6com 64	. . . . . 6 |- (A.k e. (1...N)(U e. W /\ S1 e. X /\ S2 e. X) -> ((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) -> (A.k e. (1...N)(S1( /g ` +t )S2) = 0t <-> A.k e. (1...N)S1 = S2)))
174	66, 173	sylbir 218	. . . . 5 |- ((A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) -> ((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) -> (A.k e. (1...N)(S1( /g ` +t )S2) = 0t <-> A.k e. (1...N)S1 = S2)))
175	174	impcom 378	. . . 4 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X)) -> (A.k e. (1...N)(S1( /g ` +t )S2) = 0t <-> A.k e. (1...N)S1 = S2))
176	175	3adant3 896	. . 3 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) /\ A.s e. (X ^m (1...N))(prod_k e. (1...N)+w ((s` k).w U) = 0w -> A.k e. (1...N)(s` k) = 0t )) -> (A.k e. (1...N)(S1( /g ` +t )S2) = 0t <-> A.k e. (1...N)S1 = S2))
177	74, 162, 176	3bitrd 603	. 2 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) /\ A.s e. (X ^m (1...N))(prod_k e. (1...N)+w ((s` k).w U) = 0w -> A.k e. (1...N)(s` k) = 0t )) -> (prod_k e. (1...N)+w ((S1.w U)( /g ` +w )(S2.w U)) = 0w <-> A.k e. (1...N)S1 = S2))
178	49, 57, 177	3bitrd 603	1 |- (((R e. Vec /\ <.+t , .t >. e. Ring /\ N e. NN) /\ (A.k e. (1...N)U e. W /\ A.k e. (1...N)S1 e. X /\ A.k e. (1...N)S2 e. X) /\ A.s e. (X ^m (1...N))(prod_k e. (1...N)+w ((s` k).w U) = 0w -> A.k e. (1...N)(s` k) = 0t )) -> (prod_k e. (1...N)+w (S1.w U) = prod_k e. (1...N)+w (S2.w U) <-> A.k e. (1...N)S1 = S2))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  _Vcvv 2292   i^i cin 2592  <.cop 3046  {copab 3395  ran crn 3987  -->wf 3994  ` cfv 3998  (class class class)co 4884  1stc1st 5018  2ndc2nd 5019   ^m cmap 5381  1c1 6387  NNcn 6449  ZZ>=cuz 7586  ...cfz 7637  Grpcgr 9311  Idcgi 9312   /g cgs 9314  Abelcabl 9407  Ringcring 9463   ExId cexid 10361  Magmacmagm 10365  Mndcmnd 10384  prod_cprd2 14654  Veccvec 14792

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1302  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-inf2 5731

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-nel 2020  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-mpt 5006  df-1st 5020  df-2nd 5021  df-iota 5089  df-rdg 5140  df-1o 5177  df-oadd 5179  df-omul 5180  df-er 5318  df-ec 5320  df-qs 5323  df-map 5383  df-en 5427  df-dom 5428  df-sdom 5429  df-undef 5556  df-riota 5560  df-ni 6152  df-pli 6153  df-mi 6154  df-lti 6155  df-plpq 6187  df-mpq 6188  df-enq 6189  df-nq 6190  df-plq 6191  df-mq 6192  df-rq 6193  df-ltq 6194  df-1q 6195  df-np 6238  df-1p 6239  df-plp 6240  df-mp 6241  df-ltp 6242  df-plpr 6316  df-mpr 6317  df-enr 6318  df-nr 6319  df-plr 6320  df-mr 6321  df-ltr 6322  df-0r 6323  df-1r 6324  df-m1r 6325  df-c 6392  df-0 6393  df-1 6394  df-i 6395  df-r 6396  df-plus 6397  df-mul 6398  df-lt 6399  df-sub 6511  df-neg 6513  df-pnf 6654  df-mnf 6655  df-xr 6656  df-ltxr 6657  df-le 6658  df-n 7108  df-n0 7309  df-z 7345  df-uz 7587  df-fz 7638  df-seq1 7721  df-shft 7754  df-seqz 7776  df-grp 9316  df-gid 9317  df-ginv 9318  df-gdiv 9319  df-abl 9408  df-ring 9464  df-ass 10360  df-exid 10362  df-mgm 10366  df-sgr 10378  df-mnd 10385  df-prod 14653  df-prod2 14655  df-com1 14688  df-vec 14793

Copyright terms: Public domain