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

Metamath Proof Explorer

Theorem rlocmulval

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 )
rlocmulval.1 
|- .(x) = ( .r ` L )
Assertion rlocmulval 
|- ( ph -> ( [ <. E , G >. ] .~ .(x) [ <. F , H >. ] .~ ) = [ <. ( E .x. F ) , ( 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 rlocmulval.1 
 |-  .(x) = ( .r ` 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. ( 1st ` v ) ) , ( ( 2nd ` u ) .x. ( 2nd ` v ) ) >. = <. ( ( 1st ` u ) .x. ( 1st ` v ) ) , ( ( 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. ( 1st ` q ) ) , ( ( 2nd ` p ) .x. ( 2nd ` q ) ) >. = <. ( ( 1st ` p ) .x. ( 1st ` q ) ) , ( ( 2nd ` p ) .x. ( 2nd ` q ) ) >. )
63 6 crngringd 
 |-  ( ph -> R e. Ring )
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. Ring )
65 simplr 
 |-  ( ( ( ph /\ u .~ p ) /\ v .~ q ) -> u .~ p )
66 1 5 58 65 erlcl1 
 |-  ( ( ( ph /\ u .~ p ) /\ v .~ q ) -> u e. ( B X. S ) )
67 66 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 ) )
68 xp1st 
 |-  ( u e. ( B X. S ) -> ( 1st ` u ) e. B )
69 67 68 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 )
70 simpr 
 |-  ( ( ( ph /\ u .~ p ) /\ v .~ q ) -> v .~ q )
71 1 5 58 70 erlcl1 
 |-  ( ( ( ph /\ u .~ p ) /\ v .~ q ) -> v e. ( B X. S ) )
72 71 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 ) )
73 xp1st 
 |-  ( v e. ( B X. S ) -> ( 1st ` v ) e. B )
74 72 73 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 )
75 1 2 64 69 74 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. ( 1st ` v ) ) e. B )
76 1 5 58 65 erlcl2 
 |-  ( ( ( ph /\ u .~ p ) /\ v .~ q ) -> p e. ( B X. S ) )
77 76 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 ) )
78 xp1st 
 |-  ( p e. ( B X. S ) -> ( 1st ` p ) e. B )
79 77 78 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 )
80 1 5 58 70 erlcl2 
 |-  ( ( ( ph /\ u .~ p ) /\ v .~ q ) -> q e. ( B X. S ) )
81 80 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 ) )
82 xp1st 
 |-  ( q e. ( B X. S ) -> ( 1st ` q ) e. B )
83 81 82 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 )
84 1 2 64 79 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. ( 1st ` q ) ) e. B )
85 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 ) ) )
86 xp2nd 
 |-  ( u e. ( B X. S ) -> ( 2nd ` u ) e. S )
87 67 86 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 )
88 xp2nd 
 |-  ( v e. ( B X. S ) -> ( 2nd ` v ) e. S )
