Metamath Proof Explorer

Theorem slmdlema

Description: Lemma for properties of a semimodule. (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014) (Revised by Thierry Arnoux, 1-Apr-2018)

Ref Expression
Hypotheses isslmd.v 
|- V = ( Base ` W )
isslmd.a 
|- .+ = ( +g ` W )
isslmd.s 
|- .x. = ( .s ` W )
isslmd.0 
|- .0. = ( 0g ` W )
isslmd.f 
|- F = ( Scalar ` W )
isslmd.k 
|- K = ( Base ` F )
isslmd.p 
|- .+^ = ( +g ` F )
isslmd.t 
|- .X. = ( .r ` F )
isslmd.u 
|- .1. = ( 1r ` F )
isslmd.o 
|- O = ( 0g ` F )
Assertion slmdlema 
|- ( ( W e. SLMod /\ ( Q e. K /\ R e. K ) /\ ( X e. V /\ Y e. V ) ) -> ( ( ( R .x. Y ) e. V /\ ( R .x. ( Y .+ X ) ) = ( ( R .x. Y ) .+ ( R .x. X ) ) /\ ( ( Q .+^ R ) .x. Y ) = ( ( Q .x. Y ) .+ ( R .x. Y ) ) ) /\ ( ( ( Q .X. R ) .x. Y ) = ( Q .x. ( R .x. Y ) ) /\ ( .1. .x. Y ) = Y /\ ( O .x. Y ) = .0. ) ) )

Proof

Step Hyp Ref Expression
1 isslmd.v 
 |-  V = ( Base ` W )
2 isslmd.a 
 |-  .+ = ( +g ` W )
3 isslmd.s 
 |-  .x. = ( .s ` W )
4 isslmd.0 
 |-  .0. = ( 0g ` W )
5 isslmd.f 
 |-  F = ( Scalar ` W )
6 isslmd.k 
 |-  K = ( Base ` F )
7 isslmd.p 
 |-  .+^ = ( +g ` F )
8 isslmd.t 
 |-  .X. = ( .r ` F )
9 isslmd.u 
 |-  .1. = ( 1r ` F )
10 isslmd.o 
 |-  O = ( 0g ` F )
11 1 2 3 4 5 6 7 8 9 10 isslmd 
 |-  ( W e. SLMod <-> ( W e. CMnd /\ F e. SRing /\ A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ x ) ) = ( ( r .x. w ) .+ ( r .x. x ) ) /\ ( ( q .+^ r ) .x. w ) = ( ( q .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( q .X. r ) .x. w ) = ( q .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) ) ) )
12 11 simp3bi 
 |-  ( W e. SLMod -> A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ x ) ) = ( ( r .x. w ) .+ ( r .x. x ) ) /\ ( ( q .+^ r ) .x. w ) = ( ( q .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( q .X. r ) .x. w ) = ( q .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) ) )
13 oveq1 
 |-  ( q = Q -> ( q .+^ r ) = ( Q .+^ r ) )
14 13 oveq1d 
 |-  ( q = Q -> ( ( q .+^ r ) .x. w ) = ( ( Q .+^ r ) .x. w ) )
15 oveq1 
 |-  ( q = Q -> ( q .x. w ) = ( Q .x. w ) )
16 15 oveq1d 
 |-  ( q = Q -> ( ( q .x. w ) .+ ( r .x. w ) ) = ( ( Q .x. w ) .+ ( r .x. w ) ) )
17 14 16 eqeq12d 
 |-  ( q = Q -> ( ( ( q .+^ r ) .x. w ) = ( ( q .x. w ) .+ ( r .x. w ) ) <-> ( ( Q .+^ r ) .x. w ) = ( ( Q .x. w ) .+ ( r .x. w ) ) ) )
18 17 3anbi3d 
 |-  ( q = Q -> ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ x ) ) = ( ( r .x. w ) .+ ( r .x. x ) ) /\ ( ( q .+^ r ) .x. w ) = ( ( q .x. w ) .+ ( r .x. w ) ) ) <-> ( ( r .x. w ) e. V /\ ( r .x. ( w .+ x ) ) = ( ( r .x. w ) .+ ( r .x. x ) ) /\ ( ( Q .+^ r ) .x. w ) = ( ( Q .x. w ) .+ ( r .x. w ) ) ) ) )
19 oveq1 
 |-  ( q = Q -> ( q .X. r ) = ( Q .X. r ) )
