Metamath Proof Explorer

Theorem erler

Description: The relation used to build the ring localization is an equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025)

Ref Expression
Hypotheses erler.1 
|- B = ( Base ` R )
erler.2 
|- .0. = ( 0g ` R )
erler.3 
|- .1. = ( 1r ` R )
erler.4 
|- .x. = ( .r ` R )
erler.5 
|- .- = ( -g ` R )
erler.w 
|- W = ( B X. S )
erler.q 
|- .~ = ( R ~RL S )
erler.r 
|- ( ph -> R e. CRing )
erler.s 
|- ( ph -> S e. ( SubMnd ` ( mulGrp ` R ) ) )
Assertion erler 
|- ( ph -> .~ Er W )

Proof

Step Hyp Ref Expression
1 erler.1 
 |-  B = ( Base ` R )
2 erler.2 
 |-  .0. = ( 0g ` R )
3 erler.3 
 |-  .1. = ( 1r ` R )
4 erler.4 
 |-  .x. = ( .r ` R )
5 erler.5 
 |-  .- = ( -g ` R )
6 erler.w 
 |-  W = ( B X. S )
7 erler.q 
 |-  .~ = ( R ~RL S )
8 erler.r 
 |-  ( ph -> R e. CRing )
9 erler.s 
 |-  ( ph -> S e. ( SubMnd ` ( mulGrp ` R ) ) )
10 eqid 
 |-  { <. a , b >. | ( ( a e. W /\ b e. W ) /\ E. t e. S ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. ) } = { <. a , b >. | ( ( a e. W /\ b e. W ) /\ E. t e. S ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. ) }
11 10 relopabiv 
 |-  Rel { <. a , b >. | ( ( a e. W /\ b e. W ) /\ E. t e. S ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. ) }
12 11 a1i 
 |-  ( ph -> Rel { <. a , b >. | ( ( a e. W /\ b e. W ) /\ E. t e. S ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. ) } )
13 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
14 13 1 mgpbas 
 |-  B = ( Base ` ( mulGrp ` R ) )
15 14 submss 
 |-  ( S e. ( SubMnd ` ( mulGrp ` R ) ) -> S C_ B )
16 9 15 syl 
 |-  ( ph -> S C_ B )
17 1 2 4 5 6 10 16 erlval 
 |-  ( ph -> ( R ~RL S ) = { <. a , b >. | ( ( a e. W /\ b e. W ) /\ E. t e. S ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. ) } )
18 7 17 eqtrid 
 |-  ( ph -> .~ = { <. a , b >. | ( ( a e. W /\ b e. W ) /\ E. t e. S ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. ) } )
19 18 releqd 
 |-  ( ph -> ( Rel .~ <-> Rel { <. a , b >. | ( ( a e. W /\ b e. W ) /\ E. t e. S ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. ) } ) )
20 12 19 mpbird 
 |-  ( ph -> Rel .~ )
21 simpl 
 |-  ( ( a = x /\ b = y ) -> a = x )
22 21 fveq2d 
 |-  ( ( a = x /\ b = y ) -> ( 1st ` a ) = ( 1st ` x ) )
23 simpr 
 |-  ( ( a = x /\ b = y ) -> b = y )
24 23 fveq2d 
 |-  ( ( a = x /\ b = y ) -> ( 2nd ` b ) = ( 2nd ` y ) )
25 22 24 oveq12d 
 |-  ( ( a = x /\ b = y ) -> ( ( 1st ` a ) .x. ( 2nd ` b ) ) = ( ( 1st ` x ) .x. ( 2nd ` y ) ) )
26 23 fveq2d 
 |-  ( ( a = x /\ b = y ) -> ( 1st ` b ) = ( 1st ` y ) )
27 21 fveq2d 
 |-  ( ( a = x /\ b = y ) -> ( 2nd ` a ) = ( 2nd ` x ) )
28 26 27 oveq12d 
 |-  ( ( a = x /\ b = y ) -> ( ( 1st ` b ) .x. ( 2nd ` a ) ) = ( ( 1st ` y ) .x. ( 2nd ` x ) ) )
29 25 28 oveq12d 
 |-  ( ( a = x /\ b = y ) -> ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) = ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) )
30 29 oveq2d 
 |-  ( ( a = x /\ b = y ) -> ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) )
31 30 eqeq1d 
 |-  ( ( a = x /\ b = y ) -> ( ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. <-> ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) )
32 31 rexbidv 
 |-  ( ( a = x /\ b = y ) -> ( E. t e. S ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. <-> E. t e. S ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) )
33 32 adantl 
 |-  ( ( ph /\ ( a = x /\ b = y ) ) -> ( E. t e. S ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. <-> E. t e. S ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) )
34 18 33 brab2d 
 |-  ( ph -> ( x .~ y <-> ( ( x e. W /\ y e. W ) /\ E. t e. S ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) ) )
35 34 biimpa 
 |-  ( ( ph /\ x .~ y ) -> ( ( x e. W /\ y e. W ) /\ E. t e. S ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) )
36 35 simplrd 
 |-  ( ( ph /\ x .~ y ) -> y e. W )
37 35 simplld 
 |-  ( ( ph /\ x .~ y ) -> x e. W )
38 36 37 jca 
 |-  ( ( ph /\ x .~ y ) -> ( y e. W /\ x e. W ) )
39 35 simprd 
 |-  ( ( ph /\ x .~ y ) -> E. t e. S ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. )
40 8 crngringd 
 |-  ( ph -> R e. Ring )
41 40 ringgrpd 
 |-  ( ph -> R e. Grp )
