Theorem islmodd 13973

Description: Properties that determine a left module. See note in isgrpd2 13271 regarding the ph on hypotheses that name structure components. (Contributed by Mario Carneiro, 22-Jun-2014.)

Hypotheses

Ref	Expression
islmodd.v	|- ( ph -> V = ( Base ` W ) )
islmodd.a	|- ( ph -> .+ = ( +g ` W ) )
islmodd.f	|- ( ph -> F = (Scalar ` W ) )
islmodd.s	|- ( ph -> .x. = ( .s ` W ) )
islmodd.b	|- ( ph -> B = ( Base ` F ) )
islmodd.p	|- ( ph -> .+^ = ( +g ` F ) )
islmodd.t	|- ( ph -> .X. = ( .r ` F ) )
islmodd.u	|- ( ph -> .1. = ( 1r ` F ) )
islmodd.r	|- ( ph -> F e. Ring )
islmodd.l	|- ( ph -> W e. Grp )
islmodd.w	|- ( ( ph /\ x e. B /\ y e. V ) -> ( x .x. y ) e. V )
islmodd.c	|- ( ( ph /\ ( x e. B /\ y e. V /\ z e. V ) ) -> ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) )
islmodd.d	|- ( ( ph /\ ( x e. B /\ y e. B /\ z e. V ) ) -> ( ( x .+^ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) )
islmodd.e	|- ( ( ph /\ ( x e. B /\ y e. B /\ z e. V ) ) -> ( ( x .X. y ) .x. z ) = ( x .x. ( y .x. z ) ) )
islmodd.g	|- ( ( ph /\ x e. V ) -> ( .1. .x. x ) = x )

Assertion

Ref	Expression
islmodd	|- ( ph -> W e. LMod )

Distinct variable groups:   y, z, .+^   x, y, z, B   ph, x, y, z   x, V, y, z   x, .+ , y, z   x, W   x, .x. , y, z   y, .X. , z   x, .1.

Allowed substitution hints:   .+^ ( x)   .X. ( x)   .1. ( y, z)   F( x, y, z)   W( y, z)

Proof of Theorem islmodd

Dummy variables u r w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		islmodd.l	. 2 |- ( ph -> W e. Grp )
2		islmodd.f	. . 3 |- ( ph -> F = (Scalar ` W ) )
3		islmodd.r	. . 3 |- ( ph -> F e. Ring )
4	2, 3	eqeltrrd 2282	. 2 |- ( ph -> (Scalar ` W ) e. Ring )
5		islmodd.w	. . . . . . . . . . 11 |- ( ( ph /\ x e. B /\ y e. V ) -> ( x .x. y ) e. V )
6	5	3expb 1206	. . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. V ) ) -> ( x .x. y ) e. V )
7	6	ralrimivva 2587	. . . . . . . . 9 |- ( ph -> A. x e. B A. y e. V ( x .x. y ) e. V )
8		oveq1 5941	. . . . . . . . . . . 12 |- ( x = r -> ( x .x. y ) = ( r .x. y ) )
9	8	eleq1d 2273	. . . . . . . . . . 11 |- ( x = r -> ( ( x .x. y ) e. V <-> ( r .x. y ) e. V ) )
10		oveq2 5942	. . . . . . . . . . . 12 |- ( y = w -> ( r .x. y ) = ( r .x. w ) )
11	10	eleq1d 2273	. . . . . . . . . . 11 |- ( y = w -> ( ( r .x. y ) e. V <-> ( r .x. w ) e. V ) )
12	9, 11	rspc2v 2889	. . . . . . . . . 10 |- ( ( r e. B /\ w e. V ) -> ( A. x e. B A. y e. V ( x .x. y ) e. V -> ( r .x. w ) e. V ) )
13	12	ad2ant2l 508	. . . . . . . . 9 |- ( ( ( x e. B /\ r e. B ) /\ ( u e. V /\ w e. V ) ) -> ( A. x e. B A. y e. V ( x .x. y ) e. V -> ( r .x. w ) e. V ) )
14	7, 13	mpan9 281	. . . . . . . 8 |- ( ( ph /\ ( ( x e. B /\ r e. B ) /\ ( u e. V /\ w e. V ) ) ) -> ( r .x. w ) e. V )
15		islmodd.c	. . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. V /\ z e. V ) ) -> ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) )
16	15	ralrimivvva 2588	. . . . . . . . 9 |- ( ph -> A. x e. B A. y e. V A. z e. V ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) )
17		oveq1 5941	. . . . . . . . . . . . . 14 |- ( x = r -> ( x .x. ( y .+ z ) ) = ( r .x. ( y .+ z ) ) )
18		oveq1 5941	. . . . . . . . . . . . . . 15 |- ( x = r -> ( x .x. z ) = ( r .x. z ) )
19	8, 18	oveq12d 5952	. . . . . . . . . . . . . 14 |- ( x = r -> ( ( x .x. y ) .+ ( x .x. z ) ) = ( ( r .x. y ) .+ ( r .x. z ) ) )
20	17, 19	eqeq12d 2219	. . . . . . . . . . . . 13 |- ( x = r -> ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) <-> ( r .x. ( y .+ z ) ) = ( ( r .x. y ) .+ ( r .x. z ) ) ) )
21		oveq1 5941	. . . . . . . . . . . . . . 15 |- ( y = w -> ( y .+ z ) = ( w .+ z ) )
22	21	oveq2d 5950	. . . . . . . . . . . . . 14 |- ( y = w -> ( r .x. ( y .+ z ) ) = ( r .x. ( w .+ z ) ) )
23	10	oveq1d 5949	. . . . . . . . . . . . . 14 |- ( y = w -> ( ( r .x. y ) .+ ( r .x. z ) ) = ( ( r .x. w ) .+ ( r .x. z ) ) )
24	22, 23	eqeq12d 2219	. . . . . . . . . . . . 13 |- ( y = w -> ( ( r .x. ( y .+ z ) ) = ( ( r .x. y ) .+ ( r .x. z ) ) <-> ( r .x. ( w .+ z ) ) = ( ( r .x. w ) .+ ( r .x. z ) ) ) )
25		oveq2 5942	. . . . . . . . . . . . . . 15 |- ( z = u -> ( w .+ z ) = ( w .+ u ) )
26	25	oveq2d 5950	. . . . . . . . . . . . . 14 |- ( z = u -> ( r .x. ( w .+ z ) ) = ( r .x. ( w .+ u ) ) )
27		oveq2 5942	. . . . . . . . . . . . . . 15 |- ( z = u -> ( r .x. z ) = ( r .x. u ) )
28	27	oveq2d 5950	. . . . . . . . . . . . . 14 |- ( z = u -> ( ( r .x. w ) .+ ( r .x. z ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) )
29	26, 28	eqeq12d 2219	. . . . . . . . . . . . 13 |- ( z = u -> ( ( r .x. ( w .+ z ) ) = ( ( r .x. w ) .+ ( r .x. z ) ) <-> ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) ) )
30	20, 24, 29	rspc3v 2892	. . . . . . . . . . . 12 |- ( ( r e. B /\ w e. V /\ u e. V ) -> ( A. x e. B A. y e. V A. z e. V ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) -> ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) ) )
31	30	3com23 1211	. . . . . . . . . . 11 |- ( ( r e. B /\ u e. V /\ w e. V ) -> ( A. x e. B A. y e. V A. z e. V ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) -> ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) ) )
32	31	3expb 1206	. . . . . . . . . 10 |- ( ( r e. B /\ ( u e. V /\ w e. V ) ) -> ( A. x e. B A. y e. V A. z e. V ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) -> ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) ) )
33	32	adantll 476	. . . . . . . . 9 |- ( ( ( x e. B /\ r e. B ) /\ ( u e. V /\ w e. V ) ) -> ( A. x e. B A. y e. V A. z e. V ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) -> ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) ) )
34	16, 33	mpan9 281	. . . . . . . 8 |- ( ( ph /\ ( ( x e. B /\ r e. B ) /\ ( u e. V /\ w e. V ) ) ) -> ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) )
35		simpll 527	. . . . . . . . . 10 |- ( ( ( x e. B /\ r e. B ) /\ ( u e. V /\ w e. V ) ) -> x e. B )
36		islmodd.d	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. V ) ) -> ( ( x .+^ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) )
37	36	3exp2 1227	. . . . . . . . . . . 12 |- ( ph -> ( x e. B -> ( y e. B -> ( z e. V -> ( ( x .+^ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) ) )
38	37	imp43 355	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. V ) ) -> ( ( x .+^ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) )
39	38	ralrimivva 2587	. . . . . . . . . 10 |- ( ( ph /\ x e. B ) -> A. y e. B A. z e. V ( ( x .+^ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) )
40	35, 39	sylan2 286	. . . . . . . . 9 |- ( ( ph /\ ( ( x e. B /\ r e. B ) /\ ( u e. V /\ w e. V ) ) ) -> A. y e. B A. z e. V ( ( x .+^ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) )
41		simprlr 538	. . . . . . . . . 10 |- ( ( ph /\ ( ( x e. B /\ r e. B ) /\ ( u e. V /\ w e. V ) ) ) -> r e. B )
42		simprrr 540	. . . . . . . . . 10 |- ( ( ph /\ ( ( x e. B /\ r e. B ) /\ ( u e. V /\ w e. V ) ) ) -> w e. V )
43		oveq2 5942	. . . . . . . . . . . . 13 |- ( y = r -> ( x .+^ y ) = ( x .+^ r ) )
44	43	oveq1d 5949	. . . . . . . . . . . 12 |- ( y = r -> ( ( x .+^ y ) .x. z ) = ( ( x .+^ r ) .x. z ) )
45		oveq1 5941	. . . . . . . . . . . . 13 |- ( y = r -> ( y .x. z ) = ( r .x. z ) )
46	45	oveq2d 5950	. . . . . . . . . . . 12 |- ( y = r -> ( ( x .x. z ) .+ ( y .x. z ) ) = ( ( x .x. z ) .+ ( r .x. z ) ) )
47	44, 46	eqeq12d 2219	. . . . . . . . . . 11 |- ( y = r -> ( ( ( x .+^ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) <-> ( ( x .+^ r ) .x. z ) = ( ( x .x. z ) .+ ( r .x. z ) ) ) )
48		oveq2 5942	. . . . . . . . . . . 12 |- ( z = w -> ( ( x .+^ r ) .x. z ) = ( ( x .+^ r ) .x. w ) )
49		oveq2 5942	. . . . . . . . . . . . 13 |- ( z = w -> ( x .x. z ) = ( x .x. w ) )
50		oveq2 5942	. . . . . . . . . . . . 13 |- ( z = w -> ( r .x. z ) = ( r .x. w ) )
51	49, 50	oveq12d 5952	. . . . . . . . . . . 12 |- ( z = w -> ( ( x .x. z ) .+ ( r .x. z ) ) = ( ( x .x. w ) .+ ( r .x. w ) ) )
52	48, 51	eqeq12d 2219	. . . . . . . . . . 11 |- ( z = w -> ( ( ( x .+^ r ) .x. z ) = ( ( x .x. z ) .+ ( r .x. z ) ) <-> ( ( x .+^ r ) .x. w ) = ( ( x .x. w ) .+ ( r .x. w ) ) ) )
53	47, 52	rspc2v 2889	. . . . . . . . . 10 |- ( ( r e. B /\ w e. V ) -> ( A. y e. B A. z e. V ( ( x .+^ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) -> ( ( x .+^ r ) .x. w ) = ( ( x .x. w ) .+ ( r .x. w ) ) ) )
54	41, 42, 53	syl2anc 411	. . . . . . . . 9 |- ( ( ph /\ ( ( x e. B /\ r e. B ) /\ ( u e. V /\ w e. V ) ) ) -> ( A. y e. B A. z e. V ( ( x .+^ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) -> ( ( x .+^ r ) .x. w ) = ( ( x .x. w ) .+ ( r .x. w ) ) ) )
55	40, 54	mpd 13	. . . . . . . 8 |- ( ( ph /\ ( ( x e. B /\ r e. B ) /\ ( u e. V /\ w e. V ) ) ) -> ( ( x .+^ r ) .x. w ) = ( ( x .x. w ) .+ ( r .x. w ) ) )
56	14, 34, 55	3jca 1179	. . . . . . 7 |- ( ( ph /\ ( ( x e. B /\ r e. B ) /\ ( u e. V /\ w e. V ) ) ) -> ( ( r .x. w ) e. V /\ ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) /\ ( ( x .+^ r ) .x. w ) = ( ( x .x. w ) .+ ( r .x. w ) ) ) )
57		islmodd.e	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. V ) ) -> ( ( x .X. y ) .x. z ) = ( x .x. ( y .x. z ) ) )
58	57	3exp2 1227	. . . . . . . . . . 11 |- ( ph -> ( x e. B -> ( y e. B -> ( z e. V -> ( ( x .X. y ) .x. z ) = ( x .x. ( y .x. z ) ) ) ) ) )
59	58	imp43 355	. . . . . . . . . 10 |- ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. V ) ) -> ( ( x .X. y ) .x. z ) = ( x .x. ( y .x. z ) ) )
60	59	ralrimivva 2587	. . . . . . . . 9 |- ( ( ph /\ x e. B ) -> A. y e. B A. z e. V ( ( x .X. y ) .x. z ) = ( x .x. ( y .x. z ) ) )
61	35, 60	sylan2 286	. . . . . . . 8 |- ( ( ph /\ ( ( x e. B /\ r e. B ) /\ ( u e. V /\ w e. V ) ) ) -> A. y e. B A. z e. V ( ( x .X. y ) .x. z ) = ( x .x. ( y .x. z ) ) )
62		oveq2 5942	. . . . . . . . . . . 12 |- ( y = r -> ( x .X. y ) = ( x .X. r ) )
63	62	oveq1d 5949	. . . . . . . . . . 11 |- ( y = r -> ( ( x .X. y ) .x. z ) = ( ( x .X. r ) .x. z ) )
64	45	oveq2d 5950	. . . . . . . . . . 11 |- ( y = r -> ( x .x. ( y .x. z ) ) = ( x .x. ( r .x. z ) ) )
65	63, 64	eqeq12d 2219	. . . . . . . . . 10 |- ( y = r -> ( ( ( x .X. y ) .x. z ) = ( x .x. ( y .x. z ) ) <-> ( ( x .X. r ) .x. z ) = ( x .x. ( r .x. z ) ) ) )
66		oveq2 5942	. . . . . . . . . . 11 |- ( z = w -> ( ( x .X. r ) .x. z ) = ( ( x .X. r ) .x. w ) )
67	50	oveq2d 5950	. . . . . . . . . . 11 |- ( z = w -> ( x .x. ( r .x. z ) ) = ( x .x. ( r .x. w ) ) )
68	66, 67	eqeq12d 2219	. . . . . . . . . 10 |- ( z = w -> ( ( ( x .X. r ) .x. z ) = ( x .x. ( r .x. z ) ) <-> ( ( x .X. r ) .x. w ) = ( x .x. ( r .x. w ) ) ) )
69	65, 68	rspc2v 2889	. . . . . . . . 9 |- ( ( r e. B /\ w e. V ) -> ( A. y e. B A. z e. V ( ( x .X. y ) .x. z ) = ( x .x. ( y .x. z ) ) -> ( ( x .X. r ) .x. w ) = ( x .x. ( r .x. w ) ) ) )
70	41, 42, 69	syl2anc 411	. . . . . . . 8 |- ( ( ph /\ ( ( x e. B /\ r e. B ) /\ ( u e. V /\ w e. V ) ) ) -> ( A. y e. B A. z e. V ( ( x .X. y ) .x. z ) = ( x .x. ( y .x. z ) ) -> ( ( x .X. r ) .x. w ) = ( x .x. ( r .x. w ) ) ) )
71	61, 70	mpd 13	. . . . . . 7 |- ( ( ph /\ ( ( x e. B /\ r e. B ) /\ ( u e. V /\ w e. V ) ) ) -> ( ( x .X. r ) .x. w ) = ( x .x. ( r .x. w ) ) )
72		islmodd.g	. . . . . . . . 9 |- ( ( ph /\ x e. V ) -> ( .1. .x. x ) = x )
73	72	ralrimiva 2578	. . . . . . . 8 |- ( ph -> A. x e. V ( .1. .x. x ) = x )
74		oveq2 5942	. . . . . . . . . . 11 |- ( x = w -> ( .1. .x. x ) = ( .1. .x. w ) )
75		id 19	. . . . . . . . . . 11 |- ( x = w -> x = w )
76	74, 75	eqeq12d 2219	. . . . . . . . . 10 |- ( x = w -> ( ( .1. .x. x ) = x <-> ( .1. .x. w ) = w ) )
77	76	rspcv 2872	. . . . . . . . 9 |- ( w e. V -> ( A. x e. V ( .1. .x. x ) = x -> ( .1. .x. w ) = w ) )
78	77	ad2antll 491	. . . . . . . 8 |- ( ( ( x e. B /\ r e. B ) /\ ( u e. V /\ w e. V ) ) -> ( A. x e. V ( .1. .x. x ) = x -> ( .1. .x. w ) = w ) )
79	73, 78	mpan9 281	. . . . . . 7 |- ( ( ph /\ ( ( x e. B /\ r e. B ) /\ ( u e. V /\ w e. V ) ) ) -> ( .1. .x. w ) = w )
80	56, 71, 79	jca32 310	. . . . . 6 |- ( ( ph /\ ( ( x e. B /\ r e. B ) /\ ( u e. V /\ w e. V ) ) ) -> ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) /\ ( ( x .+^ r ) .x. w ) = ( ( x .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( x .X. r ) .x. w ) = ( x .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w ) ) )
81	80	anassrs 400	. . . . 5 |- ( ( ( ph /\ ( x e. B /\ r e. B ) ) /\ ( u e. V /\ w e. V ) ) -> ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) /\ ( ( x .+^ r ) .x. w ) = ( ( x .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( x .X. r ) .x. w ) = ( x .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w ) ) )
82	81	ralrimivva 2587	. . . 4 |- ( ( ph /\ ( x e. B /\ r e. B ) ) -> A. u e. V A. w e. V ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) /\ ( ( x .+^ r ) .x. w ) = ( ( x .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( x .X. r ) .x. w ) = ( x .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w ) ) )
83	82	ralrimivva 2587	. . 3 |- ( ph -> A. x e. B A. r e. B A. u e. V A. w e. V ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) /\ ( ( x .+^ r ) .x. w ) = ( ( x .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( x .X. r ) .x. w ) = ( x .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w ) ) )
84		islmodd.b	. . . . 5 |- ( ph -> B = ( Base ` F ) )
85	2	fveq2d 5574	. . . . 5 |- ( ph -> ( Base ` F ) = ( Base ` (Scalar ` W ) ) )
86	84, 85	eqtrd 2237	. . . 4 |- ( ph -> B = ( Base ` (Scalar ` W ) ) )
87		islmodd.v	. . . . . 6 |- ( ph -> V = ( Base ` W ) )
88		islmodd.s	. . . . . . . . . . 11 |- ( ph -> .x. = ( .s ` W ) )
89	88	oveqd 5951	. . . . . . . . . 10 |- ( ph -> ( r .x. w ) = ( r ( .s ` W ) w ) )
90	89, 87	eleq12d 2275	. . . . . . . . 9 |- ( ph -> ( ( r .x. w ) e. V <-> ( r ( .s ` W ) w ) e. ( Base ` W ) ) )
91		eqidd 2205	. . . . . . . . . . 11 |- ( ph -> r = r )
92		islmodd.a	. . . . . . . . . . . 12 |- ( ph -> .+ = ( +g ` W ) )
93	92	oveqd 5951	. . . . . . . . . . 11 |- ( ph -> ( w .+ u ) = ( w ( +g ` W ) u ) )
94	88, 91, 93	oveq123d 5955	. . . . . . . . . 10 |- ( ph -> ( r .x. ( w .+ u ) ) = ( r ( .s ` W ) ( w ( +g ` W ) u ) ) )
95	88	oveqd 5951	. . . . . . . . . . 11 |- ( ph -> ( r .x. u ) = ( r ( .s ` W ) u ) )
96	92, 89, 95	oveq123d 5955	. . . . . . . . . 10 |- ( ph -> ( ( r .x. w ) .+ ( r .x. u ) ) = ( ( r ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) u ) ) )
97	94, 96	eqeq12d 2219	. . . . . . . . 9 |- ( ph -> ( ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) <-> ( r ( .s ` W ) ( w ( +g ` W ) u ) ) = ( ( r ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) u ) ) ) )
98		islmodd.p	. . . . . . . . . . . . 13 |- ( ph -> .+^ = ( +g ` F ) )
99	2	fveq2d 5574	. . . . . . . . . . . . 13 |- ( ph -> ( +g ` F ) = ( +g ` (Scalar ` W ) ) )
100	98, 99	eqtrd 2237	. . . . . . . . . . . 12 |- ( ph -> .+^ = ( +g ` (Scalar ` W ) ) )
101	100	oveqd 5951	. . . . . . . . . . 11 |- ( ph -> ( x .+^ r ) = ( x ( +g ` (Scalar ` W ) ) r ) )
102		eqidd 2205	. . . . . . . . . . 11 |- ( ph -> w = w )
103	88, 101, 102	oveq123d 5955	. . . . . . . . . 10 |- ( ph -> ( ( x .+^ r ) .x. w ) = ( ( x ( +g ` (Scalar ` W ) ) r ) ( .s ` W ) w ) )
104	88	oveqd 5951	. . . . . . . . . . 11 |- ( ph -> ( x .x. w ) = ( x ( .s ` W ) w ) )
105	92, 104, 89	oveq123d 5955	. . . . . . . . . 10 |- ( ph -> ( ( x .x. w ) .+ ( r .x. w ) ) = ( ( x ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) w ) ) )
106	103, 105	eqeq12d 2219	. . . . . . . . 9 |- ( ph -> ( ( ( x .+^ r ) .x. w ) = ( ( x .x. w ) .+ ( r .x. w ) ) <-> ( ( x ( +g ` (Scalar ` W ) ) r ) ( .s ` W ) w ) = ( ( x ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) w ) ) ) )
107	90, 97, 106	3anbi123d 1324	. . . . . . . 8 |- ( ph -> ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) /\ ( ( x .+^ r ) .x. w ) = ( ( x .x. w ) .+ ( r .x. w ) ) ) <-> ( ( r ( .s ` W ) w ) e. ( Base ` W ) /\ ( r ( .s ` W ) ( w ( +g ` W ) u ) ) = ( ( r ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) u ) ) /\ ( ( x ( +g ` (Scalar ` W ) ) r ) ( .s ` W ) w ) = ( ( x ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) w ) ) ) ) )
108		islmodd.t	. . . . . . . . . . . . 13 |- ( ph -> .X. = ( .r ` F ) )
109	2	fveq2d 5574	. . . . . . . . . . . . 13 |- ( ph -> ( .r ` F ) = ( .r ` (Scalar ` W ) ) )
110	108, 109	eqtrd 2237	. . . . . . . . . . . 12 |- ( ph -> .X. = ( .r ` (Scalar ` W ) ) )
111	110	oveqd 5951	. . . . . . . . . . 11 |- ( ph -> ( x .X. r ) = ( x ( .r ` (Scalar ` W ) ) r ) )
112	88, 111, 102	oveq123d 5955	. . . . . . . . . 10 |- ( ph -> ( ( x .X. r ) .x. w ) = ( ( x ( .r ` (Scalar ` W ) ) r ) ( .s ` W ) w ) )
113		eqidd 2205	. . . . . . . . . . 11 |- ( ph -> x = x )
114	88, 113, 89	oveq123d 5955	. . . . . . . . . 10 |- ( ph -> ( x .x. ( r .x. w ) ) = ( x ( .s ` W ) ( r ( .s ` W ) w ) ) )
115	112, 114	eqeq12d 2219	. . . . . . . . 9 |- ( ph -> ( ( ( x .X. r ) .x. w ) = ( x .x. ( r .x. w ) ) <-> ( ( x ( .r ` (Scalar ` W ) ) r ) ( .s ` W ) w ) = ( x ( .s ` W ) ( r ( .s ` W ) w ) ) ) )
116		islmodd.u	. . . . . . . . . . . 12 |- ( ph -> .1. = ( 1r ` F ) )
117	2	fveq2d 5574	. . . . . . . . . . . 12 |- ( ph -> ( 1r ` F ) = ( 1r ` (Scalar ` W ) ) )
118	116, 117	eqtrd 2237	. . . . . . . . . . 11 |- ( ph -> .1. = ( 1r ` (Scalar ` W ) ) )
119	88, 118, 102	oveq123d 5955	. . . . . . . . . 10 |- ( ph -> ( .1. .x. w ) = ( ( 1r ` (Scalar ` W ) ) ( .s ` W ) w ) )
120	119	eqeq1d 2213	. . . . . . . . 9 |- ( ph -> ( ( .1. .x. w ) = w <-> ( ( 1r ` (Scalar ` W ) ) ( .s ` W ) w ) = w ) )
121	115, 120	anbi12d 473	. . . . . . . 8 |- ( ph -> ( ( ( ( x .X. r ) .x. w ) = ( x .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w ) <-> ( ( ( x ( .r ` (Scalar ` W ) ) r ) ( .s ` W ) w ) = ( x ( .s ` W ) ( r ( .s ` W ) w ) ) /\ ( ( 1r ` (Scalar ` W ) ) ( .s ` W ) w ) = w ) ) )
122	107, 121	anbi12d 473	. . . . . . 7 |- ( ph -> ( ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) /\ ( ( x .+^ r ) .x. w ) = ( ( x .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( x .X. r ) .x. w ) = ( x .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w ) ) <-> ( ( ( r ( .s ` W ) w ) e. ( Base ` W ) /\ ( r ( .s ` W ) ( w ( +g ` W ) u ) ) = ( ( r ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) u ) ) /\ ( ( x ( +g ` (Scalar ` W ) ) r ) ( .s ` W ) w ) = ( ( x ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) w ) ) ) /\ ( ( ( x ( .r ` (Scalar ` W ) ) r ) ( .s ` W ) w ) = ( x ( .s ` W ) ( r ( .s ` W ) w ) ) /\ ( ( 1r ` (Scalar ` W ) ) ( .s ` W ) w ) = w ) ) ) )
123	87, 122	raleqbidv 2717	. . . . . 6 |- ( ph -> ( A. w e. V ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) /\ ( ( x .+^ r ) .x. w ) = ( ( x .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( x .X. r ) .x. w ) = ( x .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w ) ) <-> A. w e. ( Base ` W ) ( ( ( r ( .s ` W ) w ) e. ( Base ` W ) /\ ( r ( .s ` W ) ( w ( +g ` W ) u ) ) = ( ( r ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) u ) ) /\ ( ( x ( +g ` (Scalar ` W ) ) r ) ( .s ` W ) w ) = ( ( x ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) w ) ) ) /\ ( ( ( x ( .r ` (Scalar ` W ) ) r ) ( .s ` W ) w ) = ( x ( .s ` W ) ( r ( .s ` W ) w ) ) /\ ( ( 1r ` (Scalar ` W ) ) ( .s ` W ) w ) = w ) ) ) )
124	87, 123	raleqbidv 2717	. . . . 5 |- ( ph -> ( A. u e. V A. w e. V ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) /\ ( ( x .+^ r ) .x. w ) = ( ( x .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( x .X. r ) .x. w ) = ( x .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w ) ) <-> A. u e. ( Base ` W ) A. w e. ( Base ` W ) ( ( ( r ( .s ` W ) w ) e. ( Base ` W ) /\ ( r ( .s ` W ) ( w ( +g ` W ) u ) ) = ( ( r ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) u ) ) /\ ( ( x ( +g ` (Scalar ` W ) ) r ) ( .s ` W ) w ) = ( ( x ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) w ) ) ) /\ ( ( ( x ( .r ` (Scalar ` W ) ) r ) ( .s ` W ) w ) = ( x ( .s ` W ) ( r ( .s ` W ) w ) ) /\ ( ( 1r ` (Scalar ` W ) ) ( .s ` W ) w ) = w ) ) ) )
125	86, 124	raleqbidv 2717	. . . 4 |- ( ph -> ( A. r e. B A. u e. V A. w e. V ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) /\ ( ( x .+^ r ) .x. w ) = ( ( x .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( x .X. r ) .x. w ) = ( x .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w ) ) <-> A. r e. ( Base ` (Scalar ` W ) ) A. u e. ( Base ` W ) A. w e. ( Base ` W ) ( ( ( r ( .s ` W ) w ) e. ( Base ` W ) /\ ( r ( .s ` W ) ( w ( +g ` W ) u ) ) = ( ( r ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) u ) ) /\ ( ( x ( +g ` (Scalar ` W ) ) r ) ( .s ` W ) w ) = ( ( x ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) w ) ) ) /\ ( ( ( x ( .r ` (Scalar ` W ) ) r ) ( .s ` W ) w ) = ( x ( .s ` W ) ( r ( .s ` W ) w ) ) /\ ( ( 1r ` (Scalar ` W ) ) ( .s ` W ) w ) = w ) ) ) )
126	86, 125	raleqbidv 2717	. . 3 |- ( ph -> ( A. x e. B A. r e. B A. u e. V A. w e. V ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ u ) ) = ( ( r .x. w ) .+ ( r .x. u ) ) /\ ( ( x .+^ r ) .x. w ) = ( ( x .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( x .X. r ) .x. w ) = ( x .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w ) ) <-> A. x e. ( Base ` (Scalar ` W ) ) A. r e. ( Base ` (Scalar ` W ) ) A. u e. ( Base ` W ) A. w e. ( Base ` W ) ( ( ( r ( .s ` W ) w ) e. ( Base ` W ) /\ ( r ( .s ` W ) ( w ( +g ` W ) u ) ) = ( ( r ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) u ) ) /\ ( ( x ( +g ` (Scalar ` W ) ) r ) ( .s ` W ) w ) = ( ( x ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) w ) ) ) /\ ( ( ( x ( .r ` (Scalar ` W ) ) r ) ( .s ` W ) w ) = ( x ( .s ` W ) ( r ( .s ` W ) w ) ) /\ ( ( 1r ` (Scalar ` W ) ) ( .s ` W ) w ) = w ) ) ) )
127	83, 126	mpbid 147	. 2 |- ( ph -> A. x e. ( Base ` (Scalar ` W ) ) A. r e. ( Base ` (Scalar ` W ) ) A. u e. ( Base ` W ) A. w e. ( Base ` W ) ( ( ( r ( .s ` W ) w ) e. ( Base ` W ) /\ ( r ( .s ` W ) ( w ( +g ` W ) u ) ) = ( ( r ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) u ) ) /\ ( ( x ( +g ` (Scalar ` W ) ) r ) ( .s ` W ) w ) = ( ( x ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) w ) ) ) /\ ( ( ( x ( .r ` (Scalar ` W ) ) r ) ( .s ` W ) w ) = ( x ( .s ` W ) ( r ( .s ` W ) w ) ) /\ ( ( 1r ` (Scalar ` W ) ) ( .s ` W ) w ) = w ) ) )
128		eqid 2204	. . 3 |- ( Base ` W ) = ( Base ` W )
129		eqid 2204	. . 3 |- ( +g ` W ) = ( +g ` W )
130		eqid 2204	. . 3 |- ( .s ` W ) = ( .s ` W )
131		eqid 2204	. . 3 |- (Scalar ` W ) = (Scalar ` W )
132		eqid 2204	. . 3 |- ( Base ` (Scalar ` W ) ) = ( Base ` (Scalar ` W ) )
133		eqid 2204	. . 3 |- ( +g ` (Scalar ` W ) ) = ( +g ` (Scalar ` W ) )
134		eqid 2204	. . 3 |- ( .r ` (Scalar ` W ) ) = ( .r ` (Scalar ` W ) )
135		eqid 2204	. . 3 |- ( 1r ` (Scalar ` W ) ) = ( 1r ` (Scalar ` W ) )
136	128, 129, 130, 131, 132, 133, 134, 135	islmod 13971	. 2 |- ( W e. LMod <-> ( W e. Grp /\ (Scalar ` W ) e. Ring /\ A. x e. ( Base ` (Scalar ` W ) ) A. r e. ( Base ` (Scalar ` W ) ) A. u e. ( Base ` W ) A. w e. ( Base ` W ) ( ( ( r ( .s ` W ) w ) e. ( Base ` W ) /\ ( r ( .s ` W ) ( w ( +g ` W ) u ) ) = ( ( r ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) u ) ) /\ ( ( x ( +g ` (Scalar ` W ) ) r ) ( .s ` W ) w ) = ( ( x ( .s ` W ) w ) ( +g ` W ) ( r ( .s ` W ) w ) ) ) /\ ( ( ( x ( .r ` (Scalar ` W ) ) r ) ( .s ` W ) w ) = ( x ( .s ` W ) ( r ( .s ` W ) w ) ) /\ ( ( 1r ` (Scalar ` W ) ) ( .s ` W ) w ) = w ) ) ) )
137	1, 4, 127, 136	syl3anbrc 1183	1 |- ( ph -> W e. LMod )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 980   = wceq 1372   e. wcel 2175   A.wral 2483   ` cfv 5268  (class class class)co 5934   Basecbs 12751   +g cplusg 12828   .rcmulr 12829  Scalarcsca 12831   .scvsca 12832   Grpcgrp 13250   1rcur 13639   Ringcrg 13676   LModclmod 13967

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-13 2177  ax-14 2178  ax-ext 2186  ax-sep 4161  ax-pow 4217  ax-pr 4252  ax-un 4478  ax-cnex 7998  ax-resscn 7999  ax-1re 8001  ax-addrcl 8004

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-eu 2056  df-mo 2057  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ral 2488  df-rex 2489  df-rab 2492  df-v 2773  df-sbc 2998  df-un 3169  df-in 3171  df-ss 3178  df-pw 3617  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-int 3885  df-br 4044  df-opab 4105  df-mpt 4106  df-id 4338  df-xp 4679  df-rel 4680  df-cnv 4681  df-co 4682  df-dm 4683  df-rn 4684  df-res 4685  df-iota 5229  df-fun 5270  df-fn 5271  df-fv 5276  df-ov 5937  df-inn 9019  df-2 9077  df-3 9078  df-4 9079  df-5 9080  df-6 9081  df-ndx 12754  df-slot 12755  df-base 12757  df-plusg 12841  df-mulr 12842  df-sca 12844  df-vsca 12845  df-lmod 13969

This theorem is referenced by:  rmodislmod  14031  islss3  14059  sralmod  14130