89 72 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 ) ) -> ( 2nd ` v ) e. S )
90 29 2 mgpplusg 
 |-  .x. = ( +g ` ( mulGrp ` R ) )
91 90 submcl 
 |-  ( ( S e. ( SubMnd ` ( mulGrp ` R ) ) /\ ( 2nd ` u ) e. S /\ ( 2nd ` v ) e. S ) -> ( ( 2nd ` u ) .x. ( 2nd ` v ) ) e. S )
92 85 87 89 91 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 )
93 xp2nd 
 |-  ( p e. ( B X. S ) -> ( 2nd ` p ) e. S )
94 77 93 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 )
95 xp2nd 
 |-  ( q e. ( B X. S ) -> ( 2nd ` q ) e. S )
96 81 95 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 )
97 90 submcl 
 |-  ( ( S e. ( SubMnd ` ( mulGrp ` R ) ) /\ ( 2nd ` p ) e. S /\ ( 2nd ` q ) e. S ) -> ( ( 2nd ` p ) .x. ( 2nd ` q ) ) e. S )
98 85 94 96 97 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 )
99 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 )
100 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 )
101 90 submcl 
 |-  ( ( S e. ( SubMnd ` ( mulGrp ` R ) ) /\ f e. S /\ g e. S ) -> ( f .x. g ) e. S )
102 85 99 100 101 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 )
103 60 102 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 .x. g ) e. B )
104 60 98 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 )
105 1 2 64 75 104 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. ( 1st ` v ) ) .x. ( ( 2nd ` p ) .x. ( 2nd ` q ) ) ) e. B )
106 60 92 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 )
107 1 2 64 84 106 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. ( 1st ` q ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` v ) ) ) e. B )
108 1 2 16 64 103 105 107 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. ( 1st ` v ) ) .x. ( ( 2nd ` p ) .x. ( 2nd ` q ) ) ) ( -g ` R ) ( ( ( 1st ` p ) .x. ( 1st ` q ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` v ) ) ) ) ) = ( ( ( f .x. g ) .x. ( ( ( 1st ` u ) .x. ( 1st ` v ) ) .x. ( ( 2nd ` p ) .x. ( 2nd ` q ) ) ) ) ( -g ` R ) ( ( f .x. g ) .x. ( ( ( 1st ` p ) .x. ( 1st ` q ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` v ) ) ) ) ) )
109 64 ringgrpd 
 |-  ( ( ( ( ( ( ( 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 )
110 1 2 64 103 105 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. ( 1st ` v ) ) .x. ( ( 2nd ` p ) .x. ( 2nd ` q ) ) ) ) e. B )
111 1 2 64 79 74 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. ( 1st ` v ) ) e. B )
112 60 87 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 )
113 60 96 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 )
114 1 2 64 112 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 ) ) -> ( ( 2nd ` u ) .x. ( 2nd ` q ) ) e. B )
115 1 2 64 111 114 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. ( 1st ` v ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` q ) ) ) e. B )
116 1 2 64 103 115 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. ( 1st ` v ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` q ) ) ) ) e. B )
117 1 2 64 103 107 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. ( 1st ` q ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` v ) ) ) ) e. B )
118 1 3 16 grpnpncan 
 |-  ( ( R e. Grp /\ ( ( ( f .x. g ) .x. ( ( ( 1st ` u ) .x. ( 1st ` v ) ) .x. ( ( 2nd ` p ) .x. ( 2nd ` q ) ) ) ) e. B /\ ( ( f .x. g ) .x. ( ( ( 1st ` p ) .x. ( 1st ` v ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` q ) ) ) ) e. B /\ ( ( f .x. g ) .x. ( ( ( 1st ` p ) .x. ( 1st ` q ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` v ) ) ) ) e. B ) ) -> ( ( ( ( f .x. g ) .x. ( ( ( 1st ` u ) .x. ( 1st ` v ) ) .x. ( ( 2nd ` p ) .x. ( 2nd ` q ) ) ) ) ( -g ` R ) ( ( f .x. g ) .x. ( ( ( 1st ` p ) .x. ( 1st ` v ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` q ) ) ) ) ) .+ ( ( ( f .x. g ) .x. ( ( ( 1st ` p ) .x. ( 1st ` v ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` q ) ) ) ) ( -g ` R ) ( ( f .x. g ) .x. ( ( ( 1st ` p ) .x. ( 1st ` q ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` v ) ) ) ) ) ) = ( ( ( f .x. g ) .x. ( ( ( 1st ` u ) .x. ( 1st ` v ) ) .x. ( ( 2nd ` p ) .x. ( 2nd ` q ) ) ) ) ( -g ` R ) ( ( f .x. g ) .x. ( ( ( 1st ` p ) .x. ( 1st ` q ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` v ) ) ) ) ) )
119 109 110 116 117 118 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. ( 1st ` v ) ) .x. ( ( 2nd ` p ) .x. ( 2nd ` q ) ) ) ) ( -g ` R ) ( ( f .x. g ) .x. ( ( ( 1st ` p ) .x. ( 1st ` v ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` q ) ) ) ) ) .+ ( ( ( f .x. g ) .x. ( ( ( 1st ` p ) .x. ( 1st ` v ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` q ) ) ) ) ( -g ` R ) ( ( f .x. g ) .x. ( ( ( 1st ` p ) .x. ( 1st ` q ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` v ) ) ) ) ) ) = ( ( ( f .x. g ) .x. ( ( ( 1st ` u ) .x. ( 1st ` v ) ) .x. ( ( 2nd ` p ) .x. ( 2nd ` q ) ) ) ) ( -g ` R ) ( ( f .x. g ) .x. ( ( ( 1st ` p ) .x. ( 1st ` q ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` v ) ) ) ) ) )
120 6 ad2antrr 
 |-  ( ( ( ph /\ u .~ p ) /\ v .~ q ) -> R e. CRing )