42 41 ad3antrrr 
 |-  ( ( ( ( ph /\ x .~ y ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) -> R e. Grp )
43 40 ad3antrrr 
 |-  ( ( ( ( ph /\ x .~ y ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) -> R e. Ring )
44 37 ad2antrr 
 |-  ( ( ( ( ph /\ x .~ y ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) -> x e. W )
45 xp1st 
 |-  ( x e. ( B X. S ) -> ( 1st ` x ) e. B )
46 45 6 eleq2s 
 |-  ( x e. W -> ( 1st ` x ) e. B )
47 44 46 syl 
 |-  ( ( ( ( ph /\ x .~ y ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) -> ( 1st ` x ) e. B )
48 16 ad3antrrr 
 |-  ( ( ( ( ph /\ x .~ y ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) -> S C_ B )
49 36 ad2antrr 
 |-  ( ( ( ( ph /\ x .~ y ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) -> y e. W )
50 xp2nd 
 |-  ( y e. ( B X. S ) -> ( 2nd ` y ) e. S )
51 50 6 eleq2s 
 |-  ( y e. W -> ( 2nd ` y ) e. S )
52 49 51 syl 
 |-  ( ( ( ( ph /\ x .~ y ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) -> ( 2nd ` y ) e. S )
53 48 52 sseldd 
 |-  ( ( ( ( ph /\ x .~ y ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) -> ( 2nd ` y ) e. B )
54 1 4 43 47 53 ringcld 
 |-  ( ( ( ( ph /\ x .~ y ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) -> ( ( 1st ` x ) .x. ( 2nd ` y ) ) e. B )
55 xp1st 
 |-  ( y e. ( B X. S ) -> ( 1st ` y ) e. B )
56 55 6 eleq2s 
 |-  ( y e. W -> ( 1st ` y ) e. B )
57 49 56 syl 
 |-  ( ( ( ( ph /\ x .~ y ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) -> ( 1st ` y ) e. B )
58 xp2nd 
 |-  ( x e. ( B X. S ) -> ( 2nd ` x ) e. S )
59 58 6 eleq2s 
 |-  ( x e. W -> ( 2nd ` x ) e. S )
60 44 59 syl 
 |-  ( ( ( ( ph /\ x .~ y ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) -> ( 2nd ` x ) e. S )
61 48 60 sseldd 
 |-  ( ( ( ( ph /\ x .~ y ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) -> ( 2nd ` x ) e. B )
62 1 4 43 57 61 ringcld 
 |-  ( ( ( ( ph /\ x .~ y ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) -> ( ( 1st ` y ) .x. ( 2nd ` x ) ) e. B )
63 eqid 
 |-  ( invg ` R ) = ( invg ` R )
64 1 5 63 grpinvsub 
 |-  ( ( R e. Grp /\ ( ( 1st ` x ) .x. ( 2nd ` y ) ) e. B /\ ( ( 1st ` y ) .x. ( 2nd ` x ) ) e. B ) -> ( ( invg ` R ) ` ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = ( ( ( 1st ` y ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` y ) ) ) )
65 42 54 62 64 syl3anc 
 |-  ( ( ( ( ph /\ x .~ y ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) -> ( ( invg ` R ) ` ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = ( ( ( 1st ` y ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` y ) ) ) )
66 65 oveq2d 
 |-  ( ( ( ( ph /\ x .~ y ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) -> ( t .x. ( ( invg ` R ) ` ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) ) = ( t .x. ( ( ( 1st ` y ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` y ) ) ) ) )
67 simplr 
 |-  ( ( ( ( ph /\ x .~ y ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) -> t e. S )
68 48 67 sseldd 
 |-  ( ( ( ( ph /\ x .~ y ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) -> t e. B )
69 1 5 grpsubcl 
 |-  ( ( R e. Grp /\ ( ( 1st ` x ) .x. ( 2nd ` y ) ) e. B /\ ( ( 1st ` y ) .x. ( 2nd ` x ) ) e. B ) -> ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) e. B )
70 42 54 62 69 syl3anc 
 |-  ( ( ( ( ph /\ x .~ y ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) -> ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) e. B )
71 1 4 63 43 68 70 ringmneg2 
 |-  ( ( ( ( ph /\ x .~ y ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) -> ( t .x. ( ( invg ` R ) ` ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) ) = ( ( invg ` R ) ` ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) ) )
72 simpr 
 |-  ( ( ( ( ph /\ x .~ y ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) -> ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. )
73 72 fveq2d 
 |-  ( ( ( ( ph /\ x .~ y ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) -> ( ( invg ` R ) ` ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) ) = ( ( invg ` R ) ` .0. ) )
74 2 63 grpinvid 
 |-  ( R e. Grp -> ( ( invg ` R ) ` .0. ) = .0. )
75 42 74 syl 
 |-  ( ( ( ( ph /\ x .~ y ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) -> ( ( invg ` R ) ` .0. ) = .0. )
76 71 73 75 3eqtrd 
 |-  ( ( ( ( ph /\ x .~ y ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) -> ( t .x. ( ( invg ` R ) ` ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) ) = .0. )
77 66 76 eqtr3d 
 |-  ( ( ( ( ph /\ x .~ y ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) -> ( t .x. ( ( ( 1st ` y ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` y ) ) ) ) = .0. )
78 77 ex 
 |-  ( ( ( ph /\ x .~ y ) /\ t e. S ) -> ( ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. -> ( t .x. ( ( ( 1st ` y ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` y ) ) ) ) = .0. ) )
79 78 reximdva 
 |-  ( ( ph /\ x .~ y ) -> ( E. t e. S ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. -> E. t e. S ( t .x. ( ( ( 1st ` y ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` y ) ) ) ) = .0. ) )
80 39 79 mpd 
 |-  ( ( ph /\ x .~ y ) -> E. t e. S ( t .x. ( ( ( 1st ` y ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` y ) ) ) ) = .0. )
81 38 80 jca 
 |-  ( ( ph /\ x .~ y ) -> ( ( y e. W /\ x e. W ) /\ E. t e. S ( t .x. ( ( ( 1st ` y ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` y ) ) ) ) = .0. ) )
82 simpl 
 |-  ( ( a = y /\ b = x ) -> a = y )
83 82 fveq2d 
 |-  ( ( a = y /\ b = x ) -> ( 1st ` a ) = ( 1st ` y ) )
84 simpr 
 |-  ( ( a = y /\ b = x ) -> b = x )
85 84 fveq2d 
 |-  ( ( a = y /\ b = x ) -> ( 2nd ` b ) = ( 2nd ` x ) )
86 83 85 oveq12d 
 |-  ( ( a = y /\ b = x ) -> ( ( 1st ` a ) .x. ( 2nd ` b ) ) = ( ( 1st ` y ) .x. ( 2nd ` x ) ) )
87 84 fveq2d 
 |-  ( ( a = y /\ b = x ) -> ( 1st ` b ) = ( 1st ` x ) )
88 82 fveq2d 
 |-  ( ( a = y /\ b = x ) -> ( 2nd ` a ) = ( 2nd ` y ) )
89 87 88 oveq12d 
 |-  ( ( a = y /\ b = x ) -> ( ( 1st ` b ) .x. ( 2nd ` a ) ) = ( ( 1st ` x ) .x. ( 2nd ` y ) ) )
90 86 89 oveq12d 
 |-  ( ( a = y /\ b = x ) -> ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) = ( ( ( 1st ` y ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` y ) ) ) )
91 90 oveq2d 
 |-  ( ( a = y /\ b = x ) -> ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = ( t .x. ( ( ( 1st ` y ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` y ) ) ) ) )
92 91 eqeq1d 
 |-  ( ( a = y /\ b = x ) -> ( ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. <-> ( t .x. ( ( ( 1st ` y ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` y ) ) ) ) = .0. ) )
93 92 rexbidv 
 |-  ( ( a = y /\ b = x ) -> ( E. t e. S ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. <-> E. t e. S ( t .x. ( ( ( 1st ` y ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` y ) ) ) ) = .0. ) )
94 93 adantl 
 |-  ( ( ph /\ ( a = y /\ b = x ) ) -> ( E. t e. S ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. <-> E. t e. S ( t .x. ( ( ( 1st ` y ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` y ) ) ) ) = .0. ) )
95 18 94 brab2d 
 |-  ( ph -> ( y .~ x <-> ( ( y e. W /\ x e. W ) /\ E. t e. S ( t .x. ( ( ( 1st ` y ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` y ) ) ) ) = .0. ) ) )
96 95 adantr 
 |-  ( ( ph /\ x .~ y ) -> ( y .~ x <-> ( ( y e. W /\ x e. W ) /\ E. t e. S ( t .x. ( ( ( 1st ` y ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` y ) ) ) ) = .0. ) ) )
97 81 96 mpbird 
 |-  ( ( ph /\ x .~ y ) -> y .~ x )
98 9 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> S e. ( SubMnd ` ( mulGrp ` R ) ) )
99 98 15 syl 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> S C_ B )
100 37 adantr 
 |-  ( ( ( ph /\ x .~ y ) /\ y .~ z ) -> x e. W )
101 100 ad4antr 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> x e. W )
102 101 6 eleqtrdi 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> x e. ( B X. S ) )
103 1st2nd2 
 |-  ( x e. ( B X. S ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
104 102 103 syl 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
105 simpl 
 |-  ( ( a = y /\ b = z ) -> a = y )
106 105 fveq2d 
 |-  ( ( a = y /\ b = z ) -> ( 1st ` a ) = ( 1st ` y ) )
107 simpr 
 |-  ( ( a = y /\ b = z ) -> b = z )
108 107 fveq2d 
 |-  ( ( a = y /\ b = z ) -> ( 2nd ` b ) = ( 2nd ` z ) )
109 106 108 oveq12d 
 |-  ( ( a = y /\ b = z ) -> ( ( 1st ` a ) .x. ( 2nd ` b ) ) = ( ( 1st ` y ) .x. ( 2nd ` z ) ) )
110 107 fveq2d 
 |-  ( ( a = y /\ b = z ) -> ( 1st ` b ) = ( 1st ` z ) )
111 105 fveq2d 
 |-  ( ( a = y /\ b = z ) -> ( 2nd ` a ) = ( 2nd ` y ) )
112 110 111 oveq12d 
 |-  ( ( a = y /\ b = z ) -> ( ( 1st ` b ) .x. ( 2nd ` a ) ) = ( ( 1st ` z ) .x. ( 2nd ` y ) ) )
113 109 112 oveq12d 
 |-  ( ( a = y /\ b = z ) -> ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) = ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) )
114 113 oveq2d 
 |-  ( ( a = y /\ b = z ) -> ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = ( t .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) )
115 114 eqeq1d 
 |-  ( ( a = y /\ b = z ) -> ( ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. <-> ( t .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) )
116 115 rexbidv 
 |-  ( ( a = y /\ b = z ) -> ( E. t e. S ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. <-> E. t e. S ( t .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) )
117 oveq1 
 |-  ( t = u -> ( t .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) )
118 117 eqeq1d 
 |-  ( t = u -> ( ( t .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. <-> ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) )
119 118 cbvrexvw 
 |-  ( E. t e. S ( t .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. <-> E. u e. S ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. )
120 116 119 bitrdi 
 |-  ( ( a = y /\ b = z ) -> ( E. t e. S ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. <-> E. u e. S ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) )
121 120 adantl 
 |-  ( ( ph /\ ( a = y /\ b = z ) ) -> ( E. t e. S ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. <-> E. u e. S ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) )
122 18 121 brab2d 
 |-  ( ph -> ( y .~ z <-> ( ( y e. W /\ z e. W ) /\ E. u e. S ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) ) )
123 122 biimpa 
 |-  ( ( ph /\ y .~ z ) -> ( ( y e. W /\ z e. W ) /\ E. u e. S ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) )
124 123 adantlr 
 |-  ( ( ( ph /\ x .~ y ) /\ y .~ z ) -> ( ( y e. W /\ z e. W ) /\ E. u e. S ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) )
125 124 simplrd 
 |-  ( ( ( ph /\ x .~ y ) /\ y .~ z ) -> z e. W )
126 125 ad4antr 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> z e. W )
127 126 6 eleqtrdi 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> z e. ( B X. S ) )
128 1st2nd2 
 |-  ( z e. ( B X. S ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
129 127 128 syl 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
130 101 46 syl 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( 1st ` x ) e. B )
131 xp1st 
 |-  ( z e. ( B X. S ) -> ( 1st ` z ) e. B )
132 131 6 eleq2s 
 |-  ( z e. W -> ( 1st ` z ) e. B )
133 126 132 syl 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( 1st ` z ) e. B )
134 101 59 syl 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( 2nd ` x ) e. S )
135 xp2nd 
 |-  ( z e. ( B X. S ) -> ( 2nd ` z ) e. S )
136 135 6 eleq2s 
 |-  ( z e. W -> ( 2nd ` z ) e. S )
137 126 136 syl 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( 2nd ` z ) e. S )
138 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> t e. S )
139 simplr 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> u e. S )
140 13 4 mgpplusg 
 |-  .x. = ( +g ` ( mulGrp ` R ) )
141 140 submcl 
 |-  ( ( S e. ( SubMnd ` ( mulGrp ` R ) ) /\ t e. S /\ u e. S ) -> ( t .x. u ) e. S )
142 98 138 139 141 syl3anc 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( t .x. u ) e. S )
143 36 ad5antr 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> y e. W )
144 143 51 syl 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( 2nd ` y ) e. S )
145 140 submcl 
 |-  ( ( S e. ( SubMnd ` ( mulGrp ` R ) ) /\ ( t .x. u ) e. S /\ ( 2nd ` y ) e. S ) -> ( ( t .x. u ) .x. ( 2nd ` y ) ) e. S )
146 98 142 144 145 syl3anc 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( t .x. u ) .x. ( 2nd ` y ) ) e. S )
147 40 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> R e. Ring )
148 99 144 sseldd 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( 2nd ` y ) e. B )
149 99 137 sseldd 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( 2nd ` z ) e. B )
150 1 4 147 130 149 ringcld 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( 1st ` x ) .x. ( 2nd ` z ) ) e. B )
151 99 134 sseldd 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( 2nd ` x ) e. B )
152 1 4 147 133 151 ringcld 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( 1st ` z ) .x. ( 2nd ` x ) ) e. B )
153 1 4 5 147 148 150 152 ringsubdi 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( 2nd ` y ) .x. ( ( ( 1st ` x ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` x ) ) ) ) = ( ( ( 2nd ` y ) .x. ( ( 1st ` x ) .x. ( 2nd ` z ) ) ) .- ( ( 2nd ` y ) .x. ( ( 1st ` z ) .x. ( 2nd ` x ) ) ) ) )
154 8 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> R e. CRing )
155 1 4 154 148 130 149 crng12d 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( 2nd ` y ) .x. ( ( 1st ` x ) .x. ( 2nd ` z ) ) ) = ( ( 1st ` x ) .x. ( ( 2nd ` y ) .x. ( 2nd ` z ) ) ) )
156 1 4 154 148 149 crngcomd 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( 2nd ` y ) .x. ( 2nd ` z ) ) = ( ( 2nd ` z ) .x. ( 2nd ` y ) ) )
157 156 oveq2d 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( 1st ` x ) .x. ( ( 2nd ` y ) .x. ( 2nd ` z ) ) ) = ( ( 1st ` x ) .x. ( ( 2nd ` z ) .x. ( 2nd ` y ) ) ) )
158 1 4 154 130 149 148 crng12d 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( 1st ` x ) .x. ( ( 2nd ` z ) .x. ( 2nd ` y ) ) ) = ( ( 2nd ` z ) .x. ( ( 1st ` x ) .x. ( 2nd ` y ) ) ) )
159 155 157 158 3eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( 2nd ` y ) .x. ( ( 1st ` x ) .x. ( 2nd ` z ) ) ) = ( ( 2nd ` z ) .x. ( ( 1st ` x ) .x. ( 2nd ` y ) ) ) )
160 1 4 154 148 133 151 crng12d 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( 2nd ` y ) .x. ( ( 1st ` z ) .x. ( 2nd ` x ) ) ) = ( ( 1st ` z ) .x. ( ( 2nd ` y ) .x. ( 2nd ` x ) ) ) )
161 1 4 154 148 151 crngcomd 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( 2nd ` y ) .x. ( 2nd ` x ) ) = ( ( 2nd ` x ) .x. ( 2nd ` y ) ) )
162 161 oveq2d 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( 1st ` z ) .x. ( ( 2nd ` y ) .x. ( 2nd ` x ) ) ) = ( ( 1st ` z ) .x. ( ( 2nd ` x ) .x. ( 2nd ` y ) ) ) )
163 1 4 154 133 151 148 crng12d 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( 1st ` z ) .x. ( ( 2nd ` x ) .x. ( 2nd ` y ) ) ) = ( ( 2nd ` x ) .x. ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) )
164 160 162 163 3eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( 2nd ` y ) .x. ( ( 1st ` z ) .x. ( 2nd ` x ) ) ) = ( ( 2nd ` x ) .x. ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) )
165 159 164 oveq12d 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( ( 2nd ` y ) .x. ( ( 1st ` x ) .x. ( 2nd ` z ) ) ) .- ( ( 2nd ` y ) .x. ( ( 1st ` z ) .x. ( 2nd ` x ) ) ) ) = ( ( ( 2nd ` z ) .x. ( ( 1st ` x ) .x. ( 2nd ` y ) ) ) .- ( ( 2nd ` x ) .x. ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) )
166 1 4 147 130 148 ringcld 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( 1st ` x ) .x. ( 2nd ` y ) ) e. B )
167 143 56 syl 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( 1st ` y ) e. B )
168 1 4 147 167 151 ringcld 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( 1st ` y ) .x. ( 2nd ` x ) ) e. B )
169 1 4 5 147 149 166 168 ringsubdi 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( 2nd ` z ) .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = ( ( ( 2nd ` z ) .x. ( ( 1st ` x ) .x. ( 2nd ` y ) ) ) .- ( ( 2nd ` z ) .x. ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) )
170 1 4 147 167 149 ringcld 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( 1st ` y ) .x. ( 2nd ` z ) ) e. B )
171 1 4 147 133 148 ringcld 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( 1st ` z ) .x. ( 2nd ` y ) ) e. B )
172 1 4 5 147 151 170 171 ringsubdi 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( 2nd ` x ) .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = ( ( ( 2nd ` x ) .x. ( ( 1st ` y ) .x. ( 2nd ` z ) ) ) .- ( ( 2nd ` x ) .x. ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) )
173 169 172 oveq12d 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( ( 2nd ` z ) .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) ( +g ` R ) ( ( 2nd ` x ) .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) ) = ( ( ( ( 2nd ` z ) .x. ( ( 1st ` x ) .x. ( 2nd ` y ) ) ) .- ( ( 2nd ` z ) .x. ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) ( +g ` R ) ( ( ( 2nd ` x ) .x. ( ( 1st ` y ) .x. ( 2nd ` z ) ) ) .- ( ( 2nd ` x ) .x. ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) ) )
174 1 4 154 167 149 151 crng12d 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( 1st ` y ) .x. ( ( 2nd ` z ) .x. ( 2nd ` x ) ) ) = ( ( 2nd ` z ) .x. ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) )
175 174 oveq2d 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( ( 2nd ` z ) .x. ( ( 1st ` x ) .x. ( 2nd ` y ) ) ) .- ( ( 1st ` y ) .x. ( ( 2nd ` z ) .x. ( 2nd ` x ) ) ) ) = ( ( ( 2nd ` z ) .x. ( ( 1st ` x ) .x. ( 2nd ` y ) ) ) .- ( ( 2nd ` z ) .x. ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) )
176 1 4 154 149 151 crngcomd 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( 2nd ` z ) .x. ( 2nd ` x ) ) = ( ( 2nd ` x ) .x. ( 2nd ` z ) ) )
177 176 oveq2d 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( 1st ` y ) .x. ( ( 2nd ` z ) .x. ( 2nd ` x ) ) ) = ( ( 1st ` y ) .x. ( ( 2nd ` x ) .x. ( 2nd ` z ) ) ) )
178 1 4 154 151 167 149 crng12d 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( 2nd ` x ) .x. ( ( 1st ` y ) .x. ( 2nd ` z ) ) ) = ( ( 1st ` y ) .x. ( ( 2nd ` x ) .x. ( 2nd ` z ) ) ) )
179 177 178 eqtr4d 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( 1st ` y ) .x. ( ( 2nd ` z ) .x. ( 2nd ` x ) ) ) = ( ( 2nd ` x ) .x. ( ( 1st ` y ) .x. ( 2nd ` z ) ) ) )
180 179 oveq1d 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( ( 1st ` y ) .x. ( ( 2nd ` z ) .x. ( 2nd ` x ) ) ) .- ( ( 2nd ` x ) .x. ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = ( ( ( 2nd ` x ) .x. ( ( 1st ` y ) .x. ( 2nd ` z ) ) ) .- ( ( 2nd ` x ) .x. ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) )
181 175 180 oveq12d 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( ( ( 2nd ` z ) .x. ( ( 1st ` x ) .x. ( 2nd ` y ) ) ) .- ( ( 1st ` y ) .x. ( ( 2nd ` z ) .x. ( 2nd ` x ) ) ) ) ( +g ` R ) ( ( ( 1st ` y ) .x. ( ( 2nd ` z ) .x. ( 2nd ` x ) ) ) .- ( ( 2nd ` x ) .x. ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) ) = ( ( ( ( 2nd ` z ) .x. ( ( 1st ` x ) .x. ( 2nd ` y ) ) ) .- ( ( 2nd ` z ) .x. ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) ( +g ` R ) ( ( ( 2nd ` x ) .x. ( ( 1st ` y ) .x. ( 2nd ` z ) ) ) .- ( ( 2nd ` x ) .x. ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) ) )
182 41 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> R e. Grp )
183 1 4 147 149 166 ringcld 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( 2nd ` z ) .x. ( ( 1st ` x ) .x. ( 2nd ` y ) ) ) e. B )
184 1 4 147 149 151 ringcld 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( 2nd ` z ) .x. ( 2nd ` x ) ) e. B )
185 1 4 147 167 184 ringcld 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( 1st ` y ) .x. ( ( 2nd ` z ) .x. ( 2nd ` x ) ) ) e. B )
186 1 4 147 151 171 ringcld 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( 2nd ` x ) .x. ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) e. B )
187 eqid 
 |-  ( +g ` R ) = ( +g ` R )
