Theorem rlocaddval

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

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

Proof

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