20 19 oveq1d 
 |-  ( q = Q -> ( ( q .X. r ) .x. w ) = ( ( Q .X. r ) .x. w ) )
21 oveq1 
 |-  ( q = Q -> ( q .x. ( r .x. w ) ) = ( Q .x. ( r .x. w ) ) )
22 20 21 eqeq12d 
 |-  ( q = Q -> ( ( ( q .X. r ) .x. w ) = ( q .x. ( r .x. w ) ) <-> ( ( Q .X. r ) .x. w ) = ( Q .x. ( r .x. w ) ) ) )
23 22 3anbi1d 
 |-  ( q = Q -> ( ( ( ( q .X. r ) .x. w ) = ( q .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) <-> ( ( ( Q .X. r ) .x. w ) = ( Q .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) ) )
24 18 23 anbi12d 
 |-  ( q = Q -> ( ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ x ) ) = ( ( r .x. w ) .+ ( r .x. x ) ) /\ ( ( q .+^ r ) .x. w ) = ( ( q .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( q .X. r ) .x. w ) = ( q .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) ) <-> ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ x ) ) = ( ( r .x. w ) .+ ( r .x. x ) ) /\ ( ( Q .+^ r ) .x. w ) = ( ( Q .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( Q .X. r ) .x. w ) = ( Q .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) ) ) )
25 24 2ralbidv 
 |-  ( q = Q -> ( A. x e. V A. w e. V ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ x ) ) = ( ( r .x. w ) .+ ( r .x. x ) ) /\ ( ( q .+^ r ) .x. w ) = ( ( q .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( q .X. r ) .x. w ) = ( q .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) ) <-> A. x e. V A. w e. V ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ x ) ) = ( ( r .x. w ) .+ ( r .x. x ) ) /\ ( ( Q .+^ r ) .x. w ) = ( ( Q .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( Q .X. r ) .x. w ) = ( Q .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) ) ) )
26 oveq1 
 |-  ( r = R -> ( r .x. w ) = ( R .x. w ) )
27 26 eleq1d 
 |-  ( r = R -> ( ( r .x. w ) e. V <-> ( R .x. w ) e. V ) )
28 oveq1 
 |-  ( r = R -> ( r .x. ( w .+ x ) ) = ( R .x. ( w .+ x ) ) )
29 oveq1 
 |-  ( r = R -> ( r .x. x ) = ( R .x. x ) )
30 26 29 oveq12d 
 |-  ( r = R -> ( ( r .x. w ) .+ ( r .x. x ) ) = ( ( R .x. w ) .+ ( R .x. x ) ) )
31 28 30 eqeq12d 
 |-  ( r = R -> ( ( r .x. ( w .+ x ) ) = ( ( r .x. w ) .+ ( r .x. x ) ) <-> ( R .x. ( w .+ x ) ) = ( ( R .x. w ) .+ ( R .x. x ) ) ) )
32 oveq2 
 |-  ( r = R -> ( Q .+^ r ) = ( Q .+^ R ) )
33 32 oveq1d 
 |-  ( r = R -> ( ( Q .+^ r ) .x. w ) = ( ( Q .+^ R ) .x. w ) )
34 26 oveq2d 
 |-  ( r = R -> ( ( Q .x. w ) .+ ( r .x. w ) ) = ( ( Q .x. w ) .+ ( R .x. w ) ) )
35 33 34 eqeq12d 
 |-  ( r = R -> ( ( ( Q .+^ r ) .x. w ) = ( ( Q .x. w ) .+ ( r .x. w ) ) <-> ( ( Q .+^ R ) .x. w ) = ( ( Q .x. w ) .+ ( R .x. w ) ) ) )
36 27 31 35 3anbi123d 
 |-  ( r = R -> ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ x ) ) = ( ( r .x. w ) .+ ( r .x. x ) ) /\ ( ( Q .+^ r ) .x. w ) = ( ( Q .x. w ) .+ ( r .x. w ) ) ) <-> ( ( R .x. w ) e. V /\ ( R .x. ( w .+ x ) ) = ( ( R .x. w ) .+ ( R .x. x ) ) /\ ( ( Q .+^ R ) .x. w ) = ( ( Q .x. w ) .+ ( R .x. w ) ) ) ) )
37 oveq2 
 |-  ( r = R -> ( Q .X. r ) = ( Q .X. R ) )
38 37 oveq1d 
 |-  ( r = R -> ( ( Q .X. r ) .x. w ) = ( ( Q .X. R ) .x. w ) )