188 1 187 5 grpnpncan 
 |-  ( ( R e. Grp /\ ( ( ( 2nd ` z ) .x. ( ( 1st ` x ) .x. ( 2nd ` y ) ) ) e. B /\ ( ( 1st ` y ) .x. ( ( 2nd ` z ) .x. ( 2nd ` x ) ) ) e. B /\ ( ( 2nd ` x ) .x. ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) e. B ) ) -> ( ( ( ( 2nd ` z ) .x. ( ( 1st ` x ) .x. ( 2nd ` y ) ) ) .- ( ( 1st ` y ) .x. ( ( 2nd ` z ) .x. ( 2nd ` x ) ) ) ) ( +g ` R ) ( ( ( 1st ` y ) .x. ( ( 2nd ` z ) .x. ( 2nd ` x ) ) ) .- ( ( 2nd ` x ) .x. ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) ) = ( ( ( 2nd ` z ) .x. ( ( 1st ` x ) .x. ( 2nd ` y ) ) ) .- ( ( 2nd ` x ) .x. ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) )
189 182 183 185 186 188 syl13anc 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( ( ( 2nd ` z ) .x. ( ( 1st ` x ) .x. ( 2nd ` y ) ) ) .- ( ( 1st ` y ) .x. ( ( 2nd ` z ) .x. ( 2nd ` x ) ) ) ) ( +g ` R ) ( ( ( 1st ` y ) .x. ( ( 2nd ` z ) .x. ( 2nd ` x ) ) ) .- ( ( 2nd ` x ) .x. ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) ) = ( ( ( 2nd ` z ) .x. ( ( 1st ` x ) .x. ( 2nd ` y ) ) ) .- ( ( 2nd ` x ) .x. ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) )
190 173 181 189 3eqtr2rd 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( ( 2nd ` z ) .x. ( ( 1st ` x ) .x. ( 2nd ` y ) ) ) .- ( ( 2nd ` x ) .x. ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = ( ( ( 2nd ` z ) .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) ( +g ` R ) ( ( 2nd ` x ) .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) ) )
191 153 165 190 3eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( 2nd ` y ) .x. ( ( ( 1st ` x ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` x ) ) ) ) = ( ( ( 2nd ` z ) .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) ( +g ` R ) ( ( 2nd ` x ) .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) ) )
192 191 oveq2d 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( t .x. u ) .x. ( ( 2nd ` y ) .x. ( ( ( 1st ` x ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` x ) ) ) ) ) = ( ( t .x. u ) .x. ( ( ( 2nd ` z ) .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) ( +g ` R ) ( ( 2nd ` x ) .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) ) ) )
193 99 142 sseldd 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( t .x. u ) e. B )
194 1 5 grpsubcl 
 |-  ( ( R e. Grp /\ ( ( 1st ` x ) .x. ( 2nd ` z ) ) e. B /\ ( ( 1st ` z ) .x. ( 2nd ` x ) ) e. B ) -> ( ( ( 1st ` x ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` x ) ) ) e. B )
