This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- .x. = ( .r ` R )
rlocaddval.3 
|- .+ = ( +g ` R )
rlocaddval.4 
|- L = ( R RLocal S )
rlocaddval.5 
|- .~ = ( R ~RL S )
rlocaddval.r 
|- ( ph -> R e. CRing )
rlocaddval.s 
|- ( ph -> S e. ( SubMnd ` ( mulGrp ` R ) ) )
rlocaddval.6 
|- ( ph -> E e. B )
rlocaddval.7 
|- ( ph -> F e. B )
rlocaddval.8 
|- ( ph -> G e. S )
rlocaddval.9 
|- ( ph -> H e. S )
rlocaddval.10 
|- .(+) = ( +g ` L )
Assertion rlocaddval 
|- ( ph -> ( [ <. E , G >. ] .~ .(+) [ <. F , H >. ] .~ ) = [ <. ( ( E .x. H ) .+ ( F .x. G ) ) , ( G .x. H ) >. ] .~ )

Proof

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