39 26 oveq2d 
 |-  ( r = R -> ( Q .x. ( r .x. w ) ) = ( Q .x. ( R .x. w ) ) )
40 38 39 eqeq12d 
 |-  ( r = R -> ( ( ( Q .X. r ) .x. w ) = ( Q .x. ( r .x. w ) ) <-> ( ( Q .X. R ) .x. w ) = ( Q .x. ( R .x. w ) ) ) )
41 40 3anbi1d 
 |-  ( r = R -> ( ( ( ( Q .X. r ) .x. w ) = ( Q .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) <-> ( ( ( Q .X. R ) .x. w ) = ( Q .x. ( R .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) ) )
42 36 41 anbi12d 
 |-  ( r = R -> ( ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ x ) ) = ( ( r .x. w ) .+ ( r .x. x ) ) /\ ( ( Q .+^ r ) .x. w ) = ( ( Q .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( Q .X. r ) .x. w ) = ( Q .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) ) <-> ( ( ( R .x. w ) e. V /\ ( R .x. ( w .+ x ) ) = ( ( R .x. w ) .+ ( R .x. x ) ) /\ ( ( Q .+^ R ) .x. w ) = ( ( Q .x. w ) .+ ( R .x. w ) ) ) /\ ( ( ( Q .X. R ) .x. w ) = ( Q .x. ( R .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) ) ) )
43 42 2ralbidv 
 |-  ( r = R -> ( A. x e. V A. w e. V ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ x ) ) = ( ( r .x. w ) .+ ( r .x. x ) ) /\ ( ( Q .+^ r ) .x. w ) = ( ( Q .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( Q .X. r ) .x. w ) = ( Q .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) ) <-> A. x e. V A. w e. V ( ( ( R .x. w ) e. V /\ ( R .x. ( w .+ x ) ) = ( ( R .x. w ) .+ ( R .x. x ) ) /\ ( ( Q .+^ R ) .x. w ) = ( ( Q .x. w ) .+ ( R .x. w ) ) ) /\ ( ( ( Q .X. R ) .x. w ) = ( Q .x. ( R .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) ) ) )
44 25 43 rspc2v 
 |-  ( ( Q e. K /\ R e. K ) -> ( A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ x ) ) = ( ( r .x. w ) .+ ( r .x. x ) ) /\ ( ( q .+^ r ) .x. w ) = ( ( q .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( q .X. r ) .x. w ) = ( q .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) ) -> A. x e. V A. w e. V ( ( ( R .x. w ) e. V /\ ( R .x. ( w .+ x ) ) = ( ( R .x. w ) .+ ( R .x. x ) ) /\ ( ( Q .+^ R ) .x. w ) = ( ( Q .x. w ) .+ ( R .x. w ) ) ) /\ ( ( ( Q .X. R ) .x. w ) = ( Q .x. ( R .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) ) ) )
45 12 44 mpan9 
 |-  ( ( W e. SLMod /\ ( Q e. K /\ R e. K ) ) -> A. x e. V A. w e. V ( ( ( R .x. w ) e. V /\ ( R .x. ( w .+ x ) ) = ( ( R .x. w ) .+ ( R .x. x ) ) /\ ( ( Q .+^ R ) .x. w ) = ( ( Q .x. w ) .+ ( R .x. w ) ) ) /\ ( ( ( Q .X. R ) .x. w ) = ( Q .x. ( R .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) ) )
46 oveq2 
 |-  ( x = X -> ( w .+ x ) = ( w .+ X ) )
47 46 oveq2d 
 |-  ( x = X -> ( R .x. ( w .+ x ) ) = ( R .x. ( w .+ X ) ) )
48 oveq2 
 |-  ( x = X -> ( R .x. x ) = ( R .x. X ) )
49 48 oveq2d 
 |-  ( x = X -> ( ( R .x. w ) .+ ( R .x. x ) ) = ( ( R .x. w ) .+ ( R .x. X ) ) )
50 47 49 eqeq12d 
 |-  ( x = X -> ( ( R .x. ( w .+ x ) ) = ( ( R .x. w ) .+ ( R .x. x ) ) <-> ( R .x. ( w .+ X ) ) = ( ( R .x. w ) .+ ( R .x. X ) ) ) )
51 50 3anbi2d 
 |-  ( x = X -> ( ( ( R .x. w ) e. V /\ ( R .x. ( w .+ x ) ) = ( ( R .x. w ) .+ ( R .x. x ) ) /\ ( ( Q .+^ R ) .x. w ) = ( ( Q .x. w ) .+ ( R .x. w ) ) ) <-> ( ( R .x. w ) e. V /\ ( R .x. ( w .+ X ) ) = ( ( R .x. w ) .+ ( R .x. X ) ) /\ ( ( Q .+^ R ) .x. w ) = ( ( Q .x. w ) .+ ( R .x. w ) ) ) ) )
52 51 anbi1d 
 |-  ( x = X -> ( ( ( ( R .x. w ) e. V /\ ( R .x. ( w .+ x ) ) = ( ( R .x. w ) .+ ( R .x. x ) ) /\ ( ( Q .+^ R ) .x. w ) = ( ( Q .x. w ) .+ ( R .x. w ) ) ) /\ ( ( ( Q .X. R ) .x. w ) = ( Q .x. ( R .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) ) <-> ( ( ( R .x. w ) e. V /\ ( R .x. ( w .+ X ) ) = ( ( R .x. w ) .+ ( R .x. X ) ) /\ ( ( Q .+^ R ) .x. w ) = ( ( Q .x. w ) .+ ( R .x. w ) ) ) /\ ( ( ( Q .X. R ) .x. w ) = ( Q .x. ( R .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) ) ) )
53 oveq2 
 |-  ( w = Y -> ( R .x. w ) = ( R .x. Y ) )
54 53 eleq1d 
 |-  ( w = Y -> ( ( R .x. w ) e. V <-> ( R .x. Y ) e. V ) )
55 oveq1 
 |-  ( w = Y -> ( w .+ X ) = ( Y .+ X ) )
56 55 oveq2d 
 |-  ( w = Y -> ( R .x. ( w .+ X ) ) = ( R .x. ( Y .+ X ) ) )
57 53 oveq1d 
 |-  ( w = Y -> ( ( R .x. w ) .+ ( R .x. X ) ) = ( ( R .x. Y ) .+ ( R .x. X ) ) )
58 56 57 eqeq12d 
 |-  ( w = Y -> ( ( R .x. ( w .+ X ) ) = ( ( R .x. w ) .+ ( R .x. X ) ) <-> ( R .x. ( Y .+ X ) ) = ( ( R .x. Y ) .+ ( R .x. X ) ) ) )
59 oveq2 
 |-  ( w = Y -> ( ( Q .+^ R ) .x. w ) = ( ( Q .+^ R ) .x. Y ) )
60 oveq2 
 |-  ( w = Y -> ( Q .x. w ) = ( Q .x. Y ) )
61 60 53 oveq12d 
 |-  ( w = Y -> ( ( Q .x. w ) .+ ( R .x. w ) ) = ( ( Q .x. Y ) .+ ( R .x. Y ) ) )
62 59 61 eqeq12d 
 |-  ( w = Y -> ( ( ( Q .+^ R ) .x. w ) = ( ( Q .x. w ) .+ ( R .x. w ) ) <-> ( ( Q .+^ R ) .x. Y ) = ( ( Q .x. Y ) .+ ( R .x. Y ) ) ) )
63 54 58 62 3anbi123d 
 |-  ( w = Y -> ( ( ( R .x. w ) e. V /\ ( R .x. ( w .+ X ) ) = ( ( R .x. w ) .+ ( R .x. X ) ) /\ ( ( Q .+^ R ) .x. w ) = ( ( Q .x. w ) .+ ( R .x. w ) ) ) <-> ( ( R .x. Y ) e. V /\ ( R .x. ( Y .+ X ) ) = ( ( R .x. Y ) .+ ( R .x. X ) ) /\ ( ( Q .+^ R ) .x. Y ) = ( ( Q .x. Y ) .+ ( R .x. Y ) ) ) ) )
64 oveq2 
 |-  ( w = Y -> ( ( Q .X. R ) .x. w ) = ( ( Q .X. R ) .x. Y ) )
65 53 oveq2d 
 |-  ( w = Y -> ( Q .x. ( R .x. w ) ) = ( Q .x. ( R .x. Y ) ) )
66 64 65 eqeq12d 
 |-  ( w = Y -> ( ( ( Q .X. R ) .x. w ) = ( Q .x. ( R .x. w ) ) <-> ( ( Q .X. R ) .x. Y ) = ( Q .x. ( R .x. Y ) ) ) )
67 oveq2 
 |-  ( w = Y -> ( .1. .x. w ) = ( .1. .x. Y ) )
68 id 
 |-  ( w = Y -> w = Y )
69 67 68 eqeq12d 
 |-  ( w = Y -> ( ( .1. .x. w ) = w <-> ( .1. .x. Y ) = Y ) )
70 oveq2 
 |-  ( w = Y -> ( O .x. w ) = ( O .x. Y ) )
71 70 eqeq1d 
 |-  ( w = Y -> ( ( O .x. w ) = .0. <-> ( O .x. Y ) = .0. ) )
72 66 69 71 3anbi123d 
 |-  ( w = Y -> ( ( ( ( Q .X. R ) .x. w ) = ( Q .x. ( R .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) <-> ( ( ( Q .X. R ) .x. Y ) = ( Q .x. ( R .x. Y ) ) /\ ( .1. .x. Y ) = Y /\ ( O .x. Y ) = .0. ) ) )
73 63 72 anbi12d 
 |-  ( w = Y -> ( ( ( ( R .x. w ) e. V /\ ( R .x. ( w .+ X ) ) = ( ( R .x. w ) .+ ( R .x. X ) ) /\ ( ( Q .+^ R ) .x. w ) = ( ( Q .x. w ) .+ ( R .x. w ) ) ) /\ ( ( ( Q .X. R ) .x. w ) = ( Q .x. ( R .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) ) <-> ( ( ( R .x. Y ) e. V /\ ( R .x. ( Y .+ X ) ) = ( ( R .x. Y ) .+ ( R .x. X ) ) /\ ( ( Q .+^ R ) .x. Y ) = ( ( Q .x. Y ) .+ ( R .x. Y ) ) ) /\ ( ( ( Q .X. R ) .x. Y ) = ( Q .x. ( R .x. Y ) ) /\ ( .1. .x. Y ) = Y /\ ( O .x. Y ) = .0. ) ) ) )
74 52 73 rspc2v 
 |-  ( ( X e. V /\ Y e. V ) -> ( A. x e. V A. w e. V ( ( ( R .x. w ) e. V /\ ( R .x. ( w .+ x ) ) = ( ( R .x. w ) .+ ( R .x. x ) ) /\ ( ( Q .+^ R ) .x. w ) = ( ( Q .x. w ) .+ ( R .x. w ) ) ) /\ ( ( ( Q .X. R ) .x. w ) = ( Q .x. ( R .x. w ) ) /\ ( .1. .x. w ) = w /\ ( O .x. w ) = .0. ) ) -> ( ( ( R .x. Y ) e. V /\ ( R .x. ( Y .+ X ) ) = ( ( R .x. Y ) .+ ( R .x. X ) ) /\ ( ( Q .+^ R ) .x. Y ) = ( ( Q .x. Y ) .+ ( R .x. Y ) ) ) /\ ( ( ( Q .X. R ) .x. Y ) = ( Q .x. ( R .x. Y ) ) /\ ( .1. .x. Y ) = Y /\ ( O .x. Y ) = .0. ) ) ) )
75 45 74 syl5com 
 |-  ( ( W e. SLMod /\ ( Q e. K /\ R e. K ) ) -> ( ( X e. V /\ Y e. V ) -> ( ( ( R .x. Y ) e. V /\ ( R .x. ( Y .+ X ) ) = ( ( R .x. Y ) .+ ( R .x. X ) ) /\ ( ( Q .+^ R ) .x. Y ) = ( ( Q .x. Y ) .+ ( R .x. Y ) ) ) /\ ( ( ( Q .X. R ) .x. Y ) = ( Q .x. ( R .x. Y ) ) /\ ( .1. .x. Y ) = Y /\ ( O .x. Y ) = .0. ) ) ) )
76 75 3impia 
 |-  ( ( W e. SLMod /\ ( Q e. K /\ R e. K ) /\ ( X e. V /\ Y e. V ) ) -> ( ( ( R .x. Y ) e. V /\ ( R .x. ( Y .+ X ) ) = ( ( R .x. Y ) .+ ( R .x. X ) ) /\ ( ( Q .+^ R ) .x. Y ) = ( ( Q .x. Y ) .+ ( R .x. Y ) ) ) /\ ( ( ( Q .X. R ) .x. Y ) = ( Q .x. ( R .x. Y ) ) /\ ( .1. .x. Y ) = Y /\ ( O .x. Y ) = .0. ) ) )