195 182 150 152 194 syl3anc 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( ( 1st ` x ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` x ) ) ) e. B )
196 1 4 147 193 148 195 ringassd 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( ( t .x. u ) .x. ( 2nd ` y ) ) .x. ( ( ( 1st ` x ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` x ) ) ) ) = ( ( t .x. u ) .x. ( ( 2nd ` y ) .x. ( ( ( 1st ` x ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` x ) ) ) ) ) )
197 99 139 sseldd 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> u e. B )
198 99 138 sseldd 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> t e. B )
199 1 4 154 197 149 198 cringmul32d 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( u .x. ( 2nd ` z ) ) .x. t ) = ( ( u .x. t ) .x. ( 2nd ` z ) ) )
200 1 4 154 197 198 crngcomd 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( u .x. t ) = ( t .x. u ) )
201 200 oveq1d 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( u .x. t ) .x. ( 2nd ` z ) ) = ( ( t .x. u ) .x. ( 2nd ` z ) ) )
202 199 201 eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( u .x. ( 2nd ` z ) ) .x. t ) = ( ( t .x. u ) .x. ( 2nd ` z ) ) )
203 202 oveq1d 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( ( u .x. ( 2nd ` z ) ) .x. t ) .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = ( ( ( t .x. u ) .x. ( 2nd ` z ) ) .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) )
204 1 4 147 197 149 ringcld 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( u .x. ( 2nd ` z ) ) e. B )
205 182 166 168 69 syl3anc 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) e. B )
206 1 4 147 204 198 205 ringassd 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( ( u .x. ( 2nd ` z ) ) .x. t ) .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = ( ( u .x. ( 2nd ` z ) ) .x. ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) ) )
207 1 4 147 193 149 205 ringassd 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( ( t .x. u ) .x. ( 2nd ` z ) ) .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = ( ( t .x. u ) .x. ( ( 2nd ` z ) .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) ) )
208 203 206 207 3eqtr3d 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( u .x. ( 2nd ` z ) ) .x. ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) ) = ( ( t .x. u ) .x. ( ( 2nd ` z ) .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) ) )
209 1 4 154 198 151 197 cringmul32d 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( t .x. ( 2nd ` x ) ) .x. u ) = ( ( t .x. u ) .x. ( 2nd ` x ) ) )
210 209 oveq1d 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( ( t .x. ( 2nd ` x ) ) .x. u ) .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = ( ( ( t .x. u ) .x. ( 2nd ` x ) ) .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) )
211 1 4 147 198 151 ringcld 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( t .x. ( 2nd ` x ) ) e. B )
212 1 5 grpsubcl 
 |-  ( ( R e. Grp /\ ( ( 1st ` y ) .x. ( 2nd ` z ) ) e. B /\ ( ( 1st ` z ) .x. ( 2nd ` y ) ) e. B ) -> ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) e. B )
