Metamath Proof Explorer


Theorem rlocaddval

Description: Value of the addition in the ring localization, given two representatives. (Contributed by Thierry Arnoux, 4-May-2025)

Ref Expression
Hypotheses rlocaddval.1 B = Base R
rlocaddval.2 · ˙ = R
rlocaddval.3 + ˙ = + R
rlocaddval.4 No typesetting found for |- L = ( R RLocal S ) with typecode |-
rlocaddval.5 No typesetting found for |- .~ = ( R ~RL S ) with typecode |-
rlocaddval.r φ R CRing
rlocaddval.s φ S SubMnd mulGrp R
rlocaddval.6 φ E B
rlocaddval.7 φ F B
rlocaddval.8 φ G S
rlocaddval.9 φ H S
rlocaddval.10 ˙ = + L
Assertion rlocaddval φ E G ˙ ˙ F H ˙ = E · ˙ H + ˙ F · ˙ G G · ˙ H ˙

Proof

Step Hyp Ref Expression
1 rlocaddval.1 B = Base R
2 rlocaddval.2 · ˙ = R
3 rlocaddval.3 + ˙ = + R
4 rlocaddval.4 Could not format L = ( R RLocal S ) : No typesetting found for |- L = ( R RLocal S ) with typecode |-
5 rlocaddval.5 Could not format .~ = ( R ~RL S ) : No typesetting found for |- .~ = ( R ~RL S ) with typecode |-
6 rlocaddval.r φ R CRing
7 rlocaddval.s φ S SubMnd mulGrp R
8 rlocaddval.6 φ E B
9 rlocaddval.7 φ F B
10 rlocaddval.8 φ G S
11 rlocaddval.9 φ H S
12 rlocaddval.10 ˙ = + L
13 8 10 opelxpd φ E G B × S
14 9 11 opelxpd φ F H B × S
15 eqid 0 R = 0 R
16 eqid - R = - R
17 eqid R = R
18 eqid Scalar R = Scalar R
19 eqid Base Scalar R = Base Scalar R
20 eqid R = R
21 eqid B × S = B × S
22 eqid TopSet R = TopSet R
23 eqid dist R = dist R
24 eqid a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b = a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b
25 eqid a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b = a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b
26 eqid k Base Scalar R , a B × S k R 1 st a 2 nd a = k Base Scalar R , a B × S k R 1 st a 2 nd a
27 eqid a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a = a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a
28 eqid a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a = a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a
29 eqid mulGrp R = mulGrp R
30 29 1 mgpbas B = Base mulGrp R
31 30 submss S SubMnd mulGrp R S B
32 7 31 syl φ S B
33 1 15 2 16 3 17 18 19 20 21 5 22 23 24 25 26 27 28 6 32 rlocval Could not format ( ph -> ( R RLocal S ) = ( ( ( { <. ( Base ` ndx ) , ( B X. S ) >. , <. ( +g ` ndx ) , ( a e. ( B X. S ) , b e. ( B X. S ) |-> <. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .+ ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. ( B X. S ) , b e. ( B X. S ) |-> <. ( ( 1st ` a ) .x. ( 1st ` b ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` R ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` R ) ) , a e. ( B X. S ) |-> <. ( k ( .s ` R ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` R ) tX ( ( TopSet ` R ) |`t S ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. ( B X. S ) /\ b e. ( B X. S ) ) /\ ( ( 1st ` a ) .x. ( 2nd ` b ) ) ( le ` R ) ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. ( B X. S ) , b e. ( B X. S ) |-> ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) ( dist ` R ) ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) >. } ) /s .~ ) ) : No typesetting found for |- ( ph -> ( R RLocal S ) = ( ( ( { <. ( Base ` ndx ) , ( B X. S ) >. , <. ( +g ` ndx ) , ( a e. ( B X. S ) , b e. ( B X. S ) |-> <. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .+ ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. ( B X. S ) , b e. ( B X. S ) |-> <. ( ( 1st ` a ) .x. ( 1st ` b ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` R ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` R ) ) , a e. ( B X. S ) |-> <. ( k ( .s ` R ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` R ) tX ( ( TopSet ` R ) |`t S ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. ( B X. S ) /\ b e. ( B X. S ) ) /\ ( ( 1st ` a ) .x. ( 2nd ` b ) ) ( le ` R ) ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. ( B X. S ) , b e. ( B X. S ) |-> ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) ( dist ` R ) ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) >. } ) /s .~ ) ) with typecode |-
34 4 33 eqtrid φ L = Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a / 𝑠 ˙
35 eqidd φ Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a = Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a
36 eqid Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a = Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a
37 36 imasvalstr Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a Struct 1 12
38 baseid Base = Slot Base ndx
39 snsstp1 Base ndx B × S Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b
40 ssun1 Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx
41 ssun1 Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a
42 40 41 sstri Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a
43 39 42 sstri Base ndx B × S Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a
44 1 fvexi B V
45 44 a1i φ B V
46 45 7 xpexd φ B × S V
47 eqid Base Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a = Base Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a
48 35 37 38 43 46 47 strfv3 φ Base Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a = B × S
49 48 eqcomd φ B × S = Base Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a
50 eqid 1 R = 1 R
51 1 15 50 2 16 21 5 6 7 erler φ ˙ Er B × S
52 tpex Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b V
53 tpex Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx V
54 52 53 unex Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx V
55 tpex TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a V
56 54 55 unex Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a V
57 56 a1i φ Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a V
58 32 ad2antrr φ u ˙ p v ˙ q S B
59 58 ad2antrr φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R S B
60 59 ad2antrr φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R S B
61 eqidd φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 1 st u · ˙ 2 nd v + ˙ 1 st v · ˙ 2 nd u 2 nd u · ˙ 2 nd v = 1 st u · ˙ 2 nd v + ˙ 1 st v · ˙ 2 nd u 2 nd u · ˙ 2 nd v
62 eqidd φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 1 st p · ˙ 2 nd q + ˙ 1 st q · ˙ 2 nd p 2 nd p · ˙ 2 nd q = 1 st p · ˙ 2 nd q + ˙ 1 st q · ˙ 2 nd p 2 nd p · ˙ 2 nd q
63 6 crnggrpd φ R Grp
64 63 ad6antr φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R R Grp
65 6 crngringd φ R Ring
66 65 ad6antr φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R R Ring
67 simplr φ u ˙ p v ˙ q u ˙ p
68 1 5 58 67 erlcl1 φ u ˙ p v ˙ q u B × S
69 68 ad4antr φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R u B × S
70 xp1st u B × S 1 st u B
71 69 70 syl φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 1 st u B
72 simpr φ u ˙ p v ˙ q v ˙ q
73 1 5 58 72 erlcl1 φ u ˙ p v ˙ q v B × S
74 73 ad4antr φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R v B × S
75 xp2nd v B × S 2 nd v S
76 74 75 syl φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 2 nd v S
77 60 76 sseldd φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 2 nd v B
78 1 2 66 71 77 ringcld φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 1 st u · ˙ 2 nd v B
79 xp1st v B × S 1 st v B
80 74 79 syl φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 1 st v B
81 xp2nd u B × S 2 nd u S
82 69 81 syl φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 2 nd u S
83 60 82 sseldd φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 2 nd u B
84 1 2 66 80 83 ringcld φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 1 st v · ˙ 2 nd u B
85 1 3 64 78 84 grpcld φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 1 st u · ˙ 2 nd v + ˙ 1 st v · ˙ 2 nd u B
86 1 5 58 67 erlcl2 φ u ˙ p v ˙ q p B × S
87 86 ad4antr φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R p B × S
88 xp1st p B × S 1 st p B
89 87 88 syl φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 1 st p B
90 1 5 58 72 erlcl2 φ u ˙ p v ˙ q q B × S
91 90 ad4antr φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R q B × S
92 xp2nd q B × S 2 nd q S
93 91 92 syl φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 2 nd q S
94 60 93 sseldd φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 2 nd q B
95 1 2 66 89 94 ringcld φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 1 st p · ˙ 2 nd q B
96 xp1st q B × S 1 st q B
97 91 96 syl φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 1 st q B
98 xp2nd p B × S 2 nd p S
99 87 98 syl φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 2 nd p S
100 60 99 sseldd φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 2 nd p B
101 1 2 66 97 100 ringcld φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 1 st q · ˙ 2 nd p B
102 1 3 64 95 101 grpcld φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 1 st p · ˙ 2 nd q + ˙ 1 st q · ˙ 2 nd p B
103 7 ad6antr φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R S SubMnd mulGrp R
104 29 2 mgpplusg · ˙ = + mulGrp R
105 104 submcl S SubMnd mulGrp R 2 nd u S 2 nd v S 2 nd u · ˙ 2 nd v S
106 103 82 76 105 syl3anc φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 2 nd u · ˙ 2 nd v S
107 104 submcl S SubMnd mulGrp R 2 nd p S 2 nd q S 2 nd p · ˙ 2 nd q S
108 103 99 93 107 syl3anc φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 2 nd p · ˙ 2 nd q S
109 simp-4r φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f S
110 simplr φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R g S
111 104 submcl S SubMnd mulGrp R f S g S f · ˙ g S
112 103 109 110 111 syl3anc φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ g S
113 60 108 sseldd φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 2 nd p · ˙ 2 nd q B
114 1 3 2 ringdir R Ring 1 st u · ˙ 2 nd v B 1 st v · ˙ 2 nd u B 2 nd p · ˙ 2 nd q B 1 st u · ˙ 2 nd v + ˙ 1 st v · ˙ 2 nd u · ˙ 2 nd p · ˙ 2 nd q = 1 st u · ˙ 2 nd v · ˙ 2 nd p · ˙ 2 nd q + ˙ 1 st v · ˙ 2 nd u · ˙ 2 nd p · ˙ 2 nd q
115 66 78 84 113 114 syl13anc φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 1 st u · ˙ 2 nd v + ˙ 1 st v · ˙ 2 nd u · ˙ 2 nd p · ˙ 2 nd q = 1 st u · ˙ 2 nd v · ˙ 2 nd p · ˙ 2 nd q + ˙ 1 st v · ˙ 2 nd u · ˙ 2 nd p · ˙ 2 nd q
116 60 106 sseldd φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 2 nd u · ˙ 2 nd v B
117 1 3 2 ringdir R Ring 1 st p · ˙ 2 nd q B 1 st q · ˙ 2 nd p B 2 nd u · ˙ 2 nd v B 1 st p · ˙ 2 nd q + ˙ 1 st q · ˙ 2 nd p · ˙ 2 nd u · ˙ 2 nd v = 1 st p · ˙ 2 nd q · ˙ 2 nd u · ˙ 2 nd v + ˙ 1 st q · ˙ 2 nd p · ˙ 2 nd u · ˙ 2 nd v
118 66 95 101 116 117 syl13anc φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 1 st p · ˙ 2 nd q + ˙ 1 st q · ˙ 2 nd p · ˙ 2 nd u · ˙ 2 nd v = 1 st p · ˙ 2 nd q · ˙ 2 nd u · ˙ 2 nd v + ˙ 1 st q · ˙ 2 nd p · ˙ 2 nd u · ˙ 2 nd v
119 115 118 oveq12d φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 1 st u · ˙ 2 nd v + ˙ 1 st v · ˙ 2 nd u · ˙ 2 nd p · ˙ 2 nd q - R 1 st p · ˙ 2 nd q + ˙ 1 st q · ˙ 2 nd p · ˙ 2 nd u · ˙ 2 nd v = 1 st u · ˙ 2 nd v · ˙ 2 nd p · ˙ 2 nd q + ˙ 1 st v · ˙ 2 nd u · ˙ 2 nd p · ˙ 2 nd q - R 1 st p · ˙ 2 nd q · ˙ 2 nd u · ˙ 2 nd v + ˙ 1 st q · ˙ 2 nd p · ˙ 2 nd u · ˙ 2 nd v
120 119 oveq2d φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ g · ˙ 1 st u · ˙ 2 nd v + ˙ 1 st v · ˙ 2 nd u · ˙ 2 nd p · ˙ 2 nd q - R 1 st p · ˙ 2 nd q + ˙ 1 st q · ˙ 2 nd p · ˙ 2 nd u · ˙ 2 nd v = f · ˙ g · ˙ 1 st u · ˙ 2 nd v · ˙ 2 nd p · ˙ 2 nd q + ˙ 1 st v · ˙ 2 nd u · ˙ 2 nd p · ˙ 2 nd q - R 1 st p · ˙ 2 nd q · ˙ 2 nd u · ˙ 2 nd v + ˙ 1 st q · ˙ 2 nd p · ˙ 2 nd u · ˙ 2 nd v
121 60 109 sseldd φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f B
122 60 110 sseldd φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R g B
123 1 2 66 121 122 ringcld φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ g B
124 1 2 66 78 113 ringcld φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 1 st u · ˙ 2 nd v · ˙ 2 nd p · ˙ 2 nd q B
125 1 2 66 84 113 ringcld φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 1 st v · ˙ 2 nd u · ˙ 2 nd p · ˙ 2 nd q B
126 1 3 64 124 125 grpcld φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 1 st u · ˙ 2 nd v · ˙ 2 nd p · ˙ 2 nd q + ˙ 1 st v · ˙ 2 nd u · ˙ 2 nd p · ˙ 2 nd q B
127 1 2 66 95 116 ringcld φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 1 st p · ˙ 2 nd q · ˙ 2 nd u · ˙ 2 nd v B
128 1 2 66 101 116 ringcld φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 1 st q · ˙ 2 nd p · ˙ 2 nd u · ˙ 2 nd v B
129 1 3 64 127 128 grpcld φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 1 st p · ˙ 2 nd q · ˙ 2 nd u · ˙ 2 nd v + ˙ 1 st q · ˙ 2 nd p · ˙ 2 nd u · ˙ 2 nd v B
130 1 2 16 66 123 126 129 ringsubdi φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ g · ˙ 1 st u · ˙ 2 nd v · ˙ 2 nd p · ˙ 2 nd q + ˙ 1 st v · ˙ 2 nd u · ˙ 2 nd p · ˙ 2 nd q - R 1 st p · ˙ 2 nd q · ˙ 2 nd u · ˙ 2 nd v + ˙ 1 st q · ˙ 2 nd p · ˙ 2 nd u · ˙ 2 nd v = f · ˙ g · ˙ 1 st u · ˙ 2 nd v · ˙ 2 nd p · ˙ 2 nd q + ˙ 1 st v · ˙ 2 nd u · ˙ 2 nd p · ˙ 2 nd q - R f · ˙ g · ˙ 1 st p · ˙ 2 nd q · ˙ 2 nd u · ˙ 2 nd v + ˙ 1 st q · ˙ 2 nd p · ˙ 2 nd u · ˙ 2 nd v
131 1 3 2 ringdi R Ring f · ˙ g B 1 st u · ˙ 2 nd v · ˙ 2 nd p · ˙ 2 nd q B 1 st v · ˙ 2 nd u · ˙ 2 nd p · ˙ 2 nd q B f · ˙ g · ˙ 1 st u · ˙ 2 nd v · ˙ 2 nd p · ˙ 2 nd q + ˙ 1 st v · ˙ 2 nd u · ˙ 2 nd p · ˙ 2 nd q = f · ˙ g · ˙ 1 st u · ˙ 2 nd v · ˙ 2 nd p · ˙ 2 nd q + ˙ f · ˙ g · ˙ 1 st v · ˙ 2 nd u · ˙ 2 nd p · ˙ 2 nd q
132 66 123 124 125 131 syl13anc φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ g · ˙ 1 st u · ˙ 2 nd v · ˙ 2 nd p · ˙ 2 nd q + ˙ 1 st v · ˙ 2 nd u · ˙ 2 nd p · ˙ 2 nd q = f · ˙ g · ˙ 1 st u · ˙ 2 nd v · ˙ 2 nd p · ˙ 2 nd q + ˙ f · ˙ g · ˙ 1 st v · ˙ 2 nd u · ˙ 2 nd p · ˙ 2 nd q
133 1 3 2 ringdi R Ring f · ˙ g B 1 st p · ˙ 2 nd q · ˙ 2 nd u · ˙ 2 nd v B 1 st q · ˙ 2 nd p · ˙ 2 nd u · ˙ 2 nd v B f · ˙ g · ˙ 1 st p · ˙ 2 nd q · ˙ 2 nd u · ˙ 2 nd v + ˙ 1 st q · ˙ 2 nd p · ˙ 2 nd u · ˙ 2 nd v = f · ˙ g · ˙ 1 st p · ˙ 2 nd q · ˙ 2 nd u · ˙ 2 nd v + ˙ f · ˙ g · ˙ 1 st q · ˙ 2 nd p · ˙ 2 nd u · ˙ 2 nd v
134 66 123 127 128 133 syl13anc φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ g · ˙ 1 st p · ˙ 2 nd q · ˙ 2 nd u · ˙ 2 nd v + ˙ 1 st q · ˙ 2 nd p · ˙ 2 nd u · ˙ 2 nd v = f · ˙ g · ˙ 1 st p · ˙ 2 nd q · ˙ 2 nd u · ˙ 2 nd v + ˙ f · ˙ g · ˙ 1 st q · ˙ 2 nd p · ˙ 2 nd u · ˙ 2 nd v
135 132 134 oveq12d φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ g · ˙ 1 st u · ˙ 2 nd v · ˙ 2 nd p · ˙ 2 nd q + ˙ 1 st v · ˙ 2 nd u · ˙ 2 nd p · ˙ 2 nd q - R f · ˙ g · ˙ 1 st p · ˙ 2 nd q · ˙ 2 nd u · ˙ 2 nd v + ˙ 1 st q · ˙ 2 nd p · ˙ 2 nd u · ˙ 2 nd v = f · ˙ g · ˙ 1 st u · ˙ 2 nd v · ˙ 2 nd p · ˙ 2 nd q + ˙ f · ˙ g · ˙ 1 st v · ˙ 2 nd u · ˙ 2 nd p · ˙ 2 nd q - R f · ˙ g · ˙ 1 st p · ˙ 2 nd q · ˙ 2 nd u · ˙ 2 nd v + ˙ f · ˙ g · ˙ 1 st q · ˙ 2 nd p · ˙ 2 nd u · ˙ 2 nd v
136 66 ringabld φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R R Abel
137 1 2 66 123 124 ringcld φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ g · ˙ 1 st u · ˙ 2 nd v · ˙ 2 nd p · ˙ 2 nd q B
138 1 2 66 123 125 ringcld φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ g · ˙ 1 st v · ˙ 2 nd u · ˙ 2 nd p · ˙ 2 nd q B
139 1 2 66 123 127 ringcld φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ g · ˙ 1 st p · ˙ 2 nd q · ˙ 2 nd u · ˙ 2 nd v B
140 1 2 66 123 128 ringcld φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ g · ˙ 1 st q · ˙ 2 nd p · ˙ 2 nd u · ˙ 2 nd v B
141 1 3 16 ablsub4 R Abel f · ˙ g · ˙ 1 st u · ˙ 2 nd v · ˙ 2 nd p · ˙ 2 nd q B f · ˙ g · ˙ 1 st v · ˙ 2 nd u · ˙ 2 nd p · ˙ 2 nd q B f · ˙ g · ˙ 1 st p · ˙ 2 nd q · ˙ 2 nd u · ˙ 2 nd v B f · ˙ g · ˙ 1 st q · ˙ 2 nd p · ˙ 2 nd u · ˙ 2 nd v B f · ˙ g · ˙ 1 st u · ˙ 2 nd v · ˙ 2 nd p · ˙ 2 nd q + ˙ f · ˙ g · ˙ 1 st v · ˙ 2 nd u · ˙ 2 nd p · ˙ 2 nd q - R f · ˙ g · ˙ 1 st p · ˙ 2 nd q · ˙ 2 nd u · ˙ 2 nd v + ˙ f · ˙ g · ˙ 1 st q · ˙ 2 nd p · ˙ 2 nd u · ˙ 2 nd v = f · ˙ g · ˙ 1 st u · ˙ 2 nd v · ˙ 2 nd p · ˙ 2 nd q - R f · ˙ g · ˙ 1 st p · ˙ 2 nd q · ˙ 2 nd u · ˙ 2 nd v + ˙ f · ˙ g · ˙ 1 st v · ˙ 2 nd u · ˙ 2 nd p · ˙ 2 nd q - R f · ˙ g · ˙ 1 st q · ˙ 2 nd p · ˙ 2 nd u · ˙ 2 nd v
142 136 137 138 139 140 141 syl122anc φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ g · ˙ 1 st u · ˙ 2 nd v · ˙ 2 nd p · ˙ 2 nd q + ˙ f · ˙ g · ˙ 1 st v · ˙ 2 nd u · ˙ 2 nd p · ˙ 2 nd q - R f · ˙ g · ˙ 1 st p · ˙ 2 nd q · ˙ 2 nd u · ˙ 2 nd v + ˙ f · ˙ g · ˙ 1 st q · ˙ 2 nd p · ˙ 2 nd u · ˙ 2 nd v = f · ˙ g · ˙ 1 st u · ˙ 2 nd v · ˙ 2 nd p · ˙ 2 nd q - R f · ˙ g · ˙ 1 st p · ˙ 2 nd q · ˙ 2 nd u · ˙ 2 nd v + ˙ f · ˙ g · ˙ 1 st v · ˙ 2 nd u · ˙ 2 nd p · ˙ 2 nd q - R f · ˙ g · ˙ 1 st q · ˙ 2 nd p · ˙ 2 nd u · ˙ 2 nd v
143 29 crngmgp R CRing mulGrp R CMnd
144 6 143 syl φ mulGrp R CMnd
145 144 ad6antr φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R mulGrp R CMnd
146 30 104 145 121 122 71 77 100 94 cmn246135 φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ g · ˙ 1 st u · ˙ 2 nd v · ˙ 2 nd p · ˙ 2 nd q = g · ˙ 2 nd v · ˙ 2 nd q · ˙ f · ˙ 1 st u · ˙ 2 nd p
147 30 104 145 121 122 89 94 83 77 cmn246135 φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ g · ˙ 1 st p · ˙ 2 nd q · ˙ 2 nd u · ˙ 2 nd v = g · ˙ 2 nd q · ˙ 2 nd v · ˙ f · ˙ 1 st p · ˙ 2 nd u
148 30 104 cmncom mulGrp R CMnd 2 nd v B 2 nd q B 2 nd v · ˙ 2 nd q = 2 nd q · ˙ 2 nd v
149 145 77 94 148 syl3anc φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 2 nd v · ˙ 2 nd q = 2 nd q · ˙ 2 nd v
150 149 oveq2d φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R g · ˙ 2 nd v · ˙ 2 nd q = g · ˙ 2 nd q · ˙ 2 nd v
151 150 oveq1d φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R g · ˙ 2 nd v · ˙ 2 nd q · ˙ f · ˙ 1 st p · ˙ 2 nd u = g · ˙ 2 nd q · ˙ 2 nd v · ˙ f · ˙ 1 st p · ˙ 2 nd u
152 147 151 eqtr4d φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ g · ˙ 1 st p · ˙ 2 nd q · ˙ 2 nd u · ˙ 2 nd v = g · ˙ 2 nd v · ˙ 2 nd q · ˙ f · ˙ 1 st p · ˙ 2 nd u
153 146 152 oveq12d φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ g · ˙ 1 st u · ˙ 2 nd v · ˙ 2 nd p · ˙ 2 nd q - R f · ˙ g · ˙ 1 st p · ˙ 2 nd q · ˙ 2 nd u · ˙ 2 nd v = g · ˙ 2 nd v · ˙ 2 nd q · ˙ f · ˙ 1 st u · ˙ 2 nd p - R g · ˙ 2 nd v · ˙ 2 nd q · ˙ f · ˙ 1 st p · ˙ 2 nd u
154 1 2 66 71 100 ringcld φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 1 st u · ˙ 2 nd p B
155 1 2 66 89 83 ringcld φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 1 st p · ˙ 2 nd u B
156 1 2 16 66 121 154 155 ringsubdi φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = f · ˙ 1 st u · ˙ 2 nd p - R f · ˙ 1 st p · ˙ 2 nd u
157 simpllr φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R
158 156 157 eqtr3d φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ 1 st u · ˙ 2 nd p - R f · ˙ 1 st p · ˙ 2 nd u = 0 R
159 158 oveq2d φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R g · ˙ 2 nd v · ˙ 2 nd q · ˙ f · ˙ 1 st u · ˙ 2 nd p - R f · ˙ 1 st p · ˙ 2 nd u = g · ˙ 2 nd v · ˙ 2 nd q · ˙ 0 R
160 1 2 66 77 94 ringcld φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 2 nd v · ˙ 2 nd q B
161 1 2 66 122 160 ringcld φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R g · ˙ 2 nd v · ˙ 2 nd q B
162 1 2 66 121 154 ringcld φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ 1 st u · ˙ 2 nd p B
163 1 2 66 121 155 ringcld φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ 1 st p · ˙ 2 nd u B
164 1 2 16 66 161 162 163 ringsubdi φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R g · ˙ 2 nd v · ˙ 2 nd q · ˙ f · ˙ 1 st u · ˙ 2 nd p - R f · ˙ 1 st p · ˙ 2 nd u = g · ˙ 2 nd v · ˙ 2 nd q · ˙ f · ˙ 1 st u · ˙ 2 nd p - R g · ˙ 2 nd v · ˙ 2 nd q · ˙ f · ˙ 1 st p · ˙ 2 nd u
165 1 2 15 66 161 ringrzd φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R g · ˙ 2 nd v · ˙ 2 nd q · ˙ 0 R = 0 R
166 159 164 165 3eqtr3d φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R g · ˙ 2 nd v · ˙ 2 nd q · ˙ f · ˙ 1 st u · ˙ 2 nd p - R g · ˙ 2 nd v · ˙ 2 nd q · ˙ f · ˙ 1 st p · ˙ 2 nd u = 0 R
167 153 166 eqtrd φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ g · ˙ 1 st u · ˙ 2 nd v · ˙ 2 nd p · ˙ 2 nd q - R f · ˙ g · ˙ 1 st p · ˙ 2 nd q · ˙ 2 nd u · ˙ 2 nd v = 0 R
168 30 104 145 121 122 80 83 100 94 cmn145236 φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ g · ˙ 1 st v · ˙ 2 nd u · ˙ 2 nd p · ˙ 2 nd q = f · ˙ 2 nd u · ˙ 2 nd p · ˙ g · ˙ 1 st v · ˙ 2 nd q
169 30 104 145 121 122 97 100 83 77 cmn145236 φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ g · ˙ 1 st q · ˙ 2 nd p · ˙ 2 nd u · ˙ 2 nd v = f · ˙ 2 nd p · ˙ 2 nd u · ˙ g · ˙ 1 st q · ˙ 2 nd v
170 30 104 cmncom mulGrp R CMnd 2 nd p B 2 nd u B 2 nd p · ˙ 2 nd u = 2 nd u · ˙ 2 nd p
171 145 100 83 170 syl3anc φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 2 nd p · ˙ 2 nd u = 2 nd u · ˙ 2 nd p
172 171 oveq2d φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ 2 nd p · ˙ 2 nd u = f · ˙ 2 nd u · ˙ 2 nd p
173 172 oveq1d φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ 2 nd p · ˙ 2 nd u · ˙ g · ˙ 1 st q · ˙ 2 nd v = f · ˙ 2 nd u · ˙ 2 nd p · ˙ g · ˙ 1 st q · ˙ 2 nd v
174 169 173 eqtrd φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ g · ˙ 1 st q · ˙ 2 nd p · ˙ 2 nd u · ˙ 2 nd v = f · ˙ 2 nd u · ˙ 2 nd p · ˙ g · ˙ 1 st q · ˙ 2 nd v
175 168 174 oveq12d φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ g · ˙ 1 st v · ˙ 2 nd u · ˙ 2 nd p · ˙ 2 nd q - R f · ˙ g · ˙ 1 st q · ˙ 2 nd p · ˙ 2 nd u · ˙ 2 nd v = f · ˙ 2 nd u · ˙ 2 nd p · ˙ g · ˙ 1 st v · ˙ 2 nd q - R f · ˙ 2 nd u · ˙ 2 nd p · ˙ g · ˙ 1 st q · ˙ 2 nd v
176 1 2 66 80 94 ringcld φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 1 st v · ˙ 2 nd q B
177 1 2 66 97 77 ringcld φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 1 st q · ˙ 2 nd v B
178 1 2 16 66 122 176 177 ringsubdi φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = g · ˙ 1 st v · ˙ 2 nd q - R g · ˙ 1 st q · ˙ 2 nd v
179 simpr φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R
180 178 179 eqtr3d φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R g · ˙ 1 st v · ˙ 2 nd q - R g · ˙ 1 st q · ˙ 2 nd v = 0 R
181 180 oveq2d φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ 2 nd u · ˙ 2 nd p · ˙ g · ˙ 1 st v · ˙ 2 nd q - R g · ˙ 1 st q · ˙ 2 nd v = f · ˙ 2 nd u · ˙ 2 nd p · ˙ 0 R
182 1 2 66 83 100 ringcld φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 2 nd u · ˙ 2 nd p B
183 1 2 66 121 182 ringcld φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ 2 nd u · ˙ 2 nd p B
184 1 2 66 122 176 ringcld φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R g · ˙ 1 st v · ˙ 2 nd q B
185 1 2 66 122 177 ringcld φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R g · ˙ 1 st q · ˙ 2 nd v B
186 1 2 16 66 183 184 185 ringsubdi φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ 2 nd u · ˙ 2 nd p · ˙ g · ˙ 1 st v · ˙ 2 nd q - R g · ˙ 1 st q · ˙ 2 nd v = f · ˙ 2 nd u · ˙ 2 nd p · ˙ g · ˙ 1 st v · ˙ 2 nd q - R f · ˙ 2 nd u · ˙ 2 nd p · ˙ g · ˙ 1 st q · ˙ 2 nd v
187 1 2 15 66 183 ringrzd φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ 2 nd u · ˙ 2 nd p · ˙ 0 R = 0 R
188 181 186 187 3eqtr3d φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ 2 nd u · ˙ 2 nd p · ˙ g · ˙ 1 st v · ˙ 2 nd q - R f · ˙ 2 nd u · ˙ 2 nd p · ˙ g · ˙ 1 st q · ˙ 2 nd v = 0 R
189 175 188 eqtrd φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ g · ˙ 1 st v · ˙ 2 nd u · ˙ 2 nd p · ˙ 2 nd q - R f · ˙ g · ˙ 1 st q · ˙ 2 nd p · ˙ 2 nd u · ˙ 2 nd v = 0 R
190 167 189 oveq12d φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ g · ˙ 1 st u · ˙ 2 nd v · ˙ 2 nd p · ˙ 2 nd q - R f · ˙ g · ˙ 1 st p · ˙ 2 nd q · ˙ 2 nd u · ˙ 2 nd v + ˙ f · ˙ g · ˙ 1 st v · ˙ 2 nd u · ˙ 2 nd p · ˙ 2 nd q - R f · ˙ g · ˙ 1 st q · ˙ 2 nd p · ˙ 2 nd u · ˙ 2 nd v = 0 R + ˙ 0 R
191 1 15 grpidcl R Grp 0 R B
192 64 191 syl φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 0 R B
193 1 3 15 64 192 grplidd φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 0 R + ˙ 0 R = 0 R
194 190 193 eqtrd φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ g · ˙ 1 st u · ˙ 2 nd v · ˙ 2 nd p · ˙ 2 nd q - R f · ˙ g · ˙ 1 st p · ˙ 2 nd q · ˙ 2 nd u · ˙ 2 nd v + ˙ f · ˙ g · ˙ 1 st v · ˙ 2 nd u · ˙ 2 nd p · ˙ 2 nd q - R f · ˙ g · ˙ 1 st q · ˙ 2 nd p · ˙ 2 nd u · ˙ 2 nd v = 0 R
195 135 142 194 3eqtrd φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ g · ˙ 1 st u · ˙ 2 nd v · ˙ 2 nd p · ˙ 2 nd q + ˙ 1 st v · ˙ 2 nd u · ˙ 2 nd p · ˙ 2 nd q - R f · ˙ g · ˙ 1 st p · ˙ 2 nd q · ˙ 2 nd u · ˙ 2 nd v + ˙ 1 st q · ˙ 2 nd p · ˙ 2 nd u · ˙ 2 nd v = 0 R
196 120 130 195 3eqtrd φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R f · ˙ g · ˙ 1 st u · ˙ 2 nd v + ˙ 1 st v · ˙ 2 nd u · ˙ 2 nd p · ˙ 2 nd q - R 1 st p · ˙ 2 nd q + ˙ 1 st q · ˙ 2 nd p · ˙ 2 nd u · ˙ 2 nd v = 0 R
197 1 5 60 15 2 16 61 62 85 102 106 108 112 196 erlbrd φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R 1 st u · ˙ 2 nd v + ˙ 1 st v · ˙ 2 nd u 2 nd u · ˙ 2 nd v ˙ 1 st p · ˙ 2 nd q + ˙ 1 st q · ˙ 2 nd p 2 nd p · ˙ 2 nd q
198 72 ad2antrr φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R v ˙ q
199 1 5 59 15 2 16 198 erldi φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R g S g · ˙ 1 st v · ˙ 2 nd q - R 1 st q · ˙ 2 nd v = 0 R
200 197 199 r19.29a φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R 1 st u · ˙ 2 nd v + ˙ 1 st v · ˙ 2 nd u 2 nd u · ˙ 2 nd v ˙ 1 st p · ˙ 2 nd q + ˙ 1 st q · ˙ 2 nd p 2 nd p · ˙ 2 nd q
201 1 5 58 15 2 16 67 erldi φ u ˙ p v ˙ q f S f · ˙ 1 st u · ˙ 2 nd p - R 1 st p · ˙ 2 nd u = 0 R
202 200 201 r19.29a φ u ˙ p v ˙ q 1 st u · ˙ 2 nd v + ˙ 1 st v · ˙ 2 nd u 2 nd u · ˙ 2 nd v ˙ 1 st p · ˙ 2 nd q + ˙ 1 st q · ˙ 2 nd p 2 nd p · ˙ 2 nd q
203 plusgid + 𝑔 = Slot + ndx
204 snsstp2 + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b
205 204 42 sstri + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a
206 24 mpoexg B × S V B × S V a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b V
207 46 46 206 syl2anc φ a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b V
208 eqid + Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a = + Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a
209 35 37 203 205 207 208 strfv3 φ + Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a = a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b
210 209 ad2antrr φ u ˙ p v ˙ q + Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a = a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b
211 210 oveqd φ u ˙ p v ˙ q u + Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a v = u a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b v
212 opex 1 st u · ˙ 2 nd v + ˙ 1 st v · ˙ 2 nd u 2 nd u · ˙ 2 nd v V
213 212 a1i φ u ˙ p v ˙ q 1 st u · ˙ 2 nd v + ˙ 1 st v · ˙ 2 nd u 2 nd u · ˙ 2 nd v V
214 simpl a = u b = v a = u
215 214 fveq2d a = u b = v 1 st a = 1 st u
216 simpr a = u b = v b = v
217 216 fveq2d a = u b = v 2 nd b = 2 nd v
218 215 217 oveq12d a = u b = v 1 st a · ˙ 2 nd b = 1 st u · ˙ 2 nd v
219 216 fveq2d a = u b = v 1 st b = 1 st v
220 214 fveq2d a = u b = v 2 nd a = 2 nd u
221 219 220 oveq12d a = u b = v 1 st b · ˙ 2 nd a = 1 st v · ˙ 2 nd u
222 218 221 oveq12d a = u b = v 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a = 1 st u · ˙ 2 nd v + ˙ 1 st v · ˙ 2 nd u
223 220 217 oveq12d a = u b = v 2 nd a · ˙ 2 nd b = 2 nd u · ˙ 2 nd v
224 222 223 opeq12d a = u b = v 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b = 1 st u · ˙ 2 nd v + ˙ 1 st v · ˙ 2 nd u 2 nd u · ˙ 2 nd v
225 224 24 ovmpoga u B × S v B × S 1 st u · ˙ 2 nd v + ˙ 1 st v · ˙ 2 nd u 2 nd u · ˙ 2 nd v V u a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b v = 1 st u · ˙ 2 nd v + ˙ 1 st v · ˙ 2 nd u 2 nd u · ˙ 2 nd v
226 68 73 213 225 syl3anc φ u ˙ p v ˙ q u a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b v = 1 st u · ˙ 2 nd v + ˙ 1 st v · ˙ 2 nd u 2 nd u · ˙ 2 nd v
227 211 226 eqtrd φ u ˙ p v ˙ q u + Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a v = 1 st u · ˙ 2 nd v + ˙ 1 st v · ˙ 2 nd u 2 nd u · ˙ 2 nd v
228 210 oveqd φ u ˙ p v ˙ q p + Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a q = p a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b q
229 opex 1 st p · ˙ 2 nd q + ˙ 1 st q · ˙ 2 nd p 2 nd p · ˙ 2 nd q V
230 229 a1i φ u ˙ p v ˙ q 1 st p · ˙ 2 nd q + ˙ 1 st q · ˙ 2 nd p 2 nd p · ˙ 2 nd q V
231 simpl a = p b = q a = p
232 231 fveq2d a = p b = q 1 st a = 1 st p
233 simpr a = p b = q b = q
234 233 fveq2d a = p b = q 2 nd b = 2 nd q
235 232 234 oveq12d a = p b = q 1 st a · ˙ 2 nd b = 1 st p · ˙ 2 nd q
236 233 fveq2d a = p b = q 1 st b = 1 st q
237 231 fveq2d a = p b = q 2 nd a = 2 nd p
238 236 237 oveq12d a = p b = q 1 st b · ˙ 2 nd a = 1 st q · ˙ 2 nd p
239 235 238 oveq12d a = p b = q 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a = 1 st p · ˙ 2 nd q + ˙ 1 st q · ˙ 2 nd p
240 237 234 oveq12d a = p b = q 2 nd a · ˙ 2 nd b = 2 nd p · ˙ 2 nd q
241 239 240 opeq12d a = p b = q 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b = 1 st p · ˙ 2 nd q + ˙ 1 st q · ˙ 2 nd p 2 nd p · ˙ 2 nd q
242 241 24 ovmpoga p B × S q B × S 1 st p · ˙ 2 nd q + ˙ 1 st q · ˙ 2 nd p 2 nd p · ˙ 2 nd q V p a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b q = 1 st p · ˙ 2 nd q + ˙ 1 st q · ˙ 2 nd p 2 nd p · ˙ 2 nd q
243 86 90 230 242 syl3anc φ u ˙ p v ˙ q p a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b q = 1 st p · ˙ 2 nd q + ˙ 1 st q · ˙ 2 nd p 2 nd p · ˙ 2 nd q
244 228 243 eqtrd φ u ˙ p v ˙ q p + Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a q = 1 st p · ˙ 2 nd q + ˙ 1 st q · ˙ 2 nd p 2 nd p · ˙ 2 nd q
245 227 244 breq12d φ u ˙ p v ˙ q u + Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a v ˙ p + Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a q 1 st u · ˙ 2 nd v + ˙ 1 st v · ˙ 2 nd u 2 nd u · ˙ 2 nd v ˙ 1 st p · ˙ 2 nd q + ˙ 1 st q · ˙ 2 nd p 2 nd p · ˙ 2 nd q
246 202 245 mpbird φ u ˙ p v ˙ q u + Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a v ˙ p + Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a q
247 246 anasss φ u ˙ p v ˙ q u + Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a v ˙ p + Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a q
248 247 ex φ u ˙ p v ˙ q u + Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a v ˙ p + Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a q
249 209 oveqd φ p + Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a q = p a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b q
250 249 ad2antrr φ p B × S q B × S p + Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a q = p a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b q
251 simplr φ p B × S q B × S p B × S
252 simpr φ p B × S q B × S q B × S
253 229 a1i φ p B × S q B × S 1 st p · ˙ 2 nd q + ˙ 1 st q · ˙ 2 nd p 2 nd p · ˙ 2 nd q V
254 251 252 253 242 syl3anc φ p B × S q B × S p a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b q = 1 st p · ˙ 2 nd q + ˙ 1 st q · ˙ 2 nd p 2 nd p · ˙ 2 nd q
255 63 ad2antrr φ p B × S q B × S R Grp
256 65 ad2antrr φ p B × S q B × S R Ring
257 251 88 syl φ p B × S q B × S 1 st p B
258 32 ad2antrr φ p B × S q B × S S B
259 252 92 syl φ p B × S q B × S 2 nd q S
260 258 259 sseldd φ p B × S q B × S 2 nd q B
261 1 2 256 257 260 ringcld φ p B × S q B × S 1 st p · ˙ 2 nd q B
262 252 96 syl φ p B × S q B × S 1 st q B
263 251 98 syl φ p B × S q B × S 2 nd p S
264 258 263 sseldd φ p B × S q B × S 2 nd p B
265 1 2 256 262 264 ringcld φ p B × S q B × S 1 st q · ˙ 2 nd p B
266 1 3 255 261 265 grpcld φ p B × S q B × S 1 st p · ˙ 2 nd q + ˙ 1 st q · ˙ 2 nd p B
267 7 ad2antrr φ p B × S q B × S S SubMnd mulGrp R
268 267 263 259 107 syl3anc φ p B × S q B × S 2 nd p · ˙ 2 nd q S
269 266 268 opelxpd φ p B × S q B × S 1 st p · ˙ 2 nd q + ˙ 1 st q · ˙ 2 nd p 2 nd p · ˙ 2 nd q B × S
270 254 269 eqeltrd φ p B × S q B × S p a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b q B × S
271 250 270 eqeltrd φ p B × S q B × S p + Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a q B × S
272 271 anasss φ p B × S q B × S p + Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a q B × S
273 34 49 51 57 248 272 208 12 qusaddval φ E G B × S F H B × S E G ˙ ˙ F H ˙ = E G + Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a F H ˙
274 13 14 273 mpd3an23 φ E G ˙ ˙ F H ˙ = E G + Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a F H ˙
275 209 oveqd φ E G + Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a F H = E G a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b F H
276 24 a1i φ a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b = a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b
277 simprl φ a = E G b = F H a = E G
278 277 fveq2d φ a = E G b = F H 1 st a = 1 st E G
279 8 adantr φ a = E G b = F H E B
280 10 adantr φ a = E G b = F H G S
281 op1stg E B G S 1 st E G = E
282 279 280 281 syl2anc φ a = E G b = F H 1 st E G = E
283 278 282 eqtrd φ a = E G b = F H 1 st a = E
284 simprr φ a = E G b = F H b = F H
285 284 fveq2d φ a = E G b = F H 2 nd b = 2 nd F H
286 9 adantr φ a = E G b = F H F B
287 11 adantr φ a = E G b = F H H S
288 op2ndg F B H S 2 nd F H = H
289 286 287 288 syl2anc φ a = E G b = F H 2 nd F H = H
290 285 289 eqtrd φ a = E G b = F H 2 nd b = H
291 283 290 oveq12d φ a = E G b = F H 1 st a · ˙ 2 nd b = E · ˙ H
292 284 fveq2d φ a = E G b = F H 1 st b = 1 st F H
293 op1stg F B H S 1 st F H = F
294 286 287 293 syl2anc φ a = E G b = F H 1 st F H = F
295 292 294 eqtrd φ a = E G b = F H 1 st b = F
296 277 fveq2d φ a = E G b = F H 2 nd a = 2 nd E G
297 op2ndg E B G S 2 nd E G = G
298 279 280 297 syl2anc φ a = E G b = F H 2 nd E G = G
299 296 298 eqtrd φ a = E G b = F H 2 nd a = G
300 295 299 oveq12d φ a = E G b = F H 1 st b · ˙ 2 nd a = F · ˙ G
301 291 300 oveq12d φ a = E G b = F H 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a = E · ˙ H + ˙ F · ˙ G
302 299 290 oveq12d φ a = E G b = F H 2 nd a · ˙ 2 nd b = G · ˙ H
303 301 302 opeq12d φ a = E G b = F H 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b = E · ˙ H + ˙ F · ˙ G G · ˙ H
304 opex E · ˙ H + ˙ F · ˙ G G · ˙ H V
305 304 a1i φ E · ˙ H + ˙ F · ˙ G G · ˙ H V
306 276 303 13 14 305 ovmpod φ E G a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b F H = E · ˙ H + ˙ F · ˙ G G · ˙ H
307 275 306 eqtrd φ E G + Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a F H = E · ˙ H + ˙ F · ˙ G G · ˙ H
308 307 eceq1d φ E G + Base ndx B × S + ndx a B × S , b B × S 1 st a · ˙ 2 nd b + ˙ 1 st b · ˙ 2 nd a 2 nd a · ˙ 2 nd b ndx a B × S , b B × S 1 st a · ˙ 1 st b 2 nd a · ˙ 2 nd b Scalar ndx Scalar R ndx k Base Scalar R , a B × S k R 1 st a 2 nd a 𝑖 ndx TopSet ndx TopSet R × t TopSet R 𝑡 S ndx a b | a B × S b B × S 1 st a · ˙ 2 nd b R 1 st b · ˙ 2 nd a dist ndx a B × S , b B × S 1 st a · ˙ 2 nd b dist R 1 st b · ˙ 2 nd a F H ˙ = E · ˙ H + ˙ F · ˙ G G · ˙ H ˙
309 274 308 eqtrd φ E G ˙ ˙ F H ˙ = E · ˙ H + ˙ F · ˙ G G · ˙ H ˙