121 120 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 ) ) -> R e. CRing )
122 121 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 ) ) -> R e. CRing )
123 29 crngmgp 
 |-  ( R e. CRing -> ( mulGrp ` R ) e. CMnd )
124 122 123 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 ) ) -> ( mulGrp ` R ) e. CMnd )
125 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 ) ) -> f e. B )
126 60 100 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 )
127 60 94 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 )
128 30 90 124 125 126 69 74 127 113 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. ( 1st ` v ) ) .x. ( ( 2nd ` p ) .x. ( 2nd ` q ) ) ) ) = ( ( g .x. ( ( 1st ` v ) .x. ( 2nd ` q ) ) ) .x. ( f .x. ( ( 1st ` u ) .x. ( 2nd ` p ) ) ) ) )
129 30 90 124 125 126 79 74 112 113 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. ( 1st ` v ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` q ) ) ) ) = ( ( g .x. ( ( 1st ` v ) .x. ( 2nd ` q ) ) ) .x. ( f .x. ( ( 1st ` p ) .x. ( 2nd ` u ) ) ) ) )
130 128 129 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. ( 1st ` v ) ) .x. ( ( 2nd ` p ) .x. ( 2nd ` q ) ) ) ) ( -g ` R ) ( ( f .x. g ) .x. ( ( ( 1st ` p ) .x. ( 1st ` v ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` q ) ) ) ) ) = ( ( ( g .x. ( ( 1st ` v ) .x. ( 2nd ` q ) ) ) .x. ( f .x. ( ( 1st ` u ) .x. ( 2nd ` p ) ) ) ) ( -g ` R ) ( ( g .x. ( ( 1st ` v ) .x. ( 2nd ` q ) ) ) .x. ( f .x. ( ( 1st ` p ) .x. ( 2nd ` u ) ) ) ) ) )
131 1 2 64 74 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 ` q ) ) e. B )
132 1 2 64 126 131 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 )
133 1 2 64 69 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 ) ) -> ( ( 1st ` u ) .x. ( 2nd ` p ) ) e. B )
134 1 2 64 125 133 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 )
135 1 2 64 79 112 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 )
136 1 2 64 125 135 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 )
137 1 2 16 64 132 134 136 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 ) ) ) .x. ( ( f .x. ( ( 1st ` u ) .x. ( 2nd ` p ) ) ) ( -g ` R ) ( f .x. ( ( 1st ` p ) .x. ( 2nd ` u ) ) ) ) ) = ( ( ( g .x. ( ( 1st ` v ) .x. ( 2nd ` q ) ) ) .x. ( f .x. ( ( 1st ` u ) .x. ( 2nd ` p ) ) ) ) ( -g ` R ) ( ( g .x. ( ( 1st ` v ) .x. ( 2nd ` q ) ) ) .x. ( f .x. ( ( 1st ` p ) .x. ( 2nd ` u ) ) ) ) ) )
138 1 2 16 64 125 133 135 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 ) ) ) ) )
139 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 ) )
140 138 139 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 ) )
141 140 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. ( ( 1st ` v ) .x. ( 2nd ` q ) ) ) .x. ( ( f .x. ( ( 1st ` u ) .x. ( 2nd ` p ) ) ) ( -g ` R ) ( f .x. ( ( 1st ` p ) .x. ( 2nd ` u ) ) ) ) ) = ( ( g .x. ( ( 1st ` v ) .x. ( 2nd ` q ) ) ) .x. ( 0g ` R ) ) )
142 1 2 15 64 132 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. ( ( 1st ` v ) .x. ( 2nd ` q ) ) ) .x. ( 0g ` R ) ) = ( 0g ` R ) )
143 141 142 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 ) ) -> ( ( g .x. ( ( 1st ` v ) .x. ( 2nd ` q ) ) ) .x. ( ( f .x. ( ( 1st ` u ) .x. ( 2nd ` p ) ) ) ( -g ` R ) ( f .x. ( ( 1st ` p ) .x. ( 2nd ` u ) ) ) ) ) = ( 0g ` R ) )
144 137 143 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 ) ) ) .x. ( f .x. ( ( 1st ` u ) .x. ( 2nd ` p ) ) ) ) ( -g ` R ) ( ( g .x. ( ( 1st ` v ) .x. ( 2nd ` q ) ) ) .x. ( f .x. ( ( 1st ` p ) .x. ( 2nd ` u ) ) ) ) ) = ( 0g ` R ) )
145 130 144 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. ( 1st ` v ) ) .x. ( ( 2nd ` p ) .x. ( 2nd ` q ) ) ) ) ( -g ` R ) ( ( f .x. g ) .x. ( ( ( 1st ` p ) .x. ( 1st ` v ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` q ) ) ) ) ) = ( 0g ` R ) )
146 1 2 122 79 74 crngcomd 
 |-  ( ( ( ( ( ( ( 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. ( 1st ` v ) ) = ( ( 1st ` v ) .x. ( 1st ` p ) ) )
147 146 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 ) ) -> ( ( ( 1st ` p ) .x. ( 1st ` v ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` q ) ) ) = ( ( ( 1st ` v ) .x. ( 1st ` p ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` q ) ) ) )
148 147 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 ` p ) .x. ( 1st ` v ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` q ) ) ) ) = ( ( f .x. g ) .x. ( ( ( 1st ` v ) .x. ( 1st ` p ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` q ) ) ) ) )
149 30 90 124 125 126 74 79 112 113 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. ( 1st ` p ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` q ) ) ) ) = ( ( f .x. ( ( 1st ` p ) .x. ( 2nd ` u ) ) ) .x. ( g .x. ( ( 1st ` v ) .x. ( 2nd ` q ) ) ) ) )
150 148 149 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 ` p ) .x. ( 1st ` v ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` q ) ) ) ) = ( ( f .x. ( ( 1st ` p ) .x. ( 2nd ` u ) ) ) .x. ( g .x. ( ( 1st ` v ) .x. ( 2nd ` q ) ) ) ) )
151 1 2 122 83 79 crngcomd 
 |-  ( ( ( ( ( ( ( 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. ( 1st ` p ) ) = ( ( 1st ` p ) .x. ( 1st ` q ) ) )
152 151 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 ) ) -> ( ( ( 1st ` q ) .x. ( 1st ` p ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` v ) ) ) = ( ( ( 1st ` p ) .x. ( 1st ` q ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` v ) ) ) )
153 152 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 ` q ) .x. ( 1st ` p ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` v ) ) ) ) = ( ( f .x. g ) .x. ( ( ( 1st ` p ) .x. ( 1st ` q ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` v ) ) ) ) )
154 60 89 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 )
155 30 90 124 125 126 83 79 112 154 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. ( 1st ` p ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` v ) ) ) ) = ( ( f .x. ( ( 1st ` p ) .x. ( 2nd ` u ) ) ) .x. ( g .x. ( ( 1st ` q ) .x. ( 2nd ` v ) ) ) ) )
156 153 155 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. g ) .x. ( ( ( 1st ` p ) .x. ( 1st ` q ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` v ) ) ) ) = ( ( f .x. ( ( 1st ` p ) .x. ( 2nd ` u ) ) ) .x. ( g .x. ( ( 1st ` q ) .x. ( 2nd ` v ) ) ) ) )
157 150 156 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 ` p ) .x. ( 1st ` v ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` q ) ) ) ) ( -g ` R ) ( ( f .x. g ) .x. ( ( ( 1st ` p ) .x. ( 1st ` q ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` v ) ) ) ) ) = ( ( ( f .x. ( ( 1st ` p ) .x. ( 2nd ` u ) ) ) .x. ( g .x. ( ( 1st ` v ) .x. ( 2nd ` q ) ) ) ) ( -g ` R ) ( ( f .x. ( ( 1st ` p ) .x. ( 2nd ` u ) ) ) .x. ( g .x. ( ( 1st ` q ) .x. ( 2nd ` v ) ) ) ) ) )
158 1 2 64 83 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 ) ) -> ( ( 1st ` q ) .x. ( 2nd ` v ) ) e. B )
159 1 2 16 64 126 131 158 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 ) ) ) ) )
160 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 ) )
161 159 160 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 ) )
162 161 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. ( ( 1st ` p ) .x. ( 2nd ` u ) ) ) .x. ( ( g .x. ( ( 1st ` v ) .x. ( 2nd ` q ) ) ) ( -g ` R ) ( g .x. ( ( 1st ` q ) .x. ( 2nd ` v ) ) ) ) ) = ( ( f .x. ( ( 1st ` p ) .x. ( 2nd ` u ) ) ) .x. ( 0g ` R ) ) )
163 1 2 64 126 158 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 )
164 1 2 16 64 136 132 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 ) ) -> ( ( f .x. ( ( 1st ` p ) .x. ( 2nd ` u ) ) ) .x. ( ( g .x. ( ( 1st ` v ) .x. ( 2nd ` q ) ) ) ( -g ` R ) ( g .x. ( ( 1st ` q ) .x. ( 2nd ` v ) ) ) ) ) = ( ( ( f .x. ( ( 1st ` p ) .x. ( 2nd ` u ) ) ) .x. ( g .x. ( ( 1st ` v ) .x. ( 2nd ` q ) ) ) ) ( -g ` R ) ( ( f .x. ( ( 1st ` p ) .x. ( 2nd ` u ) ) ) .x. ( g .x. ( ( 1st ` q ) .x. ( 2nd ` v ) ) ) ) ) )
165 1 2 15 64 136 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. ( ( 1st ` p ) .x. ( 2nd ` u ) ) ) .x. ( 0g ` R ) ) = ( 0g ` R ) )
166 162 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 ) ) -> ( ( ( f .x. ( ( 1st ` p ) .x. ( 2nd ` u ) ) ) .x. ( g .x. ( ( 1st ` v ) .x. ( 2nd ` q ) ) ) ) ( -g ` R ) ( ( f .x. ( ( 1st ` p ) .x. ( 2nd ` u ) ) ) .x. ( g .x. ( ( 1st ` q ) .x. ( 2nd ` v ) ) ) ) ) = ( 0g ` R ) )
167 157 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 ` p ) .x. ( 1st ` v ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` q ) ) ) ) ( -g ` R ) ( ( f .x. g ) .x. ( ( ( 1st ` p ) .x. ( 1st ` q ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` v ) ) ) ) ) = ( 0g ` R ) )
168 145 167 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. ( 1st ` v ) ) .x. ( ( 2nd ` p ) .x. ( 2nd ` q ) ) ) ) ( -g ` R ) ( ( f .x. g ) .x. ( ( ( 1st ` p ) .x. ( 1st ` v ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` q ) ) ) ) ) .+ ( ( ( f .x. g ) .x. ( ( ( 1st ` p ) .x. ( 1st ` v ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` q ) ) ) ) ( -g ` R ) ( ( f .x. g ) .x. ( ( ( 1st ` p ) .x. ( 1st ` q ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` v ) ) ) ) ) ) = ( ( 0g ` R ) .+ ( 0g ` R ) ) )
169 1 15 grpidcl 
 |-  ( R e. Grp -> ( 0g ` R ) e. B )
170 109 169 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 )
171 1 3 15 109 170 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 ) )
172 168 171 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. ( 1st ` v ) ) .x. ( ( 2nd ` p ) .x. ( 2nd ` q ) ) ) ) ( -g ` R ) ( ( f .x. g ) .x. ( ( ( 1st ` p ) .x. ( 1st ` v ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` q ) ) ) ) ) .+ ( ( ( f .x. g ) .x. ( ( ( 1st ` p ) .x. ( 1st ` v ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` q ) ) ) ) ( -g ` R ) ( ( f .x. g ) .x. ( ( ( 1st ` p ) .x. ( 1st ` q ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` v ) ) ) ) ) ) = ( 0g ` R ) )
173 108 119 172 3eqtr2d 
 |-  ( ( ( ( ( ( ( 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. ( 1st ` v ) ) .x. ( ( 2nd ` p ) .x. ( 2nd ` q ) ) ) ( -g ` R ) ( ( ( 1st ` p ) .x. ( 1st ` q ) ) .x. ( ( 2nd ` u ) .x. ( 2nd ` v ) ) ) ) ) = ( 0g ` R ) )
174 1 5 60 15 2 16 61 62 75 84 92 98 102 173 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. ( 1st ` v ) ) , ( ( 2nd ` u ) .x. ( 2nd ` v ) ) >. .~ <. ( ( 1st ` p ) .x. ( 1st ` q ) ) , ( ( 2nd ` p ) .x. ( 2nd ` q ) ) >. )
175 70 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 )
176 1 5 59 15 2 16 175 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 ) )
177 174 176 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. ( 1st ` v ) ) , ( ( 2nd ` u ) .x. ( 2nd ` v ) ) >. .~ <. ( ( 1st ` p ) .x. ( 1st ` q ) ) , ( ( 2nd ` p ) .x. ( 2nd ` q ) ) >. )
178 1 5 58 15 2 16 65 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 ) )
179 177 178 r19.29a 
 |-  ( ( ( ph /\ u .~ p ) /\ v .~ q ) -> <. ( ( 1st ` u ) .x. ( 1st ` v ) ) , ( ( 2nd ` u ) .x. ( 2nd ` v ) ) >. .~ <. ( ( 1st ` p ) .x. ( 1st ` q ) ) , ( ( 2nd ` p ) .x. ( 2nd ` q ) ) >. )
180 mulridx 
 |-  .r = Slot ( .r ` ndx )
181 snsstp3 
 |-  { <. ( .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 ) ) >. ) >. }
182 181 42 sstri 
 |-  { <. ( .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 ) ) ) ) >. } )