213 182 170 171 212 syl3anc 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) e. B )
214 1 4 147 211 197 213 ringassd 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( ( t .x. ( 2nd ` x ) ) .x. u ) .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = ( ( t .x. ( 2nd ` x ) ) .x. ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) ) )
215 1 4 147 193 151 213 ringassd 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( ( t .x. u ) .x. ( 2nd ` x ) ) .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = ( ( t .x. u ) .x. ( ( 2nd ` x ) .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) ) )
216 210 214 215 3eqtr3d 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( t .x. ( 2nd ` x ) ) .x. ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) ) = ( ( t .x. u ) .x. ( ( 2nd ` x ) .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) ) )
217 208 216 oveq12d 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( ( u .x. ( 2nd ` z ) ) .x. ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) ) ( +g ` R ) ( ( t .x. ( 2nd ` x ) ) .x. ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) ) ) = ( ( ( t .x. u ) .x. ( ( 2nd ` z ) .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) ) ( +g ` R ) ( ( t .x. u ) .x. ( ( 2nd ` x ) .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) ) ) )
218 1 4 147 149 205 ringcld 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( 2nd ` z ) .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) e. B )
219 1 4 147 151 213 ringcld 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( 2nd ` x ) .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) e. B )
220 1 187 4 ringdi 
 |-  ( ( R e. Ring /\ ( ( t .x. u ) e. B /\ ( ( 2nd ` z ) .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) e. B /\ ( ( 2nd ` x ) .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) e. B ) ) -> ( ( t .x. u ) .x. ( ( ( 2nd ` z ) .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) ( +g ` R ) ( ( 2nd ` x ) .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) ) ) = ( ( ( t .x. u ) .x. ( ( 2nd ` z ) .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) ) ( +g ` R ) ( ( t .x. u ) .x. ( ( 2nd ` x ) .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) ) ) )
