rloccring

Description: The ring localization L of a commutative ring R by a multiplicatively closed set S is itself a commutative ring. (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 ) ) )
Assertion	rloccring	\|- ( ph -> L e. CRing )

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		eqid	\|- ( 0g ` R ) = ( 0g ` R )
9		eqid	\|- ( -g ` R ) = ( -g ` R )
10		eqid	\|- ( B X. S ) = ( B X. S )
11		eqid	\|- ( mulGrp ` R ) = ( mulGrp ` R )
12	11 1	mgpbas	\|- B = ( Base ` ( mulGrp ` R ) )
13	12	submss	\|- ( S e. ( SubMnd ` ( mulGrp ` R ) ) -> S C_ B )
14	7 13	syl	\|- ( ph -> S C_ B )
15	1 8 2 9 10 4 5 6 14	rlocbas	\|- ( ph -> ( ( B X. S ) /. .~ ) = ( Base ` L ) )
16		eqidd	\|- ( ph -> ( +g ` L ) = ( +g ` L ) )
17		eqidd	\|- ( ph -> ( .r ` L ) = ( .r ` L ) )
18		eqid	\|- ( Base ` L ) = ( Base ` L )
19		eqid	\|- ( 0g ` L ) = ( 0g ` L )
20		eqid	\|- ( +g ` L ) = ( +g ` L )
21	6	crngringd	\|- ( ph -> R e. Ring )
22	1 8	ring0cl	\|- ( R e. Ring -> ( 0g ` R ) e. B )
23	21 22	syl	\|- ( ph -> ( 0g ` R ) e. B )
24		eqid	\|- ( 1r ` R ) = ( 1r ` R )
25	11 24	ringidval	\|- ( 1r ` R ) = ( 0g ` ( mulGrp ` R ) )
26	25	subm0cl	\|- ( S e. ( SubMnd ` ( mulGrp ` R ) ) -> ( 1r ` R ) e. S )
27	7 26	syl	\|- ( ph -> ( 1r ` R ) e. S )
28	23 27	opelxpd	\|- ( ph -> <. ( 0g ` R ) , ( 1r ` R ) >. e. ( B X. S ) )
29	5	ovexi	\|- .~ e. _V
30	29	ecelqsi	\|- ( <. ( 0g ` R ) , ( 1r ` R ) >. e. ( B X. S ) -> [ <. ( 0g ` R ) , ( 1r ` R ) >. ] .~ e. ( ( B X. S ) /. .~ ) )
31	28 30	syl	\|- ( ph -> [ <. ( 0g ` R ) , ( 1r ` R ) >. ] .~ e. ( ( B X. S ) /. .~ ) )
32	31 15	eleqtrd	\|- ( ph -> [ <. ( 0g ` R ) , ( 1r ` R ) >. ] .~ e. ( Base ` L ) )
33	15	eleq2d	\|- ( ph -> ( x e. ( ( B X. S ) /. .~ ) <-> x e. ( Base ` L ) ) )
34	33	biimpar	\|- ( ( ph /\ x e. ( Base ` L ) ) -> x e. ( ( B X. S ) /. .~ ) )
35		simpr	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> x = [ <. a , b >. ] .~ )
36	35	oveq2d	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( [ <. ( 0g ` R ) , ( 1r ` R ) >. ] .~ ( +g ` L ) x ) = ( [ <. ( 0g ` R ) , ( 1r ` R ) >. ] .~ ( +g ` L ) [ <. a , b >. ] .~ ) )
37	21	ad4antr	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> R e. Ring )
38	7	ad4antr	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> S e. ( SubMnd ` ( mulGrp ` R ) ) )
39	38 13	syl	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> S C_ B )
40		simplr	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> b e. S )
41	39 40	sseldd	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> b e. B )
42	1 2 8 37 41	ringlzd	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( ( 0g ` R ) .x. b ) = ( 0g ` R ) )
43		simpllr	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> a e. B )
44	1 2 24 37 43	ringridmd	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( a .x. ( 1r ` R ) ) = a )
45	42 44	oveq12d	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( ( ( 0g ` R ) .x. b ) ( +g ` R ) ( a .x. ( 1r ` R ) ) ) = ( ( 0g ` R ) ( +g ` R ) a ) )
46		eqid	\|- ( +g ` R ) = ( +g ` R )
47	37	ringgrpd	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> R e. Grp )
48	1 46 8 47 43	grplidd	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( ( 0g ` R ) ( +g ` R ) a ) = a )
49	45 48	eqtrd	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( ( ( 0g ` R ) .x. b ) ( +g ` R ) ( a .x. ( 1r ` R ) ) ) = a )
50	1 2 24 37 41	ringlidmd	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( ( 1r ` R ) .x. b ) = b )
51	49 50	opeq12d	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> <. ( ( ( 0g ` R ) .x. b ) ( +g ` R ) ( a .x. ( 1r ` R ) ) ) , ( ( 1r ` R ) .x. b ) >. = <. a , b >. )
52	51	eceq1d	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> [ <. ( ( ( 0g ` R ) .x. b ) ( +g ` R ) ( a .x. ( 1r ` R ) ) ) , ( ( 1r ` R ) .x. b ) >. ] .~ = [ <. a , b >. ] .~ )
53	6	ad4antr	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> R e. CRing )
54	23	ad4antr	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( 0g ` R ) e. B )
55	38 26	syl	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( 1r ` R ) e. S )
56	1 2 46 4 5 53 38 54 43 55 40 20	rlocaddval	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( [ <. ( 0g ` R ) , ( 1r ` R ) >. ] .~ ( +g ` L ) [ <. a , b >. ] .~ ) = [ <. ( ( ( 0g ` R ) .x. b ) ( +g ` R ) ( a .x. ( 1r ` R ) ) ) , ( ( 1r ` R ) .x. b ) >. ] .~ )
57	52 56 35	3eqtr4d	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( [ <. ( 0g ` R ) , ( 1r ` R ) >. ] .~ ( +g ` L ) [ <. a , b >. ] .~ ) = x )
58	36 57	eqtrd	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( [ <. ( 0g ` R ) , ( 1r ` R ) >. ] .~ ( +g ` L ) x ) = x )
59		simpr	\|- ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) -> x e. ( ( B X. S ) /. .~ ) )
60	59	elrlocbasi	\|- ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) -> E. a e. B E. b e. S x = [ <. a , b >. ] .~ )
61	58 60	r19.29vva	\|- ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) -> ( [ <. ( 0g ` R ) , ( 1r ` R ) >. ] .~ ( +g ` L ) x ) = x )
62	34 61	syldan	\|- ( ( ph /\ x e. ( Base ` L ) ) -> ( [ <. ( 0g ` R ) , ( 1r ` R ) >. ] .~ ( +g ` L ) x ) = x )
63	1 2 3 4 5 53 38 43 54 40 55 20	rlocaddval	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( [ <. a , b >. ] .~ ( +g ` L ) [ <. ( 0g ` R ) , ( 1r ` R ) >. ] .~ ) = [ <. ( ( a .x. ( 1r ` R ) ) .+ ( ( 0g ` R ) .x. b ) ) , ( b .x. ( 1r ` R ) ) >. ] .~ )
64	35	oveq1d	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( x ( +g ` L ) [ <. ( 0g ` R ) , ( 1r ` R ) >. ] .~ ) = ( [ <. a , b >. ] .~ ( +g ` L ) [ <. ( 0g ` R ) , ( 1r ` R ) >. ] .~ ) )
65	44 42	oveq12d	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( ( a .x. ( 1r ` R ) ) .+ ( ( 0g ` R ) .x. b ) ) = ( a .+ ( 0g ` R ) ) )
66	1 3 8 47 43	grpridd	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( a .+ ( 0g ` R ) ) = a )
67	65 66	eqtr2d	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> a = ( ( a .x. ( 1r ` R ) ) .+ ( ( 0g ` R ) .x. b ) ) )
68	1 2 24 37 41	ringridmd	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( b .x. ( 1r ` R ) ) = b )
69	68	eqcomd	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> b = ( b .x. ( 1r ` R ) ) )
70	67 69	opeq12d	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> <. a , b >. = <. ( ( a .x. ( 1r ` R ) ) .+ ( ( 0g ` R ) .x. b ) ) , ( b .x. ( 1r ` R ) ) >. )
71	70	eceq1d	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> [ <. a , b >. ] .~ = [ <. ( ( a .x. ( 1r ` R ) ) .+ ( ( 0g ` R ) .x. b ) ) , ( b .x. ( 1r ` R ) ) >. ] .~ )
72	35 71	eqtrd	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> x = [ <. ( ( a .x. ( 1r ` R ) ) .+ ( ( 0g ` R ) .x. b ) ) , ( b .x. ( 1r ` R ) ) >. ] .~ )
73	63 64 72	3eqtr4d	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( x ( +g ` L ) [ <. ( 0g ` R ) , ( 1r ` R ) >. ] .~ ) = x )
74	73 60	r19.29vva	\|- ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) -> ( x ( +g ` L ) [ <. ( 0g ` R ) , ( 1r ` R ) >. ] .~ ) = x )
75	34 74	syldan	\|- ( ( ph /\ x e. ( Base ` L ) ) -> ( x ( +g ` L ) [ <. ( 0g ` R ) , ( 1r ` R ) >. ] .~ ) = x )
76	18 19 20 32 62 75	ismgmid2	\|- ( ph -> [ <. ( 0g ` R ) , ( 1r ` R ) >. ] .~ = ( 0g ` L ) )
77		simp-4r	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> x = [ <. a , b >. ] .~ )
78		simpr	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> y = [ <. c , d >. ] .~ )
79	77 78	oveq12d	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> ( x ( +g ` L ) y ) = ( [ <. a , b >. ] .~ ( +g ` L ) [ <. c , d >. ] .~ ) )
80	6	ad8antr	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> R e. CRing )
81	7	ad8antr	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> S e. ( SubMnd ` ( mulGrp ` R ) ) )
82		simp-6r	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> a e. B )
83		simpllr	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> c e. B )
84		simp-5r	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> b e. S )
85		simplr	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> d e. S )
86	1 2 3 4 5 80 81 82 83 84 85 20	rlocaddval	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> ( [ <. a , b >. ] .~ ( +g ` L ) [ <. c , d >. ] .~ ) = [ <. ( ( a .x. d ) .+ ( c .x. b ) ) , ( b .x. d ) >. ] .~ )
87	80	crnggrpd	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> R e. Grp )
88	21	ad8antr	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> R e. Ring )
89	81 13	syl	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> S C_ B )
90	89 85	sseldd	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> d e. B )
91	1 2 88 82 90	ringcld	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> ( a .x. d ) e. B )
92	89 84	sseldd	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> b e. B )
93	1 2 88 83 92	ringcld	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> ( c .x. b ) e. B )
94	1 3 87 91 93	grpcld	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> ( ( a .x. d ) .+ ( c .x. b ) ) e. B )
95	11 2	mgpplusg	\|- .x. = ( +g ` ( mulGrp ` R ) )
96	95 81 84 85	submcld	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> ( b .x. d ) e. S )
97	94 96	opelxpd	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> <. ( ( a .x. d ) .+ ( c .x. b ) ) , ( b .x. d ) >. e. ( B X. S ) )
98	29	ecelqsi	\|- ( <. ( ( a .x. d ) .+ ( c .x. b ) ) , ( b .x. d ) >. e. ( B X. S ) -> [ <. ( ( a .x. d ) .+ ( c .x. b ) ) , ( b .x. d ) >. ] .~ e. ( ( B X. S ) /. .~ ) )
99	97 98	syl	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> [ <. ( ( a .x. d ) .+ ( c .x. b ) ) , ( b .x. d ) >. ] .~ e. ( ( B X. S ) /. .~ ) )
100	86 99	eqeltrd	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> ( [ <. a , b >. ] .~ ( +g ` L ) [ <. c , d >. ] .~ ) e. ( ( B X. S ) /. .~ ) )
101	79 100	eqeltrd	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> ( x ( +g ` L ) y ) e. ( ( B X. S ) /. .~ ) )
102		simp-4r	\|- ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> y e. ( ( B X. S ) /. .~ ) )
103	102	elrlocbasi	\|- ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> E. c e. B E. d e. S y = [ <. c , d >. ] .~ )
104	101 103	r19.29vva	\|- ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( x ( +g ` L ) y ) e. ( ( B X. S ) /. .~ ) )
105		simplr	\|- ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) -> x e. ( ( B X. S ) /. .~ ) )
106	105	elrlocbasi	\|- ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) -> E. a e. B E. b e. S x = [ <. a , b >. ] .~ )
107	104 106	r19.29vva	\|- ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) -> ( x ( +g ` L ) y ) e. ( ( B X. S ) /. .~ ) )
108	107	3impa	\|- ( ( ph /\ x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) ) -> ( x ( +g ` L ) y ) e. ( ( B X. S ) /. .~ ) )
109	6	ad10antr	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> R e. CRing )
110	109	crnggrpd	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> R e. Grp )
111	21	ad10antr	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> R e. Ring )
112		simp-9r	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> a e. B )
113	7	ad10antr	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> S e. ( SubMnd ` ( mulGrp ` R ) ) )
114	113 13	syl	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> S C_ B )
115		simp-5r	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> d e. S )
116	114 115	sseldd	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> d e. B )
117	1 2 111 112 116	ringcld	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( a .x. d ) e. B )
118		simplr	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> f e. S )
119	114 118	sseldd	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> f e. B )
120	1 2 111 117 119	ringcld	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( a .x. d ) .x. f ) e. B )
121		simp-6r	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> c e. B )
122		simp-8r	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> b e. S )
123	114 122	sseldd	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> b e. B )
124	1 2 111 121 123	ringcld	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( c .x. b ) e. B )
125	1 2 111 124 119	ringcld	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( c .x. b ) .x. f ) e. B )
126		simpllr	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> e e. B )
127	1 2 111 123 116	ringcld	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( b .x. d ) e. B )
128	1 2 111 126 127	ringcld	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( e .x. ( b .x. d ) ) e. B )
129	1 3 110 120 125 128	grpassd	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( ( ( a .x. d ) .x. f ) .+ ( ( c .x. b ) .x. f ) ) .+ ( e .x. ( b .x. d ) ) ) = ( ( ( a .x. d ) .x. f ) .+ ( ( ( c .x. b ) .x. f ) .+ ( e .x. ( b .x. d ) ) ) ) )
130	1 2 111 112 116 119	ringassd	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( a .x. d ) .x. f ) = ( a .x. ( d .x. f ) ) )
131	1 2 109 121 123 119	crng32d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( c .x. b ) .x. f ) = ( ( c .x. f ) .x. b ) )
132	1 2 109 126 123 116	crng12d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( e .x. ( b .x. d ) ) = ( b .x. ( e .x. d ) ) )
133	1 2 111 126 116	ringcld	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( e .x. d ) e. B )
134	1 2 109 123 133	crngcomd	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( b .x. ( e .x. d ) ) = ( ( e .x. d ) .x. b ) )
135	132 134	eqtrd	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( e .x. ( b .x. d ) ) = ( ( e .x. d ) .x. b ) )
136	131 135	oveq12d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( ( c .x. b ) .x. f ) .+ ( e .x. ( b .x. d ) ) ) = ( ( ( c .x. f ) .x. b ) .+ ( ( e .x. d ) .x. b ) ) )
137	130 136	oveq12d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( ( a .x. d ) .x. f ) .+ ( ( ( c .x. b ) .x. f ) .+ ( e .x. ( b .x. d ) ) ) ) = ( ( a .x. ( d .x. f ) ) .+ ( ( ( c .x. f ) .x. b ) .+ ( ( e .x. d ) .x. b ) ) ) )
138	129 137	eqtrd	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( ( ( a .x. d ) .x. f ) .+ ( ( c .x. b ) .x. f ) ) .+ ( e .x. ( b .x. d ) ) ) = ( ( a .x. ( d .x. f ) ) .+ ( ( ( c .x. f ) .x. b ) .+ ( ( e .x. d ) .x. b ) ) ) )
139	1 3 2 111 117 124 119	ringdird	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( ( a .x. d ) .+ ( c .x. b ) ) .x. f ) = ( ( ( a .x. d ) .x. f ) .+ ( ( c .x. b ) .x. f ) ) )
140	139	oveq1d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( ( ( a .x. d ) .+ ( c .x. b ) ) .x. f ) .+ ( e .x. ( b .x. d ) ) ) = ( ( ( ( a .x. d ) .x. f ) .+ ( ( c .x. b ) .x. f ) ) .+ ( e .x. ( b .x. d ) ) ) )
141	1 2 111 121 119	ringcld	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( c .x. f ) e. B )
142	1 3 2 111 141 133 123	ringdird	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( ( c .x. f ) .+ ( e .x. d ) ) .x. b ) = ( ( ( c .x. f ) .x. b ) .+ ( ( e .x. d ) .x. b ) ) )
143	142	oveq2d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( a .x. ( d .x. f ) ) .+ ( ( ( c .x. f ) .+ ( e .x. d ) ) .x. b ) ) = ( ( a .x. ( d .x. f ) ) .+ ( ( ( c .x. f ) .x. b ) .+ ( ( e .x. d ) .x. b ) ) ) )
144	138 140 143	3eqtr4d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( ( ( a .x. d ) .+ ( c .x. b ) ) .x. f ) .+ ( e .x. ( b .x. d ) ) ) = ( ( a .x. ( d .x. f ) ) .+ ( ( ( c .x. f ) .+ ( e .x. d ) ) .x. b ) ) )
145	1 2 111 123 116 119	ringassd	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( b .x. d ) .x. f ) = ( b .x. ( d .x. f ) ) )
146	144 145	opeq12d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> <. ( ( ( ( a .x. d ) .+ ( c .x. b ) ) .x. f ) .+ ( e .x. ( b .x. d ) ) ) , ( ( b .x. d ) .x. f ) >. = <. ( ( a .x. ( d .x. f ) ) .+ ( ( ( c .x. f ) .+ ( e .x. d ) ) .x. b ) ) , ( b .x. ( d .x. f ) ) >. )
147	146	eceq1d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> [ <. ( ( ( ( a .x. d ) .+ ( c .x. b ) ) .x. f ) .+ ( e .x. ( b .x. d ) ) ) , ( ( b .x. d ) .x. f ) >. ] .~ = [ <. ( ( a .x. ( d .x. f ) ) .+ ( ( ( c .x. f ) .+ ( e .x. d ) ) .x. b ) ) , ( b .x. ( d .x. f ) ) >. ] .~ )
148	1 3 110 117 124	grpcld	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( a .x. d ) .+ ( c .x. b ) ) e. B )
149	95 113 122 115	submcld	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( b .x. d ) e. S )
150	1 2 3 4 5 109 113 148 126 149 118 20	rlocaddval	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( [ <. ( ( a .x. d ) .+ ( c .x. b ) ) , ( b .x. d ) >. ] .~ ( +g ` L ) [ <. e , f >. ] .~ ) = [ <. ( ( ( ( a .x. d ) .+ ( c .x. b ) ) .x. f ) .+ ( e .x. ( b .x. d ) ) ) , ( ( b .x. d ) .x. f ) >. ] .~ )
151	1 3 110 141 133	grpcld	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( c .x. f ) .+ ( e .x. d ) ) e. B )
152	95 113 115 118	submcld	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( d .x. f ) e. S )
153	1 2 3 4 5 109 113 112 151 122 152 20	rlocaddval	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( [ <. a , b >. ] .~ ( +g ` L ) [ <. ( ( c .x. f ) .+ ( e .x. d ) ) , ( d .x. f ) >. ] .~ ) = [ <. ( ( a .x. ( d .x. f ) ) .+ ( ( ( c .x. f ) .+ ( e .x. d ) ) .x. b ) ) , ( b .x. ( d .x. f ) ) >. ] .~ )
154	147 150 153	3eqtr4d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( [ <. ( ( a .x. d ) .+ ( c .x. b ) ) , ( b .x. d ) >. ] .~ ( +g ` L ) [ <. e , f >. ] .~ ) = ( [ <. a , b >. ] .~ ( +g ` L ) [ <. ( ( c .x. f ) .+ ( e .x. d ) ) , ( d .x. f ) >. ] .~ ) )
155	1 2 3 4 5 109 113 112 121 122 115 20	rlocaddval	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( [ <. a , b >. ] .~ ( +g ` L ) [ <. c , d >. ] .~ ) = [ <. ( ( a .x. d ) .+ ( c .x. b ) ) , ( b .x. d ) >. ] .~ )
156	155	oveq1d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( [ <. a , b >. ] .~ ( +g ` L ) [ <. c , d >. ] .~ ) ( +g ` L ) [ <. e , f >. ] .~ ) = ( [ <. ( ( a .x. d ) .+ ( c .x. b ) ) , ( b .x. d ) >. ] .~ ( +g ` L ) [ <. e , f >. ] .~ ) )
157	1 2 3 4 5 109 113 121 126 115 118 20	rlocaddval	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( [ <. c , d >. ] .~ ( +g ` L ) [ <. e , f >. ] .~ ) = [ <. ( ( c .x. f ) .+ ( e .x. d ) ) , ( d .x. f ) >. ] .~ )
158	157	oveq2d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( [ <. a , b >. ] .~ ( +g ` L ) ( [ <. c , d >. ] .~ ( +g ` L ) [ <. e , f >. ] .~ ) ) = ( [ <. a , b >. ] .~ ( +g ` L ) [ <. ( ( c .x. f ) .+ ( e .x. d ) ) , ( d .x. f ) >. ] .~ ) )
159	154 156 158	3eqtr4d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( [ <. a , b >. ] .~ ( +g ` L ) [ <. c , d >. ] .~ ) ( +g ` L ) [ <. e , f >. ] .~ ) = ( [ <. a , b >. ] .~ ( +g ` L ) ( [ <. c , d >. ] .~ ( +g ` L ) [ <. e , f >. ] .~ ) ) )
160		simp-7r	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> x = [ <. a , b >. ] .~ )
161		simp-4r	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> y = [ <. c , d >. ] .~ )
162	160 161	oveq12d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( x ( +g ` L ) y ) = ( [ <. a , b >. ] .~ ( +g ` L ) [ <. c , d >. ] .~ ) )
163		simpr	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> z = [ <. e , f >. ] .~ )
164	162 163	oveq12d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( x ( +g ` L ) y ) ( +g ` L ) z ) = ( ( [ <. a , b >. ] .~ ( +g ` L ) [ <. c , d >. ] .~ ) ( +g ` L ) [ <. e , f >. ] .~ ) )
165	161 163	oveq12d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( y ( +g ` L ) z ) = ( [ <. c , d >. ] .~ ( +g ` L ) [ <. e , f >. ] .~ ) )
166	160 165	oveq12d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( x ( +g ` L ) ( y ( +g ` L ) z ) ) = ( [ <. a , b >. ] .~ ( +g ` L ) ( [ <. c , d >. ] .~ ( +g ` L ) [ <. e , f >. ] .~ ) ) )
167	159 164 166	3eqtr4d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( x ( +g ` L ) y ) ( +g ` L ) z ) = ( x ( +g ` L ) ( y ( +g ` L ) z ) ) )
168		simpr3	\|- ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) -> z e. ( ( B X. S ) /. .~ ) )
169	168	ad6antr	\|- ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> z e. ( ( B X. S ) /. .~ ) )
170	169	elrlocbasi	\|- ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> E. e e. B E. f e. S z = [ <. e , f >. ] .~ )
171	167 170	r19.29vva	\|- ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> ( ( x ( +g ` L ) y ) ( +g ` L ) z ) = ( x ( +g ` L ) ( y ( +g ` L ) z ) ) )
172		simpr2	\|- ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) -> y e. ( ( B X. S ) /. .~ ) )
173	172	ad3antrrr	\|- ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> y e. ( ( B X. S ) /. .~ ) )
174	173	elrlocbasi	\|- ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> E. c e. B E. d e. S y = [ <. c , d >. ] .~ )
175	171 174	r19.29vva	\|- ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( ( x ( +g ` L ) y ) ( +g ` L ) z ) = ( x ( +g ` L ) ( y ( +g ` L ) z ) ) )
176		simpr1	\|- ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) -> x e. ( ( B X. S ) /. .~ ) )
177	176	elrlocbasi	\|- ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) -> E. a e. B E. b e. S x = [ <. a , b >. ] .~ )
178	175 177	r19.29vva	\|- ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) -> ( ( x ( +g ` L ) y ) ( +g ` L ) z ) = ( x ( +g ` L ) ( y ( +g ` L ) z ) ) )
179	15 16 108 178 31 61 74	ismndd	\|- ( ph -> L e. Mnd )
180		eqid	\|- ( invg ` R ) = ( invg ` R )
181	1 180 47 43	grpinvcld	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( ( invg ` R ) ` a ) e. B )
182	181 40	opelxpd	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> <. ( ( invg ` R ) ` a ) , b >. e. ( B X. S ) )
183	29	ecelqsi	\|- ( <. ( ( invg ` R ) ` a ) , b >. e. ( B X. S ) -> [ <. ( ( invg ` R ) ` a ) , b >. ] .~ e. ( ( B X. S ) /. .~ ) )
184	182 183	syl	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> [ <. ( ( invg ` R ) ` a ) , b >. ] .~ e. ( ( B X. S ) /. .~ ) )
185		simpr	\|- ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ u = [ <. ( ( invg ` R ) ` a ) , b >. ] .~ ) -> u = [ <. ( ( invg ` R ) ` a ) , b >. ] .~ )
186		simplr	\|- ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ u = [ <. ( ( invg ` R ) ` a ) , b >. ] .~ ) -> x = [ <. a , b >. ] .~ )
187	185 186	oveq12d	\|- ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ u = [ <. ( ( invg ` R ) ` a ) , b >. ] .~ ) -> ( u ( +g ` L ) x ) = ( [ <. ( ( invg ` R ) ` a ) , b >. ] .~ ( +g ` L ) [ <. a , b >. ] .~ ) )
188	187	eqeq1d	\|- ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ u = [ <. ( ( invg ` R ) ` a ) , b >. ] .~ ) -> ( ( u ( +g ` L ) x ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] .~ <-> ( [ <. ( ( invg ` R ) ` a ) , b >. ] .~ ( +g ` L ) [ <. a , b >. ] .~ ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] .~ ) )
189	1 2 3 4 5 53 38 181 43 40 40 20	rlocaddval	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( [ <. ( ( invg ` R ) ` a ) , b >. ] .~ ( +g ` L ) [ <. a , b >. ] .~ ) = [ <. ( ( ( ( invg ` R ) ` a ) .x. b ) .+ ( a .x. b ) ) , ( b .x. b ) >. ] .~ )
190	1 3 8 180 47 43	grplinvd	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( ( ( invg ` R ) ` a ) .+ a ) = ( 0g ` R ) )
191	190	oveq1d	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( ( ( ( invg ` R ) ` a ) .+ a ) .x. b ) = ( ( 0g ` R ) .x. b ) )
192	1 3 2 37 181 43 41	ringdird	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( ( ( ( invg ` R ) ` a ) .+ a ) .x. b ) = ( ( ( ( invg ` R ) ` a ) .x. b ) .+ ( a .x. b ) ) )
193	191 192 42	3eqtr3d	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( ( ( ( invg ` R ) ` a ) .x. b ) .+ ( a .x. b ) ) = ( 0g ` R ) )
194	193	opeq1d	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> <. ( ( ( ( invg ` R ) ` a ) .x. b ) .+ ( a .x. b ) ) , ( b .x. b ) >. = <. ( 0g ` R ) , ( b .x. b ) >. )
195	194	eceq1d	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> [ <. ( ( ( ( invg ` R ) ` a ) .x. b ) .+ ( a .x. b ) ) , ( b .x. b ) >. ] .~ = [ <. ( 0g ` R ) , ( b .x. b ) >. ] .~ )
196	1 8 24 2 9 10 5 6 7	erler	\|- ( ph -> .~ Er ( B X. S ) )
197	196	ad4antr	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> .~ Er ( B X. S ) )
198		eqidd	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> <. ( 0g ` R ) , ( b .x. b ) >. = <. ( 0g ` R ) , ( b .x. b ) >. )
199		eqidd	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> <. ( 0g ` R ) , ( 1r ` R ) >. = <. ( 0g ` R ) , ( 1r ` R ) >. )
200	95 38 40 40	submcld	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( b .x. b ) e. S )
201	1 2 24 37 54	ringridmd	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( ( 0g ` R ) .x. ( 1r ` R ) ) = ( 0g ` R ) )
202	39 200	sseldd	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( b .x. b ) e. B )
203	1 2 8 37 202	ringlzd	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( ( 0g ` R ) .x. ( b .x. b ) ) = ( 0g ` R ) )
204	201 203	oveq12d	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( ( ( 0g ` R ) .x. ( 1r ` R ) ) ( -g ` R ) ( ( 0g ` R ) .x. ( b .x. b ) ) ) = ( ( 0g ` R ) ( -g ` R ) ( 0g ` R ) ) )
205	1 8 9	grpsubid	\|- ( ( R e. Grp /\ ( 0g ` R ) e. B ) -> ( ( 0g ` R ) ( -g ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
206	47 54 205	syl2anc	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( ( 0g ` R ) ( -g ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
207	204 206	eqtrd	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( ( ( 0g ` R ) .x. ( 1r ` R ) ) ( -g ` R ) ( ( 0g ` R ) .x. ( b .x. b ) ) ) = ( 0g ` R ) )
208	207	oveq2d	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( ( b .x. b ) .x. ( ( ( 0g ` R ) .x. ( 1r ` R ) ) ( -g ` R ) ( ( 0g ` R ) .x. ( b .x. b ) ) ) ) = ( ( b .x. b ) .x. ( 0g ` R ) ) )
209	1 2 8 37 202	ringrzd	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( ( b .x. b ) .x. ( 0g ` R ) ) = ( 0g ` R ) )
210	208 209	eqtrd	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( ( b .x. b ) .x. ( ( ( 0g ` R ) .x. ( 1r ` R ) ) ( -g ` R ) ( ( 0g ` R ) .x. ( b .x. b ) ) ) ) = ( 0g ` R ) )
211	1 5 39 8 2 9 198 199 54 54 200 55 200 210	erlbrd	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> <. ( 0g ` R ) , ( b .x. b ) >. .~ <. ( 0g ` R ) , ( 1r ` R ) >. )
212	197 211	erthi	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> [ <. ( 0g ` R ) , ( b .x. b ) >. ] .~ = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] .~ )
213	189 195 212	3eqtrd	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( [ <. ( ( invg ` R ) ` a ) , b >. ] .~ ( +g ` L ) [ <. a , b >. ] .~ ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] .~ )
214	184 188 213	rspcedvd	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> E. u e. ( ( B X. S ) /. .~ ) ( u ( +g ` L ) x ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] .~ )
215	214 60	r19.29vva	\|- ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) -> E. u e. ( ( B X. S ) /. .~ ) ( u ( +g ` L ) x ) = [ <. ( 0g ` R ) , ( 1r ` R ) >. ] .~ )
216	15 16 76 179 215	isgrpd2e	\|- ( ph -> L e. Grp )
217	77 78	oveq12d	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> ( x ( .r ` L ) y ) = ( [ <. a , b >. ] .~ ( .r ` L ) [ <. c , d >. ] .~ ) )
218		eqid	\|- ( .r ` L ) = ( .r ` L )
219	1 2 3 4 5 80 81 82 83 84 85 218	rlocmulval	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> ( [ <. a , b >. ] .~ ( .r ` L ) [ <. c , d >. ] .~ ) = [ <. ( a .x. c ) , ( b .x. d ) >. ] .~ )
220	1 2 88 82 83	ringcld	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> ( a .x. c ) e. B )
221	220 96	opelxpd	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> <. ( a .x. c ) , ( b .x. d ) >. e. ( B X. S ) )
222	29	ecelqsi	\|- ( <. ( a .x. c ) , ( b .x. d ) >. e. ( B X. S ) -> [ <. ( a .x. c ) , ( b .x. d ) >. ] .~ e. ( ( B X. S ) /. .~ ) )
223	221 222	syl	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> [ <. ( a .x. c ) , ( b .x. d ) >. ] .~ e. ( ( B X. S ) /. .~ ) )
224	219 223	eqeltrd	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> ( [ <. a , b >. ] .~ ( .r ` L ) [ <. c , d >. ] .~ ) e. ( ( B X. S ) /. .~ ) )
225	217 224	eqeltrd	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> ( x ( .r ` L ) y ) e. ( ( B X. S ) /. .~ ) )
226	225 103	r19.29vva	\|- ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( x ( .r ` L ) y ) e. ( ( B X. S ) /. .~ ) )
227	226 106	r19.29vva	\|- ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) -> ( x ( .r ` L ) y ) e. ( ( B X. S ) /. .~ ) )
228	227	3impa	\|- ( ( ph /\ x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) ) -> ( x ( .r ` L ) y ) e. ( ( B X. S ) /. .~ ) )
229	1 2 111 112 121 126	ringassd	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( a .x. c ) .x. e ) = ( a .x. ( c .x. e ) ) )
230	229 145	opeq12d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> <. ( ( a .x. c ) .x. e ) , ( ( b .x. d ) .x. f ) >. = <. ( a .x. ( c .x. e ) ) , ( b .x. ( d .x. f ) ) >. )
231	230	eceq1d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> [ <. ( ( a .x. c ) .x. e ) , ( ( b .x. d ) .x. f ) >. ] .~ = [ <. ( a .x. ( c .x. e ) ) , ( b .x. ( d .x. f ) ) >. ] .~ )
232	1 2 111 112 121	ringcld	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( a .x. c ) e. B )
233	1 2 3 4 5 109 113 232 126 149 118 218	rlocmulval	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( [ <. ( a .x. c ) , ( b .x. d ) >. ] .~ ( .r ` L ) [ <. e , f >. ] .~ ) = [ <. ( ( a .x. c ) .x. e ) , ( ( b .x. d ) .x. f ) >. ] .~ )
234	1 2 111 121 126	ringcld	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( c .x. e ) e. B )
235	1 2 3 4 5 109 113 112 234 122 152 218	rlocmulval	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( [ <. a , b >. ] .~ ( .r ` L ) [ <. ( c .x. e ) , ( d .x. f ) >. ] .~ ) = [ <. ( a .x. ( c .x. e ) ) , ( b .x. ( d .x. f ) ) >. ] .~ )
236	231 233 235	3eqtr4d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( [ <. ( a .x. c ) , ( b .x. d ) >. ] .~ ( .r ` L ) [ <. e , f >. ] .~ ) = ( [ <. a , b >. ] .~ ( .r ` L ) [ <. ( c .x. e ) , ( d .x. f ) >. ] .~ ) )
237	1 2 3 4 5 109 113 112 121 122 115 218	rlocmulval	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( [ <. a , b >. ] .~ ( .r ` L ) [ <. c , d >. ] .~ ) = [ <. ( a .x. c ) , ( b .x. d ) >. ] .~ )
238	237	oveq1d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( [ <. a , b >. ] .~ ( .r ` L ) [ <. c , d >. ] .~ ) ( .r ` L ) [ <. e , f >. ] .~ ) = ( [ <. ( a .x. c ) , ( b .x. d ) >. ] .~ ( .r ` L ) [ <. e , f >. ] .~ ) )
239	1 2 3 4 5 109 113 121 126 115 118 218	rlocmulval	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( [ <. c , d >. ] .~ ( .r ` L ) [ <. e , f >. ] .~ ) = [ <. ( c .x. e ) , ( d .x. f ) >. ] .~ )
240	239	oveq2d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( [ <. a , b >. ] .~ ( .r ` L ) ( [ <. c , d >. ] .~ ( .r ` L ) [ <. e , f >. ] .~ ) ) = ( [ <. a , b >. ] .~ ( .r ` L ) [ <. ( c .x. e ) , ( d .x. f ) >. ] .~ ) )
241	236 238 240	3eqtr4d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( [ <. a , b >. ] .~ ( .r ` L ) [ <. c , d >. ] .~ ) ( .r ` L ) [ <. e , f >. ] .~ ) = ( [ <. a , b >. ] .~ ( .r ` L ) ( [ <. c , d >. ] .~ ( .r ` L ) [ <. e , f >. ] .~ ) ) )
242	160 161	oveq12d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( x ( .r ` L ) y ) = ( [ <. a , b >. ] .~ ( .r ` L ) [ <. c , d >. ] .~ ) )
243	242 163	oveq12d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( x ( .r ` L ) y ) ( .r ` L ) z ) = ( ( [ <. a , b >. ] .~ ( .r ` L ) [ <. c , d >. ] .~ ) ( .r ` L ) [ <. e , f >. ] .~ ) )
244	161 163	oveq12d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( y ( .r ` L ) z ) = ( [ <. c , d >. ] .~ ( .r ` L ) [ <. e , f >. ] .~ ) )
245	160 244	oveq12d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( x ( .r ` L ) ( y ( .r ` L ) z ) ) = ( [ <. a , b >. ] .~ ( .r ` L ) ( [ <. c , d >. ] .~ ( .r ` L ) [ <. e , f >. ] .~ ) ) )
246	241 243 245	3eqtr4d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( x ( .r ` L ) y ) ( .r ` L ) z ) = ( x ( .r ` L ) ( y ( .r ` L ) z ) ) )
247	246 170	r19.29vva	\|- ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> ( ( x ( .r ` L ) y ) ( .r ` L ) z ) = ( x ( .r ` L ) ( y ( .r ` L ) z ) ) )
248	247 174	r19.29vva	\|- ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( ( x ( .r ` L ) y ) ( .r ` L ) z ) = ( x ( .r ` L ) ( y ( .r ` L ) z ) ) )
249	248 177	r19.29vva	\|- ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) -> ( ( x ( .r ` L ) y ) ( .r ` L ) z ) = ( x ( .r ` L ) ( y ( .r ` L ) z ) ) )
250	196	ad10antr	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> .~ Er ( B X. S ) )
251		eqidd	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> <. ( a .x. ( ( c .x. f ) .+ ( e .x. d ) ) ) , ( b .x. ( d .x. f ) ) >. = <. ( a .x. ( ( c .x. f ) .+ ( e .x. d ) ) ) , ( b .x. ( d .x. f ) ) >. )
252	1 2 111 112 123	ringcld	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( a .x. b ) e. B )
253	1 3 2 111 252 141 133	ringdid	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( a .x. b ) .x. ( ( c .x. f ) .+ ( e .x. d ) ) ) = ( ( ( a .x. b ) .x. ( c .x. f ) ) .+ ( ( a .x. b ) .x. ( e .x. d ) ) ) )
254	1 2 111 112 123 151	ringassd	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( a .x. b ) .x. ( ( c .x. f ) .+ ( e .x. d ) ) ) = ( a .x. ( b .x. ( ( c .x. f ) .+ ( e .x. d ) ) ) ) )
255	253 254	eqtr3d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( ( a .x. b ) .x. ( c .x. f ) ) .+ ( ( a .x. b ) .x. ( e .x. d ) ) ) = ( a .x. ( b .x. ( ( c .x. f ) .+ ( e .x. d ) ) ) ) )
256	11	crngmgp	\|- ( R e. CRing -> ( mulGrp ` R ) e. CMnd )
257	6 256	syl	\|- ( ph -> ( mulGrp ` R ) e. CMnd )
258	257	ad10antr	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( mulGrp ` R ) e. CMnd )
259	12 95 258 112 121 123 119	cmn4d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( a .x. c ) .x. ( b .x. f ) ) = ( ( a .x. b ) .x. ( c .x. f ) ) )
260	12 95 258 112 126 123 116	cmn4d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( a .x. e ) .x. ( b .x. d ) ) = ( ( a .x. b ) .x. ( e .x. d ) ) )
261	259 260	oveq12d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( ( a .x. c ) .x. ( b .x. f ) ) .+ ( ( a .x. e ) .x. ( b .x. d ) ) ) = ( ( ( a .x. b ) .x. ( c .x. f ) ) .+ ( ( a .x. b ) .x. ( e .x. d ) ) ) )
262	1 2 109 123 112 151	crng12d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( b .x. ( a .x. ( ( c .x. f ) .+ ( e .x. d ) ) ) ) = ( a .x. ( b .x. ( ( c .x. f ) .+ ( e .x. d ) ) ) ) )
263	255 261 262	3eqtr4d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( ( a .x. c ) .x. ( b .x. f ) ) .+ ( ( a .x. e ) .x. ( b .x. d ) ) ) = ( b .x. ( a .x. ( ( c .x. f ) .+ ( e .x. d ) ) ) ) )
264	1 2 109 127 123 119	crng12d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( b .x. d ) .x. ( b .x. f ) ) = ( b .x. ( ( b .x. d ) .x. f ) ) )
265	145	oveq2d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( b .x. ( ( b .x. d ) .x. f ) ) = ( b .x. ( b .x. ( d .x. f ) ) ) )
266	264 265	eqtrd	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( b .x. d ) .x. ( b .x. f ) ) = ( b .x. ( b .x. ( d .x. f ) ) ) )
267	263 266	opeq12d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> <. ( ( ( a .x. c ) .x. ( b .x. f ) ) .+ ( ( a .x. e ) .x. ( b .x. d ) ) ) , ( ( b .x. d ) .x. ( b .x. f ) ) >. = <. ( b .x. ( a .x. ( ( c .x. f ) .+ ( e .x. d ) ) ) ) , ( b .x. ( b .x. ( d .x. f ) ) ) >. )
268	1 2 111 112 151	ringcld	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( a .x. ( ( c .x. f ) .+ ( e .x. d ) ) ) e. B )
269	1 2 111 123 268	ringcld	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( b .x. ( a .x. ( ( c .x. f ) .+ ( e .x. d ) ) ) ) e. B )
270	95 113 122 152	submcld	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( b .x. ( d .x. f ) ) e. S )
271	95 113 122 270	submcld	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( b .x. ( b .x. ( d .x. f ) ) ) e. S )
272		eqidd	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( b .x. ( a .x. ( ( c .x. f ) .+ ( e .x. d ) ) ) ) = ( b .x. ( a .x. ( ( c .x. f ) .+ ( e .x. d ) ) ) ) )
273		eqidd	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( b .x. ( b .x. ( d .x. f ) ) ) = ( b .x. ( b .x. ( d .x. f ) ) ) )
274	1 5 109 113 2 251 267 268 269 270 271 122 272 273	erlbr2d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> <. ( a .x. ( ( c .x. f ) .+ ( e .x. d ) ) ) , ( b .x. ( d .x. f ) ) >. .~ <. ( ( ( a .x. c ) .x. ( b .x. f ) ) .+ ( ( a .x. e ) .x. ( b .x. d ) ) ) , ( ( b .x. d ) .x. ( b .x. f ) ) >. )
275	250 274	erthi	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> [ <. ( a .x. ( ( c .x. f ) .+ ( e .x. d ) ) ) , ( b .x. ( d .x. f ) ) >. ] .~ = [ <. ( ( ( a .x. c ) .x. ( b .x. f ) ) .+ ( ( a .x. e ) .x. ( b .x. d ) ) ) , ( ( b .x. d ) .x. ( b .x. f ) ) >. ] .~ )
276	1 2 3 4 5 109 113 112 151 122 152 218	rlocmulval	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( [ <. a , b >. ] .~ ( .r ` L ) [ <. ( ( c .x. f ) .+ ( e .x. d ) ) , ( d .x. f ) >. ] .~ ) = [ <. ( a .x. ( ( c .x. f ) .+ ( e .x. d ) ) ) , ( b .x. ( d .x. f ) ) >. ] .~ )
277	1 2 111 112 126	ringcld	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( a .x. e ) e. B )
278	95 113 122 118	submcld	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( b .x. f ) e. S )
279	1 2 3 4 5 109 113 232 277 149 278 20	rlocaddval	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( [ <. ( a .x. c ) , ( b .x. d ) >. ] .~ ( +g ` L ) [ <. ( a .x. e ) , ( b .x. f ) >. ] .~ ) = [ <. ( ( ( a .x. c ) .x. ( b .x. f ) ) .+ ( ( a .x. e ) .x. ( b .x. d ) ) ) , ( ( b .x. d ) .x. ( b .x. f ) ) >. ] .~ )
280	275 276 279	3eqtr4d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( [ <. a , b >. ] .~ ( .r ` L ) [ <. ( ( c .x. f ) .+ ( e .x. d ) ) , ( d .x. f ) >. ] .~ ) = ( [ <. ( a .x. c ) , ( b .x. d ) >. ] .~ ( +g ` L ) [ <. ( a .x. e ) , ( b .x. f ) >. ] .~ ) )
281	157	oveq2d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( [ <. a , b >. ] .~ ( .r ` L ) ( [ <. c , d >. ] .~ ( +g ` L ) [ <. e , f >. ] .~ ) ) = ( [ <. a , b >. ] .~ ( .r ` L ) [ <. ( ( c .x. f ) .+ ( e .x. d ) ) , ( d .x. f ) >. ] .~ ) )
282	1 2 3 4 5 109 113 112 126 122 118 218	rlocmulval	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( [ <. a , b >. ] .~ ( .r ` L ) [ <. e , f >. ] .~ ) = [ <. ( a .x. e ) , ( b .x. f ) >. ] .~ )
283	237 282	oveq12d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( [ <. a , b >. ] .~ ( .r ` L ) [ <. c , d >. ] .~ ) ( +g ` L ) ( [ <. a , b >. ] .~ ( .r ` L ) [ <. e , f >. ] .~ ) ) = ( [ <. ( a .x. c ) , ( b .x. d ) >. ] .~ ( +g ` L ) [ <. ( a .x. e ) , ( b .x. f ) >. ] .~ ) )
284	280 281 283	3eqtr4d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( [ <. a , b >. ] .~ ( .r ` L ) ( [ <. c , d >. ] .~ ( +g ` L ) [ <. e , f >. ] .~ ) ) = ( ( [ <. a , b >. ] .~ ( .r ` L ) [ <. c , d >. ] .~ ) ( +g ` L ) ( [ <. a , b >. ] .~ ( .r ` L ) [ <. e , f >. ] .~ ) ) )
285	160 165	oveq12d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( x ( .r ` L ) ( y ( +g ` L ) z ) ) = ( [ <. a , b >. ] .~ ( .r ` L ) ( [ <. c , d >. ] .~ ( +g ` L ) [ <. e , f >. ] .~ ) ) )
286	160 163	oveq12d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( x ( .r ` L ) z ) = ( [ <. a , b >. ] .~ ( .r ` L ) [ <. e , f >. ] .~ ) )
287	242 286	oveq12d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( x ( .r ` L ) y ) ( +g ` L ) ( x ( .r ` L ) z ) ) = ( ( [ <. a , b >. ] .~ ( .r ` L ) [ <. c , d >. ] .~ ) ( +g ` L ) ( [ <. a , b >. ] .~ ( .r ` L ) [ <. e , f >. ] .~ ) ) )
288	284 285 287	3eqtr4d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( x ( .r ` L ) ( y ( +g ` L ) z ) ) = ( ( x ( .r ` L ) y ) ( +g ` L ) ( x ( .r ` L ) z ) ) )
289	288 170	r19.29vva	\|- ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> ( x ( .r ` L ) ( y ( +g ` L ) z ) ) = ( ( x ( .r ` L ) y ) ( +g ` L ) ( x ( .r ` L ) z ) ) )
290	289 174	r19.29vva	\|- ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( x ( .r ` L ) ( y ( +g ` L ) z ) ) = ( ( x ( .r ` L ) y ) ( +g ` L ) ( x ( .r ` L ) z ) ) )
291	290 177	r19.29vva	\|- ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) -> ( x ( .r ` L ) ( y ( +g ` L ) z ) ) = ( ( x ( .r ` L ) y ) ( +g ` L ) ( x ( .r ` L ) z ) ) )
292	1 3 2 111 117 124 126	ringdird	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( ( a .x. d ) .+ ( c .x. b ) ) .x. e ) = ( ( ( a .x. d ) .x. e ) .+ ( ( c .x. b ) .x. e ) ) )
293	292	opeq1d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> <. ( ( ( a .x. d ) .+ ( c .x. b ) ) .x. e ) , ( ( b .x. d ) .x. f ) >. = <. ( ( ( a .x. d ) .x. e ) .+ ( ( c .x. b ) .x. e ) ) , ( ( b .x. d ) .x. f ) >. )
294	1 2 111 117 126 119	ringassd	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( ( a .x. d ) .x. e ) .x. f ) = ( ( a .x. d ) .x. ( e .x. f ) ) )
295	1 2 111 117 126	ringcld	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( a .x. d ) .x. e ) e. B )
296	1 2 109 119 295	crngcomd	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( f .x. ( ( a .x. d ) .x. e ) ) = ( ( ( a .x. d ) .x. e ) .x. f ) )
297	12 95 258 112 126 116 119	cmn4d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( a .x. e ) .x. ( d .x. f ) ) = ( ( a .x. d ) .x. ( e .x. f ) ) )
298	294 296 297	3eqtr4rd	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( a .x. e ) .x. ( d .x. f ) ) = ( f .x. ( ( a .x. d ) .x. e ) ) )
299	1 2 111 124 126 119	ringassd	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( ( c .x. b ) .x. e ) .x. f ) = ( ( c .x. b ) .x. ( e .x. f ) ) )
300	1 2 111 124 126	ringcld	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( c .x. b ) .x. e ) e. B )
301	1 2 109 119 300	crngcomd	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( f .x. ( ( c .x. b ) .x. e ) ) = ( ( ( c .x. b ) .x. e ) .x. f ) )
302	12 95 258 121 126 123 119	cmn4d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( c .x. e ) .x. ( b .x. f ) ) = ( ( c .x. b ) .x. ( e .x. f ) ) )
303	299 301 302	3eqtr4rd	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( c .x. e ) .x. ( b .x. f ) ) = ( f .x. ( ( c .x. b ) .x. e ) ) )
304	298 303	oveq12d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( ( a .x. e ) .x. ( d .x. f ) ) .+ ( ( c .x. e ) .x. ( b .x. f ) ) ) = ( ( f .x. ( ( a .x. d ) .x. e ) ) .+ ( f .x. ( ( c .x. b ) .x. e ) ) ) )
305	1 3 2 111 119 295 300	ringdid	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( f .x. ( ( ( a .x. d ) .x. e ) .+ ( ( c .x. b ) .x. e ) ) ) = ( ( f .x. ( ( a .x. d ) .x. e ) ) .+ ( f .x. ( ( c .x. b ) .x. e ) ) ) )
306	304 305	eqtr4d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( ( a .x. e ) .x. ( d .x. f ) ) .+ ( ( c .x. e ) .x. ( b .x. f ) ) ) = ( f .x. ( ( ( a .x. d ) .x. e ) .+ ( ( c .x. b ) .x. e ) ) ) )
307	114 278	sseldd	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( b .x. f ) e. B )
308	1 2 111 116 307 119	ringassd	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( d .x. ( b .x. f ) ) .x. f ) = ( d .x. ( ( b .x. f ) .x. f ) ) )
309	1 2 109 123 116	crngcomd	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( b .x. d ) = ( d .x. b ) )
310	309	oveq1d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( b .x. d ) .x. f ) = ( ( d .x. b ) .x. f ) )
311	1 2 111 116 123 119	ringassd	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( d .x. b ) .x. f ) = ( d .x. ( b .x. f ) ) )
312	310 311	eqtrd	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( b .x. d ) .x. f ) = ( d .x. ( b .x. f ) ) )
313	312	oveq1d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( ( b .x. d ) .x. f ) .x. f ) = ( ( d .x. ( b .x. f ) ) .x. f ) )
314	1 2 109 307 116 119	crng12d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( b .x. f ) .x. ( d .x. f ) ) = ( d .x. ( ( b .x. f ) .x. f ) ) )
315	308 313 314	3eqtr4rd	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( b .x. f ) .x. ( d .x. f ) ) = ( ( ( b .x. d ) .x. f ) .x. f ) )
316	306 315	opeq12d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> <. ( ( ( a .x. e ) .x. ( d .x. f ) ) .+ ( ( c .x. e ) .x. ( b .x. f ) ) ) , ( ( b .x. f ) .x. ( d .x. f ) ) >. = <. ( f .x. ( ( ( a .x. d ) .x. e ) .+ ( ( c .x. b ) .x. e ) ) ) , ( ( ( b .x. d ) .x. f ) .x. f ) >. )
317	1 3 110 295 300	grpcld	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( ( a .x. d ) .x. e ) .+ ( ( c .x. b ) .x. e ) ) e. B )
318	1 2 111 119 317	ringcld	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( f .x. ( ( ( a .x. d ) .x. e ) .+ ( ( c .x. b ) .x. e ) ) ) e. B )
319	145 270	eqeltrd	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( b .x. d ) .x. f ) e. S )
320	95 113 319 118	submcld	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( ( b .x. d ) .x. f ) .x. f ) e. S )
321		eqidd	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( f .x. ( ( ( a .x. d ) .x. e ) .+ ( ( c .x. b ) .x. e ) ) ) = ( f .x. ( ( ( a .x. d ) .x. e ) .+ ( ( c .x. b ) .x. e ) ) ) )
322	114 319	sseldd	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( b .x. d ) .x. f ) e. B )
323	1 2 109 322 119	crngcomd	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( ( b .x. d ) .x. f ) .x. f ) = ( f .x. ( ( b .x. d ) .x. f ) ) )
324	1 5 109 113 2 293 316 317 318 319 320 118 321 323	erlbr2d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> <. ( ( ( a .x. d ) .+ ( c .x. b ) ) .x. e ) , ( ( b .x. d ) .x. f ) >. .~ <. ( ( ( a .x. e ) .x. ( d .x. f ) ) .+ ( ( c .x. e ) .x. ( b .x. f ) ) ) , ( ( b .x. f ) .x. ( d .x. f ) ) >. )
325	250 324	erthi	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> [ <. ( ( ( a .x. d ) .+ ( c .x. b ) ) .x. e ) , ( ( b .x. d ) .x. f ) >. ] .~ = [ <. ( ( ( a .x. e ) .x. ( d .x. f ) ) .+ ( ( c .x. e ) .x. ( b .x. f ) ) ) , ( ( b .x. f ) .x. ( d .x. f ) ) >. ] .~ )
326	1 2 3 4 5 109 113 148 126 149 118 218	rlocmulval	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( [ <. ( ( a .x. d ) .+ ( c .x. b ) ) , ( b .x. d ) >. ] .~ ( .r ` L ) [ <. e , f >. ] .~ ) = [ <. ( ( ( a .x. d ) .+ ( c .x. b ) ) .x. e ) , ( ( b .x. d ) .x. f ) >. ] .~ )
327	1 2 3 4 5 109 113 277 234 278 152 20	rlocaddval	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( [ <. ( a .x. e ) , ( b .x. f ) >. ] .~ ( +g ` L ) [ <. ( c .x. e ) , ( d .x. f ) >. ] .~ ) = [ <. ( ( ( a .x. e ) .x. ( d .x. f ) ) .+ ( ( c .x. e ) .x. ( b .x. f ) ) ) , ( ( b .x. f ) .x. ( d .x. f ) ) >. ] .~ )
328	325 326 327	3eqtr4d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( [ <. ( ( a .x. d ) .+ ( c .x. b ) ) , ( b .x. d ) >. ] .~ ( .r ` L ) [ <. e , f >. ] .~ ) = ( [ <. ( a .x. e ) , ( b .x. f ) >. ] .~ ( +g ` L ) [ <. ( c .x. e ) , ( d .x. f ) >. ] .~ ) )
329	155	oveq1d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( [ <. a , b >. ] .~ ( +g ` L ) [ <. c , d >. ] .~ ) ( .r ` L ) [ <. e , f >. ] .~ ) = ( [ <. ( ( a .x. d ) .+ ( c .x. b ) ) , ( b .x. d ) >. ] .~ ( .r ` L ) [ <. e , f >. ] .~ ) )
330	282 239	oveq12d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( [ <. a , b >. ] .~ ( .r ` L ) [ <. e , f >. ] .~ ) ( +g ` L ) ( [ <. c , d >. ] .~ ( .r ` L ) [ <. e , f >. ] .~ ) ) = ( [ <. ( a .x. e ) , ( b .x. f ) >. ] .~ ( +g ` L ) [ <. ( c .x. e ) , ( d .x. f ) >. ] .~ ) )
331	328 329 330	3eqtr4d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( [ <. a , b >. ] .~ ( +g ` L ) [ <. c , d >. ] .~ ) ( .r ` L ) [ <. e , f >. ] .~ ) = ( ( [ <. a , b >. ] .~ ( .r ` L ) [ <. e , f >. ] .~ ) ( +g ` L ) ( [ <. c , d >. ] .~ ( .r ` L ) [ <. e , f >. ] .~ ) ) )
332	162 163	oveq12d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( x ( +g ` L ) y ) ( .r ` L ) z ) = ( ( [ <. a , b >. ] .~ ( +g ` L ) [ <. c , d >. ] .~ ) ( .r ` L ) [ <. e , f >. ] .~ ) )
333	286 244	oveq12d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( x ( .r ` L ) z ) ( +g ` L ) ( y ( .r ` L ) z ) ) = ( ( [ <. a , b >. ] .~ ( .r ` L ) [ <. e , f >. ] .~ ) ( +g ` L ) ( [ <. c , d >. ] .~ ( .r ` L ) [ <. e , f >. ] .~ ) ) )
334	331 332 333	3eqtr4d	\|- ( ( ( ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) /\ e e. B ) /\ f e. S ) /\ z = [ <. e , f >. ] .~ ) -> ( ( x ( +g ` L ) y ) ( .r ` L ) z ) = ( ( x ( .r ` L ) z ) ( +g ` L ) ( y ( .r ` L ) z ) ) )
335	334 170	r19.29vva	\|- ( ( ( ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> ( ( x ( +g ` L ) y ) ( .r ` L ) z ) = ( ( x ( .r ` L ) z ) ( +g ` L ) ( y ( .r ` L ) z ) ) )
336	335 174	r19.29vva	\|- ( ( ( ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( ( x ( +g ` L ) y ) ( .r ` L ) z ) = ( ( x ( .r ` L ) z ) ( +g ` L ) ( y ( .r ` L ) z ) ) )
337	336 177	r19.29vva	\|- ( ( ph /\ ( x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) /\ z e. ( ( B X. S ) /. .~ ) ) ) -> ( ( x ( +g ` L ) y ) ( .r ` L ) z ) = ( ( x ( .r ` L ) z ) ( +g ` L ) ( y ( .r ` L ) z ) ) )
338	14 27	sseldd	\|- ( ph -> ( 1r ` R ) e. B )
339	338 27	opelxpd	\|- ( ph -> <. ( 1r ` R ) , ( 1r ` R ) >. e. ( B X. S ) )
340	29	ecelqsi	\|- ( <. ( 1r ` R ) , ( 1r ` R ) >. e. ( B X. S ) -> [ <. ( 1r ` R ) , ( 1r ` R ) >. ] .~ e. ( ( B X. S ) /. .~ ) )
341	339 340	syl	\|- ( ph -> [ <. ( 1r ` R ) , ( 1r ` R ) >. ] .~ e. ( ( B X. S ) /. .~ ) )
342	35	oveq2d	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( [ <. ( 1r ` R ) , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( [ <. ( 1r ` R ) , ( 1r ` R ) >. ] .~ ( .r ` L ) [ <. a , b >. ] .~ ) )
343	1 2 24 37 43	ringlidmd	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( ( 1r ` R ) .x. a ) = a )
344	343 50	opeq12d	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> <. ( ( 1r ` R ) .x. a ) , ( ( 1r ` R ) .x. b ) >. = <. a , b >. )
345	344	eceq1d	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> [ <. ( ( 1r ` R ) .x. a ) , ( ( 1r ` R ) .x. b ) >. ] .~ = [ <. a , b >. ] .~ )
346	39 55	sseldd	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( 1r ` R ) e. B )
347	1 2 3 4 5 53 38 346 43 55 40 218	rlocmulval	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( [ <. ( 1r ` R ) , ( 1r ` R ) >. ] .~ ( .r ` L ) [ <. a , b >. ] .~ ) = [ <. ( ( 1r ` R ) .x. a ) , ( ( 1r ` R ) .x. b ) >. ] .~ )
348	345 347 35	3eqtr4d	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( [ <. ( 1r ` R ) , ( 1r ` R ) >. ] .~ ( .r ` L ) [ <. a , b >. ] .~ ) = x )
349	342 348	eqtrd	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( [ <. ( 1r ` R ) , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = x )
350	349 60	r19.29vva	\|- ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) -> ( [ <. ( 1r ` R ) , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = x )
351	1 2 3 4 5 53 38 43 346 40 55 218	rlocmulval	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( [ <. a , b >. ] .~ ( .r ` L ) [ <. ( 1r ` R ) , ( 1r ` R ) >. ] .~ ) = [ <. ( a .x. ( 1r ` R ) ) , ( b .x. ( 1r ` R ) ) >. ] .~ )
352	35	oveq1d	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( x ( .r ` L ) [ <. ( 1r ` R ) , ( 1r ` R ) >. ] .~ ) = ( [ <. a , b >. ] .~ ( .r ` L ) [ <. ( 1r ` R ) , ( 1r ` R ) >. ] .~ ) )
353	44	eqcomd	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> a = ( a .x. ( 1r ` R ) ) )
354	353 69	opeq12d	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> <. a , b >. = <. ( a .x. ( 1r ` R ) ) , ( b .x. ( 1r ` R ) ) >. )
355	354	eceq1d	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> [ <. a , b >. ] .~ = [ <. ( a .x. ( 1r ` R ) ) , ( b .x. ( 1r ` R ) ) >. ] .~ )
356	351 352 355	3eqtr4d	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( x ( .r ` L ) [ <. ( 1r ` R ) , ( 1r ` R ) >. ] .~ ) = [ <. a , b >. ] .~ )
357	356 35	eqtr4d	\|- ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( x ( .r ` L ) [ <. ( 1r ` R ) , ( 1r ` R ) >. ] .~ ) = x )
358	357 60	r19.29vva	\|- ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) -> ( x ( .r ` L ) [ <. ( 1r ` R ) , ( 1r ` R ) >. ] .~ ) = x )
359	1 2 80 82 83	crngcomd	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> ( a .x. c ) = ( c .x. a ) )
360	1 2 80 92 90	crngcomd	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> ( b .x. d ) = ( d .x. b ) )
361	359 360	opeq12d	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> <. ( a .x. c ) , ( b .x. d ) >. = <. ( c .x. a ) , ( d .x. b ) >. )
362	361	eceq1d	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> [ <. ( a .x. c ) , ( b .x. d ) >. ] .~ = [ <. ( c .x. a ) , ( d .x. b ) >. ] .~ )
363	1 2 3 4 5 80 81 83 82 85 84 218	rlocmulval	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> ( [ <. c , d >. ] .~ ( .r ` L ) [ <. a , b >. ] .~ ) = [ <. ( c .x. a ) , ( d .x. b ) >. ] .~ )
364	362 219 363	3eqtr4d	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> ( [ <. a , b >. ] .~ ( .r ` L ) [ <. c , d >. ] .~ ) = ( [ <. c , d >. ] .~ ( .r ` L ) [ <. a , b >. ] .~ ) )
365	78 77	oveq12d	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> ( y ( .r ` L ) x ) = ( [ <. c , d >. ] .~ ( .r ` L ) [ <. a , b >. ] .~ ) )
366	364 217 365	3eqtr4d	\|- ( ( ( ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) /\ c e. B ) /\ d e. S ) /\ y = [ <. c , d >. ] .~ ) -> ( x ( .r ` L ) y ) = ( y ( .r ` L ) x ) )
367	366 103	r19.29vva	\|- ( ( ( ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) /\ a e. B ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( x ( .r ` L ) y ) = ( y ( .r ` L ) x ) )
368	367 106	r19.29vva	\|- ( ( ( ph /\ x e. ( ( B X. S ) /. .~ ) ) /\ y e. ( ( B X. S ) /. .~ ) ) -> ( x ( .r ` L ) y ) = ( y ( .r ` L ) x ) )
369	368	3impa	\|- ( ( ph /\ x e. ( ( B X. S ) /. .~ ) /\ y e. ( ( B X. S ) /. .~ ) ) -> ( x ( .r ` L ) y ) = ( y ( .r ` L ) x ) )
370	15 16 17 216 228 249 291 337 341 350 358 369	iscrngd	\|- ( ph -> L e. CRing )

Metamath Proof Explorer

Theorem rloccring

Proof