183 25 mpoexg 
 |-  ( ( ( B X. S ) e. _V /\ ( B X. S ) e. _V ) -> ( a e. ( B X. S ) , b e. ( B X. S ) |-> <. ( ( 1st ` a ) .x. ( 1st ` b ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. ) e. _V )
184 46 46 183 syl2anc 
 |-  ( ph -> ( a e. ( B X. S ) , b e. ( B X. S ) |-> <. ( ( 1st ` a ) .x. ( 1st ` b ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. ) e. _V )
185 eqid 
 |-  ( .r ` ( ( { <. ( 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 ) ) ) ) >. } ) ) = ( .r ` ( ( { <. ( 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 ) ) ) ) >. } ) )
186 35 37 180 182 184 185 strfv3 
 |-  ( ph -> ( .r ` ( ( { <. ( 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. ( 1st ` b ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. ) )
187 186 ad2antrr 
 |-  ( ( ( ph /\ u .~ p ) /\ v .~ q ) -> ( .r ` ( ( { <. ( 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. ( 1st ` b ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. ) )
188 187 oveqd 
 |-  ( ( ( ph /\ u .~ p ) /\ v .~ q ) -> ( u ( .r ` ( ( { <. ( 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. ( 1st ` b ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. ) v ) )
189 opex 
 |-  <. ( ( 1st ` u ) .x. ( 1st ` v ) ) , ( ( 2nd ` u ) .x. ( 2nd ` v ) ) >. e. _V
190 189 a1i 
 |-  ( ( ( ph /\ u .~ p ) /\ v .~ q ) -> <. ( ( 1st ` u ) .x. ( 1st ` v ) ) , ( ( 2nd ` u ) .x. ( 2nd ` v ) ) >. e. _V )
191 simpl 
 |-  ( ( a = u /\ b = v ) -> a = u )
192 191 fveq2d 
 |-  ( ( a = u /\ b = v ) -> ( 1st ` a ) = ( 1st ` u ) )
193 simpr 
 |-  ( ( a = u /\ b = v ) -> b = v )
194 193 fveq2d 
 |-  ( ( a = u /\ b = v ) -> ( 1st ` b ) = ( 1st ` v ) )
195 192 194 oveq12d 
 |-  ( ( a = u /\ b = v ) -> ( ( 1st ` a ) .x. ( 1st ` b ) ) = ( ( 1st ` u ) .x. ( 1st ` v ) ) )
196 191 fveq2d 
 |-  ( ( a = u /\ b = v ) -> ( 2nd ` a ) = ( 2nd ` u ) )
197 193 fveq2d 
 |-  ( ( a = u /\ b = v ) -> ( 2nd ` b ) = ( 2nd ` v ) )
198 196 197 oveq12d 
 |-  ( ( a = u /\ b = v ) -> ( ( 2nd ` a ) .x. ( 2nd ` b ) ) = ( ( 2nd ` u ) .x. ( 2nd ` v ) ) )
199 195 198 opeq12d 
 |-  ( ( a = u /\ b = v ) -> <. ( ( 1st ` a ) .x. ( 1st ` b ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. = <. ( ( 1st ` u ) .x. ( 1st ` v ) ) , ( ( 2nd ` u ) .x. ( 2nd ` v ) ) >. )
200 199 25 ovmpoga 
 |-  ( ( u e. ( B X. S ) /\ v e. ( B X. S ) /\ <. ( ( 1st ` u ) .x. ( 1st ` v ) ) , ( ( 2nd ` u ) .x. ( 2nd ` v ) ) >. e. _V ) -> ( u ( a e. ( B X. S ) , b e. ( B X. S ) |-> <. ( ( 1st ` a ) .x. ( 1st ` b ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. ) v ) = <. ( ( 1st ` u ) .x. ( 1st ` v ) ) , ( ( 2nd ` u ) .x. ( 2nd ` v ) ) >. )
201 66 71 190 200 syl3anc 
 |-  ( ( ( ph /\ u .~ p ) /\ v .~ q ) -> ( u ( a e. ( B X. S ) , b e. ( B X. S ) |-> <. ( ( 1st ` a ) .x. ( 1st ` b ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. ) v ) = <. ( ( 1st ` u ) .x. ( 1st ` v ) ) , ( ( 2nd ` u ) .x. ( 2nd ` v ) ) >. )
202 188 201 eqtrd 
 |-  ( ( ( ph /\ u .~ p ) /\ v .~ q ) -> ( u ( .r ` ( ( { <. ( 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. ( 1st ` v ) ) , ( ( 2nd ` u ) .x. ( 2nd ` v ) ) >. )
203 187 oveqd 
 |-  ( ( ( ph /\ u .~ p ) /\ v .~ q ) -> ( p ( .r ` ( ( { <. ( 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. ( 1st ` b ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. ) q ) )
204 opex 
 |-  <. ( ( 1st ` p ) .x. ( 1st ` q ) ) , ( ( 2nd ` p ) .x. ( 2nd ` q ) ) >. e. _V
205 204 a1i 
 |-  ( ( ( ph /\ u .~ p ) /\ v .~ q ) -> <. ( ( 1st ` p ) .x. ( 1st ` q ) ) , ( ( 2nd ` p ) .x. ( 2nd ` q ) ) >. e. _V )
206 simpl 
 |-  ( ( a = p /\ b = q ) -> a = p )
207 206 fveq2d 
 |-  ( ( a = p /\ b = q ) -> ( 1st ` a ) = ( 1st ` p ) )
208 simpr 
 |-  ( ( a = p /\ b = q ) -> b = q )
209 208 fveq2d 
 |-  ( ( a = p /\ b = q ) -> ( 1st ` b ) = ( 1st ` q ) )
210 207 209 oveq12d 
 |-  ( ( a = p /\ b = q ) -> ( ( 1st ` a ) .x. ( 1st ` b ) ) = ( ( 1st ` p ) .x. ( 1st ` q ) ) )
211 206 fveq2d 
 |-  ( ( a = p /\ b = q ) -> ( 2nd ` a ) = ( 2nd ` p ) )
212 208 fveq2d 
 |-  ( ( a = p /\ b = q ) -> ( 2nd ` b ) = ( 2nd ` q ) )
213 211 212 oveq12d 
 |-  ( ( a = p /\ b = q ) -> ( ( 2nd ` a ) .x. ( 2nd ` b ) ) = ( ( 2nd ` p ) .x. ( 2nd ` q ) ) )
214 210 213 opeq12d 
 |-  ( ( a = p /\ b = q ) -> <. ( ( 1st ` a ) .x. ( 1st ` b ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. = <. ( ( 1st ` p ) .x. ( 1st ` q ) ) , ( ( 2nd ` p ) .x. ( 2nd ` q ) ) >. )
215 214 25 ovmpoga 
 |-  ( ( p e. ( B X. S ) /\ q e. ( B X. S ) /\ <. ( ( 1st ` p ) .x. ( 1st ` q ) ) , ( ( 2nd ` p ) .x. ( 2nd ` q ) ) >. e. _V ) -> ( p ( a e. ( B X. S ) , b e. ( B X. S ) |-> <. ( ( 1st ` a ) .x. ( 1st ` b ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. ) q ) = <. ( ( 1st ` p ) .x. ( 1st ` q ) ) , ( ( 2nd ` p ) .x. ( 2nd ` q ) ) >. )
216 76 80 205 215 syl3anc 
 |-  ( ( ( ph /\ u .~ p ) /\ v .~ q ) -> ( p ( a e. ( B X. S ) , b e. ( B X. S ) |-> <. ( ( 1st ` a ) .x. ( 1st ` b ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. ) q ) = <. ( ( 1st ` p ) .x. ( 1st ` q ) ) , ( ( 2nd ` p ) .x. ( 2nd ` q ) ) >. )
217 203 216 eqtrd 
 |-  ( ( ( ph /\ u .~ p ) /\ v .~ q ) -> ( p ( .r ` ( ( { <. ( 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. ( 1st ` q ) ) , ( ( 2nd ` p ) .x. ( 2nd ` q ) ) >. )
218 202 217 breq12d 
 |-  ( ( ( ph /\ u .~ p ) /\ v .~ q ) -> ( ( u ( .r ` ( ( { <. ( 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 ( .r ` ( ( { <. ( 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. ( 1st ` v ) ) , ( ( 2nd ` u ) .x. ( 2nd ` v ) ) >. .~ <. ( ( 1st ` p ) .x. ( 1st ` q ) ) , ( ( 2nd ` p ) .x. ( 2nd ` q ) ) >. ) )
219 179 218 mpbird 
 |-  ( ( ( ph /\ u .~ p ) /\ v .~ q ) -> ( u ( .r ` ( ( { <. ( 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 ( .r ` ( ( { <. ( 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 ) )
220 219 anasss 
 |-  ( ( ph /\ ( u .~ p /\ v .~ q ) ) -> ( u ( .r ` ( ( { <. ( 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 ( .r ` ( ( { <. ( 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 ) )
221 220 ex 
 |-  ( ph -> ( ( u .~ p /\ v .~ q ) -> ( u ( .r ` ( ( { <. ( 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 ( .r ` ( ( { <. ( 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 ) ) )
222 186 oveqd 
 |-  ( ph -> ( p ( .r ` ( ( { <. ( 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. ( 1st ` b ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. ) q ) )
223 222 ad2antrr 
 |-  ( ( ( ph /\ p e. ( B X. S ) ) /\ q e. ( B X. S ) ) -> ( p ( .r ` ( ( { <. ( 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. ( 1st ` b ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. ) q ) )
224 simplr 
 |-  ( ( ( ph /\ p e. ( B X. S ) ) /\ q e. ( B X. S ) ) -> p e. ( B X. S ) )
225 simpr 
 |-  ( ( ( ph /\ p e. ( B X. S ) ) /\ q e. ( B X. S ) ) -> q e. ( B X. S ) )
226 204 a1i 
 |-  ( ( ( ph /\ p e. ( B X. S ) ) /\ q e. ( B X. S ) ) -> <. ( ( 1st ` p ) .x. ( 1st ` q ) ) , ( ( 2nd ` p ) .x. ( 2nd ` q ) ) >. e. _V )
227 224 225 226 215 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. ( 1st ` b ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. ) q ) = <. ( ( 1st ` p ) .x. ( 1st ` q ) ) , ( ( 2nd ` p ) .x. ( 2nd ` q ) ) >. )
228 63 ad2antrr 
 |-  ( ( ( ph /\ p e. ( B X. S ) ) /\ q e. ( B X. S ) ) -> R e. Ring )
229 224 78 syl 
 |-  ( ( ( ph /\ p e. ( B X. S ) ) /\ q e. ( B X. S ) ) -> ( 1st ` p ) e. B )
230 225 82 syl 
 |-  ( ( ( ph /\ p e. ( B X. S ) ) /\ q e. ( B X. S ) ) -> ( 1st ` q ) e. B )
231 1 2 228 229 230 ringcld 
 |-  ( ( ( ph /\ p e. ( B X. S ) ) /\ q e. ( B X. S ) ) -> ( ( 1st ` p ) .x. ( 1st ` q ) ) e. B )
232 7 ad2antrr 
 |-  ( ( ( ph /\ p e. ( B X. S ) ) /\ q e. ( B X. S ) ) -> S e. ( SubMnd ` ( mulGrp ` R ) ) )
233 224 93 syl 
 |-  ( ( ( ph /\ p e. ( B X. S ) ) /\ q e. ( B X. S ) ) -> ( 2nd ` p ) e. S )
234 225 95 syl 
 |-  ( ( ( ph /\ p e. ( B X. S ) ) /\ q e. ( B X. S ) ) -> ( 2nd ` q ) e. S )
235 232 233 234 97 syl3anc 
 |-  ( ( ( ph /\ p e. ( B X. S ) ) /\ q e. ( B X. S ) ) -> ( ( 2nd ` p ) .x. ( 2nd ` q ) ) e. S )
236 231 235 opelxpd 
 |-  ( ( ( ph /\ p e. ( B X. S ) ) /\ q e. ( B X. S ) ) -> <. ( ( 1st ` p ) .x. ( 1st ` q ) ) , ( ( 2nd ` p ) .x. ( 2nd ` q ) ) >. e. ( B X. S ) )
237 227 236 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. ( 1st ` b ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. ) q ) e. ( B X. S ) )
238 223 237 eqeltrd 
 |-  ( ( ( ph /\ p e. ( B X. S ) ) /\ q e. ( B X. S ) ) -> ( p ( .r ` ( ( { <. ( 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 ) )
239 238 anasss 
 |-  ( ( ph /\ ( p e. ( B X. S ) /\ q e. ( B X. S ) ) ) -> ( p ( .r ` ( ( { <. ( 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 ) )
240 34 49 51 57 221 239 185 12 qusmulval 
 |-  ( ( ph /\ <. E , G >. e. ( B X. S ) /\ <. F , H >. e. ( B X. S ) ) -> ( [ <. E , G >. ] .~ .(x) [ <. F , H >. ] .~ ) = [ ( <. E , G >. ( .r ` ( ( { <. ( 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 >. ) ] .~ )
241 13 14 240 mpd3an23 
 |-  ( ph -> ( [ <. E , G >. ] .~ .(x) [ <. F , H >. ] .~ ) = [ ( <. E , G >. ( .r ` ( ( { <. ( 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 >. ) ] .~ )
242 186 oveqd 
 |-  ( ph -> ( <. E , G >. ( .r ` ( ( { <. ( 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. ( 1st ` b ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. ) <. F , H >. ) )
243 25 a1i 
 |-  ( ph -> ( 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 ) ) >. ) )
244 simprl 
 |-  ( ( ph /\ ( a = <. E , G >. /\ b = <. F , H >. ) ) -> a = <. E , G >. )
245 244 fveq2d 
 |-  ( ( ph /\ ( a = <. E , G >. /\ b = <. F , H >. ) ) -> ( 1st ` a ) = ( 1st ` <. E , G >. ) )
246 8 adantr 
 |-  ( ( ph /\ ( a = <. E , G >. /\ b = <. F , H >. ) ) -> E e. B )
247 10 adantr 
 |-  ( ( ph /\ ( a = <. E , G >. /\ b = <. F , H >. ) ) -> G e. S )
248 op1stg 
 |-  ( ( E e. B /\ G e. S ) -> ( 1st ` <. E , G >. ) = E )
249 246 247 248 syl2anc 
 |-  ( ( ph /\ ( a = <. E , G >. /\ b = <. F , H >. ) ) -> ( 1st ` <. E , G >. ) = E )
250 245 249 eqtrd 
 |-  ( ( ph /\ ( a = <. E , G >. /\ b = <. F , H >. ) ) -> ( 1st ` a ) = E )
251 simprr 
 |-  ( ( ph /\ ( a = <. E , G >. /\ b = <. F , H >. ) ) -> b = <. F , H >. )
252 251 fveq2d 
 |-  ( ( ph /\ ( a = <. E , G >. /\ b = <. F , H >. ) ) -> ( 1st ` b ) = ( 1st ` <. F , H >. ) )
253 9 adantr 
 |-  ( ( ph /\ ( a = <. E , G >. /\ b = <. F , H >. ) ) -> F e. B )
254 11 adantr 
 |-  ( ( ph /\ ( a = <. E , G >. /\ b = <. F , H >. ) ) -> H e. S )
255 op1stg 
 |-  ( ( F e. B /\ H e. S ) -> ( 1st ` <. F , H >. ) = F )
256 253 254 255 syl2anc 
 |-  ( ( ph /\ ( a = <. E , G >. /\ b = <. F , H >. ) ) -> ( 1st ` <. F , H >. ) = F )
257 252 256 eqtrd 
 |-  ( ( ph /\ ( a = <. E , G >. /\ b = <. F , H >. ) ) -> ( 1st ` b ) = F )
258 250 257 oveq12d 
 |-  ( ( ph /\ ( a = <. E , G >. /\ b = <. F , H >. ) ) -> ( ( 1st ` a ) .x. ( 1st ` b ) ) = ( E .x. F ) )
259 244 fveq2d 
 |-  ( ( ph /\ ( a = <. E , G >. /\ b = <. F , H >. ) ) -> ( 2nd ` a ) = ( 2nd ` <. E , G >. ) )
260 op2ndg 
 |-  ( ( E e. B /\ G e. S ) -> ( 2nd ` <. E , G >. ) = G )
261 246 247 260 syl2anc 
 |-  ( ( ph /\ ( a = <. E , G >. /\ b = <. F , H >. ) ) -> ( 2nd ` <. E , G >. ) = G )
262 259 261 eqtrd 
 |-  ( ( ph /\ ( a = <. E , G >. /\ b = <. F , H >. ) ) -> ( 2nd ` a ) = G )
263 251 fveq2d 
 |-  ( ( ph /\ ( a = <. E , G >. /\ b = <. F , H >. ) ) -> ( 2nd ` b ) = ( 2nd ` <. F , H >. ) )
264 op2ndg 
 |-  ( ( F e. B /\ H e. S ) -> ( 2nd ` <. F , H >. ) = H )
265 253 254 264 syl2anc 
 |-  ( ( ph /\ ( a = <. E , G >. /\ b = <. F , H >. ) ) -> ( 2nd ` <. F , H >. ) = H )
266 263 265 eqtrd 
 |-  ( ( ph /\ ( a = <. E , G >. /\ b = <. F , H >. ) ) -> ( 2nd ` b ) = H )
267 262 266 oveq12d 
 |-  ( ( ph /\ ( a = <. E , G >. /\ b = <. F , H >. ) ) -> ( ( 2nd ` a ) .x. ( 2nd ` b ) ) = ( G .x. H ) )
268 258 267 opeq12d 
 |-  ( ( ph /\ ( a = <. E , G >. /\ b = <. F , H >. ) ) -> <. ( ( 1st ` a ) .x. ( 1st ` b ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. = <. ( E .x. F ) , ( G .x. H ) >. )
269 opex 
 |-  <. ( E .x. F ) , ( G .x. H ) >. e. _V
270 269 a1i 
 |-  ( ph -> <. ( E .x. F ) , ( G .x. H ) >. e. _V )
271 243 268 13 14 270 ovmpod 
 |-  ( ph -> ( <. E , G >. ( a e. ( B X. S ) , b e. ( B X. S ) |-> <. ( ( 1st ` a ) .x. ( 1st ` b ) ) , ( ( 2nd ` a ) .x. ( 2nd ` b ) ) >. ) <. F , H >. ) = <. ( E .x. F ) , ( G .x. H ) >. )
272 242 271 eqtrd 
 |-  ( ph -> ( <. E , G >. ( .r ` ( ( { <. ( 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. F ) , ( G .x. H ) >. )
273 272 eceq1d 
 |-  ( ph -> [ ( <. E , G >. ( .r ` ( ( { <. ( 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. F ) , ( G .x. H ) >. ] .~ )
274 241 273 eqtrd 
 |-  ( ph -> ( [ <. E , G >. ] .~ .(x) [ <. F , H >. ] .~ ) = [ <. ( E .x. F ) , ( G .x. H ) >. ] .~ )