221 147 193 218 219 220 syl13anc 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( t .x. u ) .x. ( ( ( 2nd ` z ) .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) ( +g ` R ) ( ( 2nd ` x ) .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) ) ) = ( ( ( t .x. u ) .x. ( ( 2nd ` z ) .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) ) ( +g ` R ) ( ( t .x. u ) .x. ( ( 2nd ` x ) .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) ) ) )
222 217 221 eqtr4d 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( ( u .x. ( 2nd ` z ) ) .x. ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) ) ( +g ` R ) ( ( t .x. ( 2nd ` x ) ) .x. ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) ) ) = ( ( t .x. u ) .x. ( ( ( 2nd ` z ) .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) ( +g ` R ) ( ( 2nd ` x ) .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) ) ) )
223 192 196 222 3eqtr4d 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( ( t .x. u ) .x. ( 2nd ` y ) ) .x. ( ( ( 1st ` x ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` x ) ) ) ) = ( ( ( u .x. ( 2nd ` z ) ) .x. ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) ) ( +g ` R ) ( ( t .x. ( 2nd ` x ) ) .x. ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) ) ) )
224 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. )
225 224 oveq2d 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( u .x. ( 2nd ` z ) ) .x. ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) ) = ( ( u .x. ( 2nd ` z ) ) .x. .0. ) )
226 1 4 2 147 204 ringrzd 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( u .x. ( 2nd ` z ) ) .x. .0. ) = .0. )
227 225 226 eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( u .x. ( 2nd ` z ) ) .x. ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) ) = .0. )
228 simpr 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. )
229 228 oveq2d 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( t .x. ( 2nd ` x ) ) .x. ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) ) = ( ( t .x. ( 2nd ` x ) ) .x. .0. ) )
230 1 4 2 147 211 ringrzd 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( t .x. ( 2nd ` x ) ) .x. .0. ) = .0. )
231 229 230 eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( t .x. ( 2nd ` x ) ) .x. ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) ) = .0. )
232 227 231 oveq12d 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( ( u .x. ( 2nd ` z ) ) .x. ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) ) ( +g ` R ) ( ( t .x. ( 2nd ` x ) ) .x. ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) ) ) = ( .0. ( +g ` R ) .0. ) )
233 1 2 grpidcl 
 |-  ( R e. Grp -> .0. e. B )
234 182 233 syl 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> .0. e. B )
235 1 187 2 182 234 grplidd 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( .0. ( +g ` R ) .0. ) = .0. )
236 223 232 235 3eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> ( ( ( t .x. u ) .x. ( 2nd ` y ) ) .x. ( ( ( 1st ` x ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` x ) ) ) ) = .0. )
237 1 7 99 2 4 5 104 129 130 133 134 137 146 236 erlbrd 
 |-  ( ( ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) /\ u e. S ) /\ ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. ) -> x .~ z )
238 124 simprd 
 |-  ( ( ( ph /\ x .~ y ) /\ y .~ z ) -> E. u e. S ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. )
239 238 ad2antrr 
 |-  ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) -> E. u e. S ( u .x. ( ( ( 1st ` y ) .x. ( 2nd ` z ) ) .- ( ( 1st ` z ) .x. ( 2nd ` y ) ) ) ) = .0. )
240 237 239 r19.29a 
 |-  ( ( ( ( ( ph /\ x .~ y ) /\ y .~ z ) /\ t e. S ) /\ ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. ) -> x .~ z )
241 39 adantr 
 |-  ( ( ( ph /\ x .~ y ) /\ y .~ z ) -> E. t e. S ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` y ) ) .- ( ( 1st ` y ) .x. ( 2nd ` x ) ) ) ) = .0. )
242 240 241 r19.29a 
 |-  ( ( ( ph /\ x .~ y ) /\ y .~ z ) -> x .~ z )
243 242 anasss 
 |-  ( ( ph /\ ( x .~ y /\ y .~ z ) ) -> x .~ z )
244 13 3 ringidval 
 |-  .1. = ( 0g ` ( mulGrp ` R ) )
245 244 subm0cl 
 |-  ( S e. ( SubMnd ` ( mulGrp ` R ) ) -> .1. e. S )
246 9 245 syl 
 |-  ( ph -> .1. e. S )
247 246 adantr 
 |-  ( ( ph /\ x e. W ) -> .1. e. S )
248 oveq1 
 |-  ( t = .1. -> ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` x ) ) ) ) = ( .1. .x. ( ( ( 1st ` x ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` x ) ) ) ) )
249 248 eqeq1d 
 |-  ( t = .1. -> ( ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` x ) ) ) ) = .0. <-> ( .1. .x. ( ( ( 1st ` x ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` x ) ) ) ) = .0. ) )
250 249 adantl 
 |-  ( ( ( ph /\ x e. W ) /\ t = .1. ) -> ( ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` x ) ) ) ) = .0. <-> ( .1. .x. ( ( ( 1st ` x ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` x ) ) ) ) = .0. ) )
251 40 adantr 
 |-  ( ( ph /\ x e. W ) -> R e. Ring )
252 46 adantl 
 |-  ( ( ph /\ x e. W ) -> ( 1st ` x ) e. B )
253 16 adantr 
 |-  ( ( ph /\ x e. W ) -> S C_ B )
254 59 adantl 
 |-  ( ( ph /\ x e. W ) -> ( 2nd ` x ) e. S )
255 253 254 sseldd 
 |-  ( ( ph /\ x e. W ) -> ( 2nd ` x ) e. B )
256 1 4 251 252 255 ringcld 
 |-  ( ( ph /\ x e. W ) -> ( ( 1st ` x ) .x. ( 2nd ` x ) ) e. B )
257 1 2 5 grpsubid 
 |-  ( ( R e. Grp /\ ( ( 1st ` x ) .x. ( 2nd ` x ) ) e. B ) -> ( ( ( 1st ` x ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` x ) ) ) = .0. )
258 41 256 257 syl2an2r 
 |-  ( ( ph /\ x e. W ) -> ( ( ( 1st ` x ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` x ) ) ) = .0. )
259 258 oveq2d 
 |-  ( ( ph /\ x e. W ) -> ( .1. .x. ( ( ( 1st ` x ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` x ) ) ) ) = ( .1. .x. .0. ) )
260 41 233 syl 
 |-  ( ph -> .0. e. B )
261 1 4 3 40 260 ringlidmd 
 |-  ( ph -> ( .1. .x. .0. ) = .0. )
262 261 adantr 
 |-  ( ( ph /\ x e. W ) -> ( .1. .x. .0. ) = .0. )
263 259 262 eqtrd 
 |-  ( ( ph /\ x e. W ) -> ( .1. .x. ( ( ( 1st ` x ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` x ) ) ) ) = .0. )
264 247 250 263 rspcedvd 
 |-  ( ( ph /\ x e. W ) -> E. t e. S ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` x ) ) ) ) = .0. )
265 264 ex 
 |-  ( ph -> ( x e. W -> E. t e. S ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` x ) ) ) ) = .0. ) )
266 265 pm4.71d 
 |-  ( ph -> ( x e. W <-> ( x e. W /\ E. t e. S ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` x ) ) ) ) = .0. ) ) )
267 pm4.24 
 |-  ( x e. W <-> ( x e. W /\ x e. W ) )
268 267 anbi1i 
 |-  ( ( x e. W /\ E. t e. S ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` x ) ) ) ) = .0. ) <-> ( ( x e. W /\ x e. W ) /\ E. t e. S ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` x ) ) ) ) = .0. ) )
269 266 268 bitrdi 
 |-  ( ph -> ( x e. W <-> ( ( x e. W /\ x e. W ) /\ E. t e. S ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` x ) ) ) ) = .0. ) ) )
270 simpl 
 |-  ( ( a = x /\ b = x ) -> a = x )
271 270 fveq2d 
 |-  ( ( a = x /\ b = x ) -> ( 1st ` a ) = ( 1st ` x ) )
272 simpr 
 |-  ( ( a = x /\ b = x ) -> b = x )
273 272 fveq2d 
 |-  ( ( a = x /\ b = x ) -> ( 2nd ` b ) = ( 2nd ` x ) )
274 271 273 oveq12d 
 |-  ( ( a = x /\ b = x ) -> ( ( 1st ` a ) .x. ( 2nd ` b ) ) = ( ( 1st ` x ) .x. ( 2nd ` x ) ) )
275 272 fveq2d 
 |-  ( ( a = x /\ b = x ) -> ( 1st ` b ) = ( 1st ` x ) )
276 270 fveq2d 
 |-  ( ( a = x /\ b = x ) -> ( 2nd ` a ) = ( 2nd ` x ) )
277 275 276 oveq12d 
 |-  ( ( a = x /\ b = x ) -> ( ( 1st ` b ) .x. ( 2nd ` a ) ) = ( ( 1st ` x ) .x. ( 2nd ` x ) ) )
278 274 277 oveq12d 
 |-  ( ( a = x /\ b = x ) -> ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) = ( ( ( 1st ` x ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` x ) ) ) )
279 278 oveq2d 
 |-  ( ( a = x /\ b = x ) -> ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` x ) ) ) ) )
280 279 eqeq1d 
 |-  ( ( a = x /\ b = x ) -> ( ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. <-> ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` x ) ) ) ) = .0. ) )
281 280 rexbidv 
 |-  ( ( a = x /\ b = x ) -> ( E. t e. S ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. <-> E. t e. S ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` x ) ) ) ) = .0. ) )
282 281 adantl 
 |-  ( ( ph /\ ( a = x /\ b = x ) ) -> ( E. t e. S ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. <-> E. t e. S ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` x ) ) ) ) = .0. ) )
283 18 282 brab2d 
 |-  ( ph -> ( x .~ x <-> ( ( x e. W /\ x e. W ) /\ E. t e. S ( t .x. ( ( ( 1st ` x ) .x. ( 2nd ` x ) ) .- ( ( 1st ` x ) .x. ( 2nd ` x ) ) ) ) = .0. ) ) )
284 269 283 bitr4d 
 |-  ( ph -> ( x e. W <-> x .~ x ) )
285 20 97 243 284 iserd 
 |-  ( ph -> .~ Er W )