Theorem mul4sqlem

Description: Lemma for mul4sq : algebraic manipulations. The extra assumptions involving M are for a part of 4sqlem17 which needs to know not just that the product is a sum of squares, but also that it preserves divisibility by M . (Contributed by Mario Carneiro, 14-Jul-2014)

	Ref	Expression
Hypotheses	4sq.1	|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }
	mul4sq.1	|- ( ph -> A e. Z[i] )
	mul4sq.2	|- ( ph -> B e. Z[i] )
	mul4sq.3	|- ( ph -> C e. Z[i] )
	mul4sq.4	|- ( ph -> D e. Z[i] )
	mul4sq.5	|- X = ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) )
	mul4sq.6	|- Y = ( ( ( abs ` C ) ^ 2 ) + ( ( abs ` D ) ^ 2 ) )
	mul4sq.7	|- ( ph -> M e. NN )
	mul4sq.8	|- ( ph -> ( ( A - C ) / M ) e. Z[i] )
	mul4sq.9	|- ( ph -> ( ( B - D ) / M ) e. Z[i] )
	mul4sq.10	|- ( ph -> ( X / M ) e. NN0 )
Assertion	mul4sqlem	|- ( ph -> ( ( X / M ) x. ( Y / M ) ) e. S )

Proof

Step	Hyp	Ref	Expression
1		4sq.1	|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }
2		mul4sq.1	|- ( ph -> A e. Z[i] )
3		mul4sq.2	|- ( ph -> B e. Z[i] )
4		mul4sq.3	|- ( ph -> C e. Z[i] )
5		mul4sq.4	|- ( ph -> D e. Z[i] )
6		mul4sq.5	|- X = ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) )
7		mul4sq.6	|- Y = ( ( ( abs ` C ) ^ 2 ) + ( ( abs ` D ) ^ 2 ) )
8		mul4sq.7	|- ( ph -> M e. NN )
9		mul4sq.8	|- ( ph -> ( ( A - C ) / M ) e. Z[i] )
10		mul4sq.9	|- ( ph -> ( ( B - D ) / M ) e. Z[i] )
11		mul4sq.10	|- ( ph -> ( X / M ) e. NN0 )
12		gzcn	|- ( A e. Z[i] -> A e. CC )
13	2 12	syl	|- ( ph -> A e. CC )
14		gzcn	|- ( C e. Z[i] -> C e. CC )
15	4 14	syl	|- ( ph -> C e. CC )
16	13 15	mulcld	|- ( ph -> ( A x. C ) e. CC )
17	16	absvalsqd	|- ( ph -> ( ( abs ` ( A x. C ) ) ^ 2 ) = ( ( A x. C ) x. ( * ` ( A x. C ) ) ) )
18	16	cjcld	|- ( ph -> ( * ` ( A x. C ) ) e. CC )
19	16 18	mulcld	|- ( ph -> ( ( A x. C ) x. ( * ` ( A x. C ) ) ) e. CC )
20	17 19	eqeltrd	|- ( ph -> ( ( abs ` ( A x. C ) ) ^ 2 ) e. CC )
21		gzcn	|- ( B e. Z[i] -> B e. CC )
22	3 21	syl	|- ( ph -> B e. CC )
23		gzcn	|- ( D e. Z[i] -> D e. CC )
24	5 23	syl	|- ( ph -> D e. CC )
25	22 24	mulcld	|- ( ph -> ( B x. D ) e. CC )
26	25	absvalsqd	|- ( ph -> ( ( abs ` ( B x. D ) ) ^ 2 ) = ( ( B x. D ) x. ( * ` ( B x. D ) ) ) )
27	25	cjcld	|- ( ph -> ( * ` ( B x. D ) ) e. CC )
28	25 27	mulcld	|- ( ph -> ( ( B x. D ) x. ( * ` ( B x. D ) ) ) e. CC )
29	26 28	eqeltrd	|- ( ph -> ( ( abs ` ( B x. D ) ) ^ 2 ) e. CC )
30	20 29	addcld	|- ( ph -> ( ( ( abs ` ( A x. C ) ) ^ 2 ) + ( ( abs ` ( B x. D ) ) ^ 2 ) ) e. CC )
31	13	cjcld	|- ( ph -> ( * ` A ) e. CC )
32	31 15	mulcld	|- ( ph -> ( ( * ` A ) x. C ) e. CC )
33	22	cjcld	|- ( ph -> ( * ` B ) e. CC )
34	33 24	mulcld	|- ( ph -> ( ( * ` B ) x. D ) e. CC )
35	32 34	mulcld	|- ( ph -> ( ( ( * ` A ) x. C ) x. ( ( * ` B ) x. D ) ) e. CC )
36	15	cjcld	|- ( ph -> ( * ` C ) e. CC )
37	22 36	mulcld	|- ( ph -> ( B x. ( * ` C ) ) e. CC )
38	24	cjcld	|- ( ph -> ( * ` D ) e. CC )
39	13 38	mulcld	|- ( ph -> ( A x. ( * ` D ) ) e. CC )
40	37 39	mulcld	|- ( ph -> ( ( B x. ( * ` C ) ) x. ( A x. ( * ` D ) ) ) e. CC )
41	35 40	addcld	|- ( ph -> ( ( ( ( * ` A ) x. C ) x. ( ( * ` B ) x. D ) ) + ( ( B x. ( * ` C ) ) x. ( A x. ( * ` D ) ) ) ) e. CC )
42	13 24	mulcld	|- ( ph -> ( A x. D ) e. CC )
43	42	absvalsqd	|- ( ph -> ( ( abs ` ( A x. D ) ) ^ 2 ) = ( ( A x. D ) x. ( * ` ( A x. D ) ) ) )
44	42	cjcld	|- ( ph -> ( * ` ( A x. D ) ) e. CC )
45	42 44	mulcld	|- ( ph -> ( ( A x. D ) x. ( * ` ( A x. D ) ) ) e. CC )
46	43 45	eqeltrd	|- ( ph -> ( ( abs ` ( A x. D ) ) ^ 2 ) e. CC )
47	22 15	mulcld	|- ( ph -> ( B x. C ) e. CC )
48	47	absvalsqd	|- ( ph -> ( ( abs ` ( B x. C ) ) ^ 2 ) = ( ( B x. C ) x. ( * ` ( B x. C ) ) ) )
49	47	cjcld	|- ( ph -> ( * ` ( B x. C ) ) e. CC )
50	47 49	mulcld	|- ( ph -> ( ( B x. C ) x. ( * ` ( B x. C ) ) ) e. CC )
51	48 50	eqeltrd	|- ( ph -> ( ( abs ` ( B x. C ) ) ^ 2 ) e. CC )
52	46 51	addcld	|- ( ph -> ( ( ( abs ` ( A x. D ) ) ^ 2 ) + ( ( abs ` ( B x. C ) ) ^ 2 ) ) e. CC )
53	30 41 52	ppncand	|- ( ph -> ( ( ( ( ( abs ` ( A x. C ) ) ^ 2 ) + ( ( abs ` ( B x. D ) ) ^ 2 ) ) + ( ( ( ( * ` A ) x. C ) x. ( ( * ` B ) x. D ) ) + ( ( B x. ( * ` C ) ) x. ( A x. ( * ` D ) ) ) ) ) + ( ( ( ( abs ` ( A x. D ) ) ^ 2 ) + ( ( abs ` ( B x. C ) ) ^ 2 ) ) - ( ( ( ( * ` A ) x. C ) x. ( ( * ` B ) x. D ) ) + ( ( B x. ( * ` C ) ) x. ( A x. ( * ` D ) ) ) ) ) ) = ( ( ( ( abs ` ( A x. C ) ) ^ 2 ) + ( ( abs ` ( B x. D ) ) ^ 2 ) ) + ( ( ( abs ` ( A x. D ) ) ^ 2 ) + ( ( abs ` ( B x. C ) ) ^ 2 ) ) ) )
54	22 38	mulcld	|- ( ph -> ( B x. ( * ` D ) ) e. CC )
55	32 54	addcld	|- ( ph -> ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) e. CC )
56	55	absvalsqd	|- ( ph -> ( ( abs ` ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) ) ^ 2 ) = ( ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) x. ( * ` ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) ) ) )
57	32 54	cjaddd	|- ( ph -> ( * ` ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) ) = ( ( * ` ( ( * ` A ) x. C ) ) + ( * ` ( B x. ( * ` D ) ) ) ) )
58	31 15	cjmuld	|- ( ph -> ( * ` ( ( * ` A ) x. C ) ) = ( ( * ` ( * ` A ) ) x. ( * ` C ) ) )
59	13	cjcjd	|- ( ph -> ( * ` ( * ` A ) ) = A )
60	59	oveq1d	|- ( ph -> ( ( * ` ( * ` A ) ) x. ( * ` C ) ) = ( A x. ( * ` C ) ) )
61	58 60	eqtrd	|- ( ph -> ( * ` ( ( * ` A ) x. C ) ) = ( A x. ( * ` C ) ) )
62	22 38	cjmuld	|- ( ph -> ( * ` ( B x. ( * ` D ) ) ) = ( ( * ` B ) x. ( * ` ( * ` D ) ) ) )
63	24	cjcjd	|- ( ph -> ( * ` ( * ` D ) ) = D )
64	63	oveq2d	|- ( ph -> ( ( * ` B ) x. ( * ` ( * ` D ) ) ) = ( ( * ` B ) x. D ) )
65	62 64	eqtrd	|- ( ph -> ( * ` ( B x. ( * ` D ) ) ) = ( ( * ` B ) x. D ) )
66	61 65	oveq12d	|- ( ph -> ( ( * ` ( ( * ` A ) x. C ) ) + ( * ` ( B x. ( * ` D ) ) ) ) = ( ( A x. ( * ` C ) ) + ( ( * ` B ) x. D ) ) )
67	57 66	eqtrd	|- ( ph -> ( * ` ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) ) = ( ( A x. ( * ` C ) ) + ( ( * ` B ) x. D ) ) )
68	67	oveq2d	|- ( ph -> ( ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) x. ( * ` ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) ) ) = ( ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) x. ( ( A x. ( * ` C ) ) + ( ( * ` B ) x. D ) ) ) )
69	13 36	mulcld	|- ( ph -> ( A x. ( * ` C ) ) e. CC )
70	32 69 34	adddid	|- ( ph -> ( ( ( * ` A ) x. C ) x. ( ( A x. ( * ` C ) ) + ( ( * ` B ) x. D ) ) ) = ( ( ( ( * ` A ) x. C ) x. ( A x. ( * ` C ) ) ) + ( ( ( * ` A ) x. C ) x. ( ( * ` B ) x. D ) ) ) )
71	15 31 13 36	mul4d	|- ( ph -> ( ( C x. ( * ` A ) ) x. ( A x. ( * ` C ) ) ) = ( ( C x. A ) x. ( ( * ` A ) x. ( * ` C ) ) ) )
72	31 15	mulcomd	|- ( ph -> ( ( * ` A ) x. C ) = ( C x. ( * ` A ) ) )
73	72	oveq1d	|- ( ph -> ( ( ( * ` A ) x. C ) x. ( A x. ( * ` C ) ) ) = ( ( C x. ( * ` A ) ) x. ( A x. ( * ` C ) ) ) )
74	13 15	mulcomd	|- ( ph -> ( A x. C ) = ( C x. A ) )
75	13 15	cjmuld	|- ( ph -> ( * ` ( A x. C ) ) = ( ( * ` A ) x. ( * ` C ) ) )
76	74 75	oveq12d	|- ( ph -> ( ( A x. C ) x. ( * ` ( A x. C ) ) ) = ( ( C x. A ) x. ( ( * ` A ) x. ( * ` C ) ) ) )
77	71 73 76	3eqtr4d	|- ( ph -> ( ( ( * ` A ) x. C ) x. ( A x. ( * ` C ) ) ) = ( ( A x. C ) x. ( * ` ( A x. C ) ) ) )
78	77 17	eqtr4d	|- ( ph -> ( ( ( * ` A ) x. C ) x. ( A x. ( * ` C ) ) ) = ( ( abs ` ( A x. C ) ) ^ 2 ) )
79	78	oveq1d	|- ( ph -> ( ( ( ( * ` A ) x. C ) x. ( A x. ( * ` C ) ) ) + ( ( ( * ` A ) x. C ) x. ( ( * ` B ) x. D ) ) ) = ( ( ( abs ` ( A x. C ) ) ^ 2 ) + ( ( ( * ` A ) x. C ) x. ( ( * ` B ) x. D ) ) ) )
80	70 79	eqtrd	|- ( ph -> ( ( ( * ` A ) x. C ) x. ( ( A x. ( * ` C ) ) + ( ( * ` B ) x. D ) ) ) = ( ( ( abs ` ( A x. C ) ) ^ 2 ) + ( ( ( * ` A ) x. C ) x. ( ( * ` B ) x. D ) ) ) )
81	54 69 34	adddid	|- ( ph -> ( ( B x. ( * ` D ) ) x. ( ( A x. ( * ` C ) ) + ( ( * ` B ) x. D ) ) ) = ( ( ( B x. ( * ` D ) ) x. ( A x. ( * ` C ) ) ) + ( ( B x. ( * ` D ) ) x. ( ( * ` B ) x. D ) ) ) )
82	13 36	mulcomd	|- ( ph -> ( A x. ( * ` C ) ) = ( ( * ` C ) x. A ) )
83	82	oveq2d	|- ( ph -> ( ( B x. ( * ` D ) ) x. ( A x. ( * ` C ) ) ) = ( ( B x. ( * ` D ) ) x. ( ( * ` C ) x. A ) ) )
84	22 38 36 13	mul4d	|- ( ph -> ( ( B x. ( * ` D ) ) x. ( ( * ` C ) x. A ) ) = ( ( B x. ( * ` C ) ) x. ( ( * ` D ) x. A ) ) )
85	38 13	mulcomd	|- ( ph -> ( ( * ` D ) x. A ) = ( A x. ( * ` D ) ) )
86	85	oveq2d	|- ( ph -> ( ( B x. ( * ` C ) ) x. ( ( * ` D ) x. A ) ) = ( ( B x. ( * ` C ) ) x. ( A x. ( * ` D ) ) ) )
87	83 84 86	3eqtrd	|- ( ph -> ( ( B x. ( * ` D ) ) x. ( A x. ( * ` C ) ) ) = ( ( B x. ( * ` C ) ) x. ( A x. ( * ` D ) ) ) )
88	22 38 24 33	mul4d	|- ( ph -> ( ( B x. ( * ` D ) ) x. ( D x. ( * ` B ) ) ) = ( ( B x. D ) x. ( ( * ` D ) x. ( * ` B ) ) ) )
89	33 24	mulcomd	|- ( ph -> ( ( * ` B ) x. D ) = ( D x. ( * ` B ) ) )
90	89	oveq2d	|- ( ph -> ( ( B x. ( * ` D ) ) x. ( ( * ` B ) x. D ) ) = ( ( B x. ( * ` D ) ) x. ( D x. ( * ` B ) ) ) )
91	22 24	cjmuld	|- ( ph -> ( * ` ( B x. D ) ) = ( ( * ` B ) x. ( * ` D ) ) )
92	33 38	mulcomd	|- ( ph -> ( ( * ` B ) x. ( * ` D ) ) = ( ( * ` D ) x. ( * ` B ) ) )
93	91 92	eqtrd	|- ( ph -> ( * ` ( B x. D ) ) = ( ( * ` D ) x. ( * ` B ) ) )
94	93	oveq2d	|- ( ph -> ( ( B x. D ) x. ( * ` ( B x. D ) ) ) = ( ( B x. D ) x. ( ( * ` D ) x. ( * ` B ) ) ) )
95	88 90 94	3eqtr4d	|- ( ph -> ( ( B x. ( * ` D ) ) x. ( ( * ` B ) x. D ) ) = ( ( B x. D ) x. ( * ` ( B x. D ) ) ) )
96	95 26	eqtr4d	|- ( ph -> ( ( B x. ( * ` D ) ) x. ( ( * ` B ) x. D ) ) = ( ( abs ` ( B x. D ) ) ^ 2 ) )
97	87 96	oveq12d	|- ( ph -> ( ( ( B x. ( * ` D ) ) x. ( A x. ( * ` C ) ) ) + ( ( B x. ( * ` D ) ) x. ( ( * ` B ) x. D ) ) ) = ( ( ( B x. ( * ` C ) ) x. ( A x. ( * ` D ) ) ) + ( ( abs ` ( B x. D ) ) ^ 2 ) ) )
98	81 97	eqtrd	|- ( ph -> ( ( B x. ( * ` D ) ) x. ( ( A x. ( * ` C ) ) + ( ( * ` B ) x. D ) ) ) = ( ( ( B x. ( * ` C ) ) x. ( A x. ( * ` D ) ) ) + ( ( abs ` ( B x. D ) ) ^ 2 ) ) )
99	80 98	oveq12d	|- ( ph -> ( ( ( ( * ` A ) x. C ) x. ( ( A x. ( * ` C ) ) + ( ( * ` B ) x. D ) ) ) + ( ( B x. ( * ` D ) ) x. ( ( A x. ( * ` C ) ) + ( ( * ` B ) x. D ) ) ) ) = ( ( ( ( abs ` ( A x. C ) ) ^ 2 ) + ( ( ( * ` A ) x. C ) x. ( ( * ` B ) x. D ) ) ) + ( ( ( B x. ( * ` C ) ) x. ( A x. ( * ` D ) ) ) + ( ( abs ` ( B x. D ) ) ^ 2 ) ) ) )
100	69 34	addcld	|- ( ph -> ( ( A x. ( * ` C ) ) + ( ( * ` B ) x. D ) ) e. CC )
101	32 54 100	adddird	|- ( ph -> ( ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) x. ( ( A x. ( * ` C ) ) + ( ( * ` B ) x. D ) ) ) = ( ( ( ( * ` A ) x. C ) x. ( ( A x. ( * ` C ) ) + ( ( * ` B ) x. D ) ) ) + ( ( B x. ( * ` D ) ) x. ( ( A x. ( * ` C ) ) + ( ( * ` B ) x. D ) ) ) ) )
102	20 29 35 40	add42d	|- ( ph -> ( ( ( ( abs ` ( A x. C ) ) ^ 2 ) + ( ( abs ` ( B x. D ) ) ^ 2 ) ) + ( ( ( ( * ` A ) x. C ) x. ( ( * ` B ) x. D ) ) + ( ( B x. ( * ` C ) ) x. ( A x. ( * ` D ) ) ) ) ) = ( ( ( ( abs ` ( A x. C ) ) ^ 2 ) + ( ( ( * ` A ) x. C ) x. ( ( * ` B ) x. D ) ) ) + ( ( ( B x. ( * ` C ) ) x. ( A x. ( * ` D ) ) ) + ( ( abs ` ( B x. D ) ) ^ 2 ) ) ) )
103	99 101 102	3eqtr4d	|- ( ph -> ( ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) x. ( ( A x. ( * ` C ) ) + ( ( * ` B ) x. D ) ) ) = ( ( ( ( abs ` ( A x. C ) ) ^ 2 ) + ( ( abs ` ( B x. D ) ) ^ 2 ) ) + ( ( ( ( * ` A ) x. C ) x. ( ( * ` B ) x. D ) ) + ( ( B x. ( * ` C ) ) x. ( A x. ( * ` D ) ) ) ) ) )
104	56 68 103	3eqtrd	|- ( ph -> ( ( abs ` ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) ) ^ 2 ) = ( ( ( ( abs ` ( A x. C ) ) ^ 2 ) + ( ( abs ` ( B x. D ) ) ^ 2 ) ) + ( ( ( ( * ` A ) x. C ) x. ( ( * ` B ) x. D ) ) + ( ( B x. ( * ` C ) ) x. ( A x. ( * ` D ) ) ) ) ) )
105	31 24	mulcld	|- ( ph -> ( ( * ` A ) x. D ) e. CC )
106	105 37	subcld	|- ( ph -> ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) e. CC )
107	106	absvalsqd	|- ( ph -> ( ( abs ` ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) ) ^ 2 ) = ( ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) x. ( * ` ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) ) ) )
108		cjsub	|- ( ( ( ( * ` A ) x. D ) e. CC /\ ( B x. ( * ` C ) ) e. CC ) -> ( * ` ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) ) = ( ( * ` ( ( * ` A ) x. D ) ) - ( * ` ( B x. ( * ` C ) ) ) ) )
109	105 37 108	syl2anc	|- ( ph -> ( * ` ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) ) = ( ( * ` ( ( * ` A ) x. D ) ) - ( * ` ( B x. ( * ` C ) ) ) ) )
110	31 24	cjmuld	|- ( ph -> ( * ` ( ( * ` A ) x. D ) ) = ( ( * ` ( * ` A ) ) x. ( * ` D ) ) )
111	59	oveq1d	|- ( ph -> ( ( * ` ( * ` A ) ) x. ( * ` D ) ) = ( A x. ( * ` D ) ) )
112	110 111	eqtrd	|- ( ph -> ( * ` ( ( * ` A ) x. D ) ) = ( A x. ( * ` D ) ) )
113	22 36	cjmuld	|- ( ph -> ( * ` ( B x. ( * ` C ) ) ) = ( ( * ` B ) x. ( * ` ( * ` C ) ) ) )
114	15	cjcjd	|- ( ph -> ( * ` ( * ` C ) ) = C )
115	114	oveq2d	|- ( ph -> ( ( * ` B ) x. ( * ` ( * ` C ) ) ) = ( ( * ` B ) x. C ) )
116	113 115	eqtrd	|- ( ph -> ( * ` ( B x. ( * ` C ) ) ) = ( ( * ` B ) x. C ) )
117	112 116	oveq12d	|- ( ph -> ( ( * ` ( ( * ` A ) x. D ) ) - ( * ` ( B x. ( * ` C ) ) ) ) = ( ( A x. ( * ` D ) ) - ( ( * ` B ) x. C ) ) )
118	109 117	eqtrd	|- ( ph -> ( * ` ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) ) = ( ( A x. ( * ` D ) ) - ( ( * ` B ) x. C ) ) )
119	118	oveq2d	|- ( ph -> ( ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) x. ( * ` ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) ) ) = ( ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) x. ( ( A x. ( * ` D ) ) - ( ( * ` B ) x. C ) ) ) )
120	33 15	mulcld	|- ( ph -> ( ( * ` B ) x. C ) e. CC )
121	39 120	subcld	|- ( ph -> ( ( A x. ( * ` D ) ) - ( ( * ` B ) x. C ) ) e. CC )
122	105 37 121	subdird	|- ( ph -> ( ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) x. ( ( A x. ( * ` D ) ) - ( ( * ` B ) x. C ) ) ) = ( ( ( ( * ` A ) x. D ) x. ( ( A x. ( * ` D ) ) - ( ( * ` B ) x. C ) ) ) - ( ( B x. ( * ` C ) ) x. ( ( A x. ( * ` D ) ) - ( ( * ` B ) x. C ) ) ) ) )
123	105 39 120	subdid	|- ( ph -> ( ( ( * ` A ) x. D ) x. ( ( A x. ( * ` D ) ) - ( ( * ` B ) x. C ) ) ) = ( ( ( ( * ` A ) x. D ) x. ( A x. ( * ` D ) ) ) - ( ( ( * ` A ) x. D ) x. ( ( * ` B ) x. C ) ) ) )
124	24 31 13 38	mul4d	|- ( ph -> ( ( D x. ( * ` A ) ) x. ( A x. ( * ` D ) ) ) = ( ( D x. A ) x. ( ( * ` A ) x. ( * ` D ) ) ) )
125	31 24	mulcomd	|- ( ph -> ( ( * ` A ) x. D ) = ( D x. ( * ` A ) ) )
126	125	oveq1d	|- ( ph -> ( ( ( * ` A ) x. D ) x. ( A x. ( * ` D ) ) ) = ( ( D x. ( * ` A ) ) x. ( A x. ( * ` D ) ) ) )
127	13 24	mulcomd	|- ( ph -> ( A x. D ) = ( D x. A ) )
128	13 24	cjmuld	|- ( ph -> ( * ` ( A x. D ) ) = ( ( * ` A ) x. ( * ` D ) ) )
129	127 128	oveq12d	|- ( ph -> ( ( A x. D ) x. ( * ` ( A x. D ) ) ) = ( ( D x. A ) x. ( ( * ` A ) x. ( * ` D ) ) ) )
130	124 126 129	3eqtr4d	|- ( ph -> ( ( ( * ` A ) x. D ) x. ( A x. ( * ` D ) ) ) = ( ( A x. D ) x. ( * ` ( A x. D ) ) ) )
131	130 43	eqtr4d	|- ( ph -> ( ( ( * ` A ) x. D ) x. ( A x. ( * ` D ) ) ) = ( ( abs ` ( A x. D ) ) ^ 2 ) )
132	33 15	mulcomd	|- ( ph -> ( ( * ` B ) x. C ) = ( C x. ( * ` B ) ) )
133	132	oveq2d	|- ( ph -> ( ( ( * ` A ) x. D ) x. ( ( * ` B ) x. C ) ) = ( ( ( * ` A ) x. D ) x. ( C x. ( * ` B ) ) ) )
134	31 24 15 33	mul4d	|- ( ph -> ( ( ( * ` A ) x. D ) x. ( C x. ( * ` B ) ) ) = ( ( ( * ` A ) x. C ) x. ( D x. ( * ` B ) ) ) )
135	24 33	mulcomd	|- ( ph -> ( D x. ( * ` B ) ) = ( ( * ` B ) x. D ) )
136	135	oveq2d	|- ( ph -> ( ( ( * ` A ) x. C ) x. ( D x. ( * ` B ) ) ) = ( ( ( * ` A ) x. C ) x. ( ( * ` B ) x. D ) ) )
137	133 134 136	3eqtrd	|- ( ph -> ( ( ( * ` A ) x. D ) x. ( ( * ` B ) x. C ) ) = ( ( ( * ` A ) x. C ) x. ( ( * ` B ) x. D ) ) )
138	131 137	oveq12d	|- ( ph -> ( ( ( ( * ` A ) x. D ) x. ( A x. ( * ` D ) ) ) - ( ( ( * ` A ) x. D ) x. ( ( * ` B ) x. C ) ) ) = ( ( ( abs ` ( A x. D ) ) ^ 2 ) - ( ( ( * ` A ) x. C ) x. ( ( * ` B ) x. D ) ) ) )
139	123 138	eqtrd	|- ( ph -> ( ( ( * ` A ) x. D ) x. ( ( A x. ( * ` D ) ) - ( ( * ` B ) x. C ) ) ) = ( ( ( abs ` ( A x. D ) ) ^ 2 ) - ( ( ( * ` A ) x. C ) x. ( ( * ` B ) x. D ) ) ) )
140	37 39 120	subdid	|- ( ph -> ( ( B x. ( * ` C ) ) x. ( ( A x. ( * ` D ) ) - ( ( * ` B ) x. C ) ) ) = ( ( ( B x. ( * ` C ) ) x. ( A x. ( * ` D ) ) ) - ( ( B x. ( * ` C ) ) x. ( ( * ` B ) x. C ) ) ) )
141	132	oveq2d	|- ( ph -> ( ( B x. ( * ` C ) ) x. ( ( * ` B ) x. C ) ) = ( ( B x. ( * ` C ) ) x. ( C x. ( * ` B ) ) ) )
142	22 36 15 33	mul4d	|- ( ph -> ( ( B x. ( * ` C ) ) x. ( C x. ( * ` B ) ) ) = ( ( B x. C ) x. ( ( * ` C ) x. ( * ` B ) ) ) )
143	36 33	mulcomd	|- ( ph -> ( ( * ` C ) x. ( * ` B ) ) = ( ( * ` B ) x. ( * ` C ) ) )
144	22 15	cjmuld	|- ( ph -> ( * ` ( B x. C ) ) = ( ( * ` B ) x. ( * ` C ) ) )
145	143 144	eqtr4d	|- ( ph -> ( ( * ` C ) x. ( * ` B ) ) = ( * ` ( B x. C ) ) )
146	145	oveq2d	|- ( ph -> ( ( B x. C ) x. ( ( * ` C ) x. ( * ` B ) ) ) = ( ( B x. C ) x. ( * ` ( B x. C ) ) ) )
147	141 142 146	3eqtrd	|- ( ph -> ( ( B x. ( * ` C ) ) x. ( ( * ` B ) x. C ) ) = ( ( B x. C ) x. ( * ` ( B x. C ) ) ) )
148	147 48	eqtr4d	|- ( ph -> ( ( B x. ( * ` C ) ) x. ( ( * ` B ) x. C ) ) = ( ( abs ` ( B x. C ) ) ^ 2 ) )
149	148	oveq2d	|- ( ph -> ( ( ( B x. ( * ` C ) ) x. ( A x. ( * ` D ) ) ) - ( ( B x. ( * ` C ) ) x. ( ( * ` B ) x. C ) ) ) = ( ( ( B x. ( * ` C ) ) x. ( A x. ( * ` D ) ) ) - ( ( abs ` ( B x. C ) ) ^ 2 ) ) )
150	140 149	eqtrd	|- ( ph -> ( ( B x. ( * ` C ) ) x. ( ( A x. ( * ` D ) ) - ( ( * ` B ) x. C ) ) ) = ( ( ( B x. ( * ` C ) ) x. ( A x. ( * ` D ) ) ) - ( ( abs ` ( B x. C ) ) ^ 2 ) ) )
151	139 150	oveq12d	|- ( ph -> ( ( ( ( * ` A ) x. D ) x. ( ( A x. ( * ` D ) ) - ( ( * ` B ) x. C ) ) ) - ( ( B x. ( * ` C ) ) x. ( ( A x. ( * ` D ) ) - ( ( * ` B ) x. C ) ) ) ) = ( ( ( ( abs ` ( A x. D ) ) ^ 2 ) - ( ( ( * ` A ) x. C ) x. ( ( * ` B ) x. D ) ) ) - ( ( ( B x. ( * ` C ) ) x. ( A x. ( * ` D ) ) ) - ( ( abs ` ( B x. C ) ) ^ 2 ) ) ) )
152	46 35 40 51	subadd4d	|- ( ph -> ( ( ( ( abs ` ( A x. D ) ) ^ 2 ) - ( ( ( * ` A ) x. C ) x. ( ( * ` B ) x. D ) ) ) - ( ( ( B x. ( * ` C ) ) x. ( A x. ( * ` D ) ) ) - ( ( abs ` ( B x. C ) ) ^ 2 ) ) ) = ( ( ( ( abs ` ( A x. D ) ) ^ 2 ) + ( ( abs ` ( B x. C ) ) ^ 2 ) ) - ( ( ( ( * ` A ) x. C ) x. ( ( * ` B ) x. D ) ) + ( ( B x. ( * ` C ) ) x. ( A x. ( * ` D ) ) ) ) ) )
153	122 151 152	3eqtrd	|- ( ph -> ( ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) x. ( ( A x. ( * ` D ) ) - ( ( * ` B ) x. C ) ) ) = ( ( ( ( abs ` ( A x. D ) ) ^ 2 ) + ( ( abs ` ( B x. C ) ) ^ 2 ) ) - ( ( ( ( * ` A ) x. C ) x. ( ( * ` B ) x. D ) ) + ( ( B x. ( * ` C ) ) x. ( A x. ( * ` D ) ) ) ) ) )
154	107 119 153	3eqtrd	|- ( ph -> ( ( abs ` ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) ) ^ 2 ) = ( ( ( ( abs ` ( A x. D ) ) ^ 2 ) + ( ( abs ` ( B x. C ) ) ^ 2 ) ) - ( ( ( ( * ` A ) x. C ) x. ( ( * ` B ) x. D ) ) + ( ( B x. ( * ` C ) ) x. ( A x. ( * ` D ) ) ) ) ) )
155	104 154	oveq12d	|- ( ph -> ( ( ( abs ` ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) ) ^ 2 ) + ( ( abs ` ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) ) ^ 2 ) ) = ( ( ( ( ( abs ` ( A x. C ) ) ^ 2 ) + ( ( abs ` ( B x. D ) ) ^ 2 ) ) + ( ( ( ( * ` A ) x. C ) x. ( ( * ` B ) x. D ) ) + ( ( B x. ( * ` C ) ) x. ( A x. ( * ` D ) ) ) ) ) + ( ( ( ( abs ` ( A x. D ) ) ^ 2 ) + ( ( abs ` ( B x. C ) ) ^ 2 ) ) - ( ( ( ( * ` A ) x. C ) x. ( ( * ` B ) x. D ) ) + ( ( B x. ( * ` C ) ) x. ( A x. ( * ` D ) ) ) ) ) ) )
156	13 31	mulcld	|- ( ph -> ( A x. ( * ` A ) ) e. CC )
157	22 33	mulcld	|- ( ph -> ( B x. ( * ` B ) ) e. CC )
158	15 36	mulcld	|- ( ph -> ( C x. ( * ` C ) ) e. CC )
159	24 38	mulcld	|- ( ph -> ( D x. ( * ` D ) ) e. CC )
160	158 159	addcld	|- ( ph -> ( ( C x. ( * ` C ) ) + ( D x. ( * ` D ) ) ) e. CC )
161	156 157 160	adddird	|- ( ph -> ( ( ( A x. ( * ` A ) ) + ( B x. ( * ` B ) ) ) x. ( ( C x. ( * ` C ) ) + ( D x. ( * ` D ) ) ) ) = ( ( ( A x. ( * ` A ) ) x. ( ( C x. ( * ` C ) ) + ( D x. ( * ` D ) ) ) ) + ( ( B x. ( * ` B ) ) x. ( ( C x. ( * ` C ) ) + ( D x. ( * ` D ) ) ) ) ) )
162	75	oveq2d	|- ( ph -> ( ( A x. C ) x. ( * ` ( A x. C ) ) ) = ( ( A x. C ) x. ( ( * ` A ) x. ( * ` C ) ) ) )
163	13 15 31 36	mul4d	|- ( ph -> ( ( A x. C ) x. ( ( * ` A ) x. ( * ` C ) ) ) = ( ( A x. ( * ` A ) ) x. ( C x. ( * ` C ) ) ) )
164	17 162 163	3eqtrd	|- ( ph -> ( ( abs ` ( A x. C ) ) ^ 2 ) = ( ( A x. ( * ` A ) ) x. ( C x. ( * ` C ) ) ) )
165	128	oveq2d	|- ( ph -> ( ( A x. D ) x. ( * ` ( A x. D ) ) ) = ( ( A x. D ) x. ( ( * ` A ) x. ( * ` D ) ) ) )
166	13 24 31 38	mul4d	|- ( ph -> ( ( A x. D ) x. ( ( * ` A ) x. ( * ` D ) ) ) = ( ( A x. ( * ` A ) ) x. ( D x. ( * ` D ) ) ) )
167	43 165 166	3eqtrd	|- ( ph -> ( ( abs ` ( A x. D ) ) ^ 2 ) = ( ( A x. ( * ` A ) ) x. ( D x. ( * ` D ) ) ) )
168	164 167	oveq12d	|- ( ph -> ( ( ( abs ` ( A x. C ) ) ^ 2 ) + ( ( abs ` ( A x. D ) ) ^ 2 ) ) = ( ( ( A x. ( * ` A ) ) x. ( C x. ( * ` C ) ) ) + ( ( A x. ( * ` A ) ) x. ( D x. ( * ` D ) ) ) ) )
169	156 158 159	adddid	|- ( ph -> ( ( A x. ( * ` A ) ) x. ( ( C x. ( * ` C ) ) + ( D x. ( * ` D ) ) ) ) = ( ( ( A x. ( * ` A ) ) x. ( C x. ( * ` C ) ) ) + ( ( A x. ( * ` A ) ) x. ( D x. ( * ` D ) ) ) ) )
170	168 169	eqtr4d	|- ( ph -> ( ( ( abs ` ( A x. C ) ) ^ 2 ) + ( ( abs ` ( A x. D ) ) ^ 2 ) ) = ( ( A x. ( * ` A ) ) x. ( ( C x. ( * ` C ) ) + ( D x. ( * ` D ) ) ) ) )
171	144	oveq2d	|- ( ph -> ( ( B x. C ) x. ( * ` ( B x. C ) ) ) = ( ( B x. C ) x. ( ( * ` B ) x. ( * ` C ) ) ) )
172	22 15 33 36	mul4d	|- ( ph -> ( ( B x. C ) x. ( ( * ` B ) x. ( * ` C ) ) ) = ( ( B x. ( * ` B ) ) x. ( C x. ( * ` C ) ) ) )
173	48 171 172	3eqtrd	|- ( ph -> ( ( abs ` ( B x. C ) ) ^ 2 ) = ( ( B x. ( * ` B ) ) x. ( C x. ( * ` C ) ) ) )
174	91	oveq2d	|- ( ph -> ( ( B x. D ) x. ( * ` ( B x. D ) ) ) = ( ( B x. D ) x. ( ( * ` B ) x. ( * ` D ) ) ) )
175	22 24 33 38	mul4d	|- ( ph -> ( ( B x. D ) x. ( ( * ` B ) x. ( * ` D ) ) ) = ( ( B x. ( * ` B ) ) x. ( D x. ( * ` D ) ) ) )
176	26 174 175	3eqtrd	|- ( ph -> ( ( abs ` ( B x. D ) ) ^ 2 ) = ( ( B x. ( * ` B ) ) x. ( D x. ( * ` D ) ) ) )
177	173 176	oveq12d	|- ( ph -> ( ( ( abs ` ( B x. C ) ) ^ 2 ) + ( ( abs ` ( B x. D ) ) ^ 2 ) ) = ( ( ( B x. ( * ` B ) ) x. ( C x. ( * ` C ) ) ) + ( ( B x. ( * ` B ) ) x. ( D x. ( * ` D ) ) ) ) )
178	157 158 159	adddid	|- ( ph -> ( ( B x. ( * ` B ) ) x. ( ( C x. ( * ` C ) ) + ( D x. ( * ` D ) ) ) ) = ( ( ( B x. ( * ` B ) ) x. ( C x. ( * ` C ) ) ) + ( ( B x. ( * ` B ) ) x. ( D x. ( * ` D ) ) ) ) )
179	177 178	eqtr4d	|- ( ph -> ( ( ( abs ` ( B x. C ) ) ^ 2 ) + ( ( abs ` ( B x. D ) ) ^ 2 ) ) = ( ( B x. ( * ` B ) ) x. ( ( C x. ( * ` C ) ) + ( D x. ( * ` D ) ) ) ) )
180	170 179	oveq12d	|- ( ph -> ( ( ( ( abs ` ( A x. C ) ) ^ 2 ) + ( ( abs ` ( A x. D ) ) ^ 2 ) ) + ( ( ( abs ` ( B x. C ) ) ^ 2 ) + ( ( abs ` ( B x. D ) ) ^ 2 ) ) ) = ( ( ( A x. ( * ` A ) ) x. ( ( C x. ( * ` C ) ) + ( D x. ( * ` D ) ) ) ) + ( ( B x. ( * ` B ) ) x. ( ( C x. ( * ` C ) ) + ( D x. ( * ` D ) ) ) ) ) )
181	161 180	eqtr4d	|- ( ph -> ( ( ( A x. ( * ` A ) ) + ( B x. ( * ` B ) ) ) x. ( ( C x. ( * ` C ) ) + ( D x. ( * ` D ) ) ) ) = ( ( ( ( abs ` ( A x. C ) ) ^ 2 ) + ( ( abs ` ( A x. D ) ) ^ 2 ) ) + ( ( ( abs ` ( B x. C ) ) ^ 2 ) + ( ( abs ` ( B x. D ) ) ^ 2 ) ) ) )
182	13	absvalsqd	|- ( ph -> ( ( abs ` A ) ^ 2 ) = ( A x. ( * ` A ) ) )
183	22	absvalsqd	|- ( ph -> ( ( abs ` B ) ^ 2 ) = ( B x. ( * ` B ) ) )
184	182 183	oveq12d	|- ( ph -> ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) ) = ( ( A x. ( * ` A ) ) + ( B x. ( * ` B ) ) ) )
185	6 184	syl5eq	|- ( ph -> X = ( ( A x. ( * ` A ) ) + ( B x. ( * ` B ) ) ) )
186	15	absvalsqd	|- ( ph -> ( ( abs ` C ) ^ 2 ) = ( C x. ( * ` C ) ) )
187	24	absvalsqd	|- ( ph -> ( ( abs ` D ) ^ 2 ) = ( D x. ( * ` D ) ) )
188	186 187	oveq12d	|- ( ph -> ( ( ( abs ` C ) ^ 2 ) + ( ( abs ` D ) ^ 2 ) ) = ( ( C x. ( * ` C ) ) + ( D x. ( * ` D ) ) ) )
189	7 188	syl5eq	|- ( ph -> Y = ( ( C x. ( * ` C ) ) + ( D x. ( * ` D ) ) ) )
190	185 189	oveq12d	|- ( ph -> ( X x. Y ) = ( ( ( A x. ( * ` A ) ) + ( B x. ( * ` B ) ) ) x. ( ( C x. ( * ` C ) ) + ( D x. ( * ` D ) ) ) ) )
191	20 29 46 51	add42d	|- ( ph -> ( ( ( ( abs ` ( A x. C ) ) ^ 2 ) + ( ( abs ` ( B x. D ) ) ^ 2 ) ) + ( ( ( abs ` ( A x. D ) ) ^ 2 ) + ( ( abs ` ( B x. C ) ) ^ 2 ) ) ) = ( ( ( ( abs ` ( A x. C ) ) ^ 2 ) + ( ( abs ` ( A x. D ) ) ^ 2 ) ) + ( ( ( abs ` ( B x. C ) ) ^ 2 ) + ( ( abs ` ( B x. D ) ) ^ 2 ) ) ) )
192	181 190 191	3eqtr4d	|- ( ph -> ( X x. Y ) = ( ( ( ( abs ` ( A x. C ) ) ^ 2 ) + ( ( abs ` ( B x. D ) ) ^ 2 ) ) + ( ( ( abs ` ( A x. D ) ) ^ 2 ) + ( ( abs ` ( B x. C ) ) ^ 2 ) ) ) )
193	53 155 192	3eqtr4d	|- ( ph -> ( ( ( abs ` ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) ) ^ 2 ) + ( ( abs ` ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) ) ^ 2 ) ) = ( X x. Y ) )
194	193	oveq1d	|- ( ph -> ( ( ( ( abs ` ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) ) ^ 2 ) + ( ( abs ` ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) ) ^ 2 ) ) / ( M ^ 2 ) ) = ( ( X x. Y ) / ( M ^ 2 ) ) )
195	8	nncnd	|- ( ph -> M e. CC )
196	8	nnne0d	|- ( ph -> M =/= 0 )
197	55 195 196	absdivd	|- ( ph -> ( abs ` ( ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) / M ) ) = ( ( abs ` ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) ) / ( abs ` M ) ) )
198	8	nnred	|- ( ph -> M e. RR )
199	8	nnnn0d	|- ( ph -> M e. NN0 )
200	199	nn0ge0d	|- ( ph -> 0 <_ M )
201	198 200	absidd	|- ( ph -> ( abs ` M ) = M )
202	201	oveq2d	|- ( ph -> ( ( abs ` ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) ) / ( abs ` M ) ) = ( ( abs ` ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) ) / M ) )
203	197 202	eqtrd	|- ( ph -> ( abs ` ( ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) / M ) ) = ( ( abs ` ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) ) / M ) )
204	203	oveq1d	|- ( ph -> ( ( abs ` ( ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) / M ) ) ^ 2 ) = ( ( ( abs ` ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) ) / M ) ^ 2 ) )
205	55	abscld	|- ( ph -> ( abs ` ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) ) e. RR )
206	205	recnd	|- ( ph -> ( abs ` ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) ) e. CC )
207	206 195 196	sqdivd	|- ( ph -> ( ( ( abs ` ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) ) / M ) ^ 2 ) = ( ( ( abs ` ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) ) ^ 2 ) / ( M ^ 2 ) ) )
208	204 207	eqtrd	|- ( ph -> ( ( abs ` ( ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) / M ) ) ^ 2 ) = ( ( ( abs ` ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) ) ^ 2 ) / ( M ^ 2 ) ) )
209	106 195 196	absdivd	|- ( ph -> ( abs ` ( ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) / M ) ) = ( ( abs ` ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) ) / ( abs ` M ) ) )
210	201	oveq2d	|- ( ph -> ( ( abs ` ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) ) / ( abs ` M ) ) = ( ( abs ` ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) ) / M ) )
211	209 210	eqtrd	|- ( ph -> ( abs ` ( ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) / M ) ) = ( ( abs ` ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) ) / M ) )
212	211	oveq1d	|- ( ph -> ( ( abs ` ( ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) / M ) ) ^ 2 ) = ( ( ( abs ` ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) ) / M ) ^ 2 ) )
213	106	abscld	|- ( ph -> ( abs ` ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) ) e. RR )
214	213	recnd	|- ( ph -> ( abs ` ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) ) e. CC )
215	214 195 196	sqdivd	|- ( ph -> ( ( ( abs ` ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) ) / M ) ^ 2 ) = ( ( ( abs ` ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) ) ^ 2 ) / ( M ^ 2 ) ) )
216	212 215	eqtrd	|- ( ph -> ( ( abs ` ( ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) / M ) ) ^ 2 ) = ( ( ( abs ` ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) ) ^ 2 ) / ( M ^ 2 ) ) )
217	208 216	oveq12d	|- ( ph -> ( ( ( abs ` ( ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) / M ) ) ^ 2 ) + ( ( abs ` ( ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) / M ) ) ^ 2 ) ) = ( ( ( ( abs ` ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) ) ^ 2 ) / ( M ^ 2 ) ) + ( ( ( abs ` ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) ) ^ 2 ) / ( M ^ 2 ) ) ) )
218	30 41	addcld	|- ( ph -> ( ( ( ( abs ` ( A x. C ) ) ^ 2 ) + ( ( abs ` ( B x. D ) ) ^ 2 ) ) + ( ( ( ( * ` A ) x. C ) x. ( ( * ` B ) x. D ) ) + ( ( B x. ( * ` C ) ) x. ( A x. ( * ` D ) ) ) ) ) e. CC )
219	104 218	eqeltrd	|- ( ph -> ( ( abs ` ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) ) ^ 2 ) e. CC )
220	52 41	subcld	|- ( ph -> ( ( ( ( abs ` ( A x. D ) ) ^ 2 ) + ( ( abs ` ( B x. C ) ) ^ 2 ) ) - ( ( ( ( * ` A ) x. C ) x. ( ( * ` B ) x. D ) ) + ( ( B x. ( * ` C ) ) x. ( A x. ( * ` D ) ) ) ) ) e. CC )
221	154 220	eqeltrd	|- ( ph -> ( ( abs ` ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) ) ^ 2 ) e. CC )
222	8	nnsqcld	|- ( ph -> ( M ^ 2 ) e. NN )
223	222	nncnd	|- ( ph -> ( M ^ 2 ) e. CC )
224	222	nnne0d	|- ( ph -> ( M ^ 2 ) =/= 0 )
225	219 221 223 224	divdird	|- ( ph -> ( ( ( ( abs ` ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) ) ^ 2 ) + ( ( abs ` ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) ) ^ 2 ) ) / ( M ^ 2 ) ) = ( ( ( ( abs ` ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) ) ^ 2 ) / ( M ^ 2 ) ) + ( ( ( abs ` ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) ) ^ 2 ) / ( M ^ 2 ) ) ) )
226	217 225	eqtr4d	|- ( ph -> ( ( ( abs ` ( ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) / M ) ) ^ 2 ) + ( ( abs ` ( ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) / M ) ) ^ 2 ) ) = ( ( ( ( abs ` ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) ) ^ 2 ) + ( ( abs ` ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) ) ^ 2 ) ) / ( M ^ 2 ) ) )
227	182 156	eqeltrd	|- ( ph -> ( ( abs ` A ) ^ 2 ) e. CC )
228	183 157	eqeltrd	|- ( ph -> ( ( abs ` B ) ^ 2 ) e. CC )
229	227 228	addcld	|- ( ph -> ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) ) e. CC )
230	6 229	eqeltrid	|- ( ph -> X e. CC )
231	189 160	eqeltrd	|- ( ph -> Y e. CC )
232	230 195 231 195 196 196	divmuldivd	|- ( ph -> ( ( X / M ) x. ( Y / M ) ) = ( ( X x. Y ) / ( M x. M ) ) )
233	195	sqvald	|- ( ph -> ( M ^ 2 ) = ( M x. M ) )
234	233	oveq2d	|- ( ph -> ( ( X x. Y ) / ( M ^ 2 ) ) = ( ( X x. Y ) / ( M x. M ) ) )
235	232 234	eqtr4d	|- ( ph -> ( ( X / M ) x. ( Y / M ) ) = ( ( X x. Y ) / ( M ^ 2 ) ) )
236	194 226 235	3eqtr4d	|- ( ph -> ( ( ( abs ` ( ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) / M ) ) ^ 2 ) + ( ( abs ` ( ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) / M ) ) ^ 2 ) ) = ( ( X / M ) x. ( Y / M ) ) )
237	230 55	nncand	|- ( ph -> ( X - ( X - ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) ) ) = ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) )
238	156 157 32 54	addsub4d	|- ( ph -> ( ( ( A x. ( * ` A ) ) + ( B x. ( * ` B ) ) ) - ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) ) = ( ( ( A x. ( * ` A ) ) - ( ( * ` A ) x. C ) ) + ( ( B x. ( * ` B ) ) - ( B x. ( * ` D ) ) ) ) )
239	185	oveq1d	|- ( ph -> ( X - ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) ) = ( ( ( A x. ( * ` A ) ) + ( B x. ( * ` B ) ) ) - ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) ) )
240	31 13 15	subdid	|- ( ph -> ( ( * ` A ) x. ( A - C ) ) = ( ( ( * ` A ) x. A ) - ( ( * ` A ) x. C ) ) )
241	31 13	mulcomd	|- ( ph -> ( ( * ` A ) x. A ) = ( A x. ( * ` A ) ) )
242	241	oveq1d	|- ( ph -> ( ( ( * ` A ) x. A ) - ( ( * ` A ) x. C ) ) = ( ( A x. ( * ` A ) ) - ( ( * ` A ) x. C ) ) )
243	240 242	eqtrd	|- ( ph -> ( ( * ` A ) x. ( A - C ) ) = ( ( A x. ( * ` A ) ) - ( ( * ` A ) x. C ) ) )
244		cjsub	|- ( ( B e. CC /\ D e. CC ) -> ( * ` ( B - D ) ) = ( ( * ` B ) - ( * ` D ) ) )
245	22 24 244	syl2anc	|- ( ph -> ( * ` ( B - D ) ) = ( ( * ` B ) - ( * ` D ) ) )
246	245	oveq2d	|- ( ph -> ( B x. ( * ` ( B - D ) ) ) = ( B x. ( ( * ` B ) - ( * ` D ) ) ) )
247	22 33 38	subdid	|- ( ph -> ( B x. ( ( * ` B ) - ( * ` D ) ) ) = ( ( B x. ( * ` B ) ) - ( B x. ( * ` D ) ) ) )
248	246 247	eqtrd	|- ( ph -> ( B x. ( * ` ( B - D ) ) ) = ( ( B x. ( * ` B ) ) - ( B x. ( * ` D ) ) ) )
249	243 248	oveq12d	|- ( ph -> ( ( ( * ` A ) x. ( A - C ) ) + ( B x. ( * ` ( B - D ) ) ) ) = ( ( ( A x. ( * ` A ) ) - ( ( * ` A ) x. C ) ) + ( ( B x. ( * ` B ) ) - ( B x. ( * ` D ) ) ) ) )
250	238 239 249	3eqtr4d	|- ( ph -> ( X - ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) ) = ( ( ( * ` A ) x. ( A - C ) ) + ( B x. ( * ` ( B - D ) ) ) ) )
251	250	oveq2d	|- ( ph -> ( X - ( X - ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) ) ) = ( X - ( ( ( * ` A ) x. ( A - C ) ) + ( B x. ( * ` ( B - D ) ) ) ) ) )
252	237 251	eqtr3d	|- ( ph -> ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) = ( X - ( ( ( * ` A ) x. ( A - C ) ) + ( B x. ( * ` ( B - D ) ) ) ) ) )
253	252	oveq1d	|- ( ph -> ( ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) / M ) = ( ( X - ( ( ( * ` A ) x. ( A - C ) ) + ( B x. ( * ` ( B - D ) ) ) ) ) / M ) )
254	13 15	subcld	|- ( ph -> ( A - C ) e. CC )
255	31 254	mulcld	|- ( ph -> ( ( * ` A ) x. ( A - C ) ) e. CC )
256	22 24	subcld	|- ( ph -> ( B - D ) e. CC )
257	256	cjcld	|- ( ph -> ( * ` ( B - D ) ) e. CC )
258	22 257	mulcld	|- ( ph -> ( B x. ( * ` ( B - D ) ) ) e. CC )
259	255 258	addcld	|- ( ph -> ( ( ( * ` A ) x. ( A - C ) ) + ( B x. ( * ` ( B - D ) ) ) ) e. CC )
260	230 259 195 196	divsubdird	|- ( ph -> ( ( X - ( ( ( * ` A ) x. ( A - C ) ) + ( B x. ( * ` ( B - D ) ) ) ) ) / M ) = ( ( X / M ) - ( ( ( ( * ` A ) x. ( A - C ) ) + ( B x. ( * ` ( B - D ) ) ) ) / M ) ) )
261	255 258 195 196	divdird	|- ( ph -> ( ( ( ( * ` A ) x. ( A - C ) ) + ( B x. ( * ` ( B - D ) ) ) ) / M ) = ( ( ( ( * ` A ) x. ( A - C ) ) / M ) + ( ( B x. ( * ` ( B - D ) ) ) / M ) ) )
262	31 254 195 196	divassd	|- ( ph -> ( ( ( * ` A ) x. ( A - C ) ) / M ) = ( ( * ` A ) x. ( ( A - C ) / M ) ) )
263	22 257 195 196	divassd	|- ( ph -> ( ( B x. ( * ` ( B - D ) ) ) / M ) = ( B x. ( ( * ` ( B - D ) ) / M ) ) )
264	256 195 196	cjdivd	|- ( ph -> ( * ` ( ( B - D ) / M ) ) = ( ( * ` ( B - D ) ) / ( * ` M ) ) )
265	198	cjred	|- ( ph -> ( * ` M ) = M )
266	265	oveq2d	|- ( ph -> ( ( * ` ( B - D ) ) / ( * ` M ) ) = ( ( * ` ( B - D ) ) / M ) )
267	264 266	eqtrd	|- ( ph -> ( * ` ( ( B - D ) / M ) ) = ( ( * ` ( B - D ) ) / M ) )
268	267	oveq2d	|- ( ph -> ( B x. ( * ` ( ( B - D ) / M ) ) ) = ( B x. ( ( * ` ( B - D ) ) / M ) ) )
269	263 268	eqtr4d	|- ( ph -> ( ( B x. ( * ` ( B - D ) ) ) / M ) = ( B x. ( * ` ( ( B - D ) / M ) ) ) )
270	262 269	oveq12d	|- ( ph -> ( ( ( ( * ` A ) x. ( A - C ) ) / M ) + ( ( B x. ( * ` ( B - D ) ) ) / M ) ) = ( ( ( * ` A ) x. ( ( A - C ) / M ) ) + ( B x. ( * ` ( ( B - D ) / M ) ) ) ) )
271	261 270	eqtrd	|- ( ph -> ( ( ( ( * ` A ) x. ( A - C ) ) + ( B x. ( * ` ( B - D ) ) ) ) / M ) = ( ( ( * ` A ) x. ( ( A - C ) / M ) ) + ( B x. ( * ` ( ( B - D ) / M ) ) ) ) )
272	271	oveq2d	|- ( ph -> ( ( X / M ) - ( ( ( ( * ` A ) x. ( A - C ) ) + ( B x. ( * ` ( B - D ) ) ) ) / M ) ) = ( ( X / M ) - ( ( ( * ` A ) x. ( ( A - C ) / M ) ) + ( B x. ( * ` ( ( B - D ) / M ) ) ) ) ) )
273	253 260 272	3eqtrd	|- ( ph -> ( ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) / M ) = ( ( X / M ) - ( ( ( * ` A ) x. ( ( A - C ) / M ) ) + ( B x. ( * ` ( ( B - D ) / M ) ) ) ) ) )
274	11	nn0zd	|- ( ph -> ( X / M ) e. ZZ )
275		zgz	|- ( ( X / M ) e. ZZ -> ( X / M ) e. Z[i] )
276	274 275	syl	|- ( ph -> ( X / M ) e. Z[i] )
277		gzcjcl	|- ( A e. Z[i] -> ( * ` A ) e. Z[i] )
278	2 277	syl	|- ( ph -> ( * ` A ) e. Z[i] )
279		gzmulcl	|- ( ( ( * ` A ) e. Z[i] /\ ( ( A - C ) / M ) e. Z[i] ) -> ( ( * ` A ) x. ( ( A - C ) / M ) ) e. Z[i] )
280	278 9 279	syl2anc	|- ( ph -> ( ( * ` A ) x. ( ( A - C ) / M ) ) e. Z[i] )
281		gzcjcl	|- ( ( ( B - D ) / M ) e. Z[i] -> ( * ` ( ( B - D ) / M ) ) e. Z[i] )
282	10 281	syl	|- ( ph -> ( * ` ( ( B - D ) / M ) ) e. Z[i] )
283		gzmulcl	|- ( ( B e. Z[i] /\ ( * ` ( ( B - D ) / M ) ) e. Z[i] ) -> ( B x. ( * ` ( ( B - D ) / M ) ) ) e. Z[i] )
284	3 282 283	syl2anc	|- ( ph -> ( B x. ( * ` ( ( B - D ) / M ) ) ) e. Z[i] )
285		gzaddcl	|- ( ( ( ( * ` A ) x. ( ( A - C ) / M ) ) e. Z[i] /\ ( B x. ( * ` ( ( B - D ) / M ) ) ) e. Z[i] ) -> ( ( ( * ` A ) x. ( ( A - C ) / M ) ) + ( B x. ( * ` ( ( B - D ) / M ) ) ) ) e. Z[i] )
286	280 284 285	syl2anc	|- ( ph -> ( ( ( * ` A ) x. ( ( A - C ) / M ) ) + ( B x. ( * ` ( ( B - D ) / M ) ) ) ) e. Z[i] )
287		gzsubcl	|- ( ( ( X / M ) e. Z[i] /\ ( ( ( * ` A ) x. ( ( A - C ) / M ) ) + ( B x. ( * ` ( ( B - D ) / M ) ) ) ) e. Z[i] ) -> ( ( X / M ) - ( ( ( * ` A ) x. ( ( A - C ) / M ) ) + ( B x. ( * ` ( ( B - D ) / M ) ) ) ) ) e. Z[i] )
288	276 286 287	syl2anc	|- ( ph -> ( ( X / M ) - ( ( ( * ` A ) x. ( ( A - C ) / M ) ) + ( B x. ( * ` ( ( B - D ) / M ) ) ) ) ) e. Z[i] )
289	273 288	eqeltrd	|- ( ph -> ( ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) / M ) e. Z[i] )
290	254	cjcld	|- ( ph -> ( * ` ( A - C ) ) e. CC )
291	22 290	mulcld	|- ( ph -> ( B x. ( * ` ( A - C ) ) ) e. CC )
292	31 256	mulcld	|- ( ph -> ( ( * ` A ) x. ( B - D ) ) e. CC )
293	291 292 195 196	divsubdird	|- ( ph -> ( ( ( B x. ( * ` ( A - C ) ) ) - ( ( * ` A ) x. ( B - D ) ) ) / M ) = ( ( ( B x. ( * ` ( A - C ) ) ) / M ) - ( ( ( * ` A ) x. ( B - D ) ) / M ) ) )
294		cjsub	|- ( ( A e. CC /\ C e. CC ) -> ( * ` ( A - C ) ) = ( ( * ` A ) - ( * ` C ) ) )
295	13 15 294	syl2anc	|- ( ph -> ( * ` ( A - C ) ) = ( ( * ` A ) - ( * ` C ) ) )
296	295	oveq2d	|- ( ph -> ( B x. ( * ` ( A - C ) ) ) = ( B x. ( ( * ` A ) - ( * ` C ) ) ) )
297	22 31 36	subdid	|- ( ph -> ( B x. ( ( * ` A ) - ( * ` C ) ) ) = ( ( B x. ( * ` A ) ) - ( B x. ( * ` C ) ) ) )
298	296 297	eqtrd	|- ( ph -> ( B x. ( * ` ( A - C ) ) ) = ( ( B x. ( * ` A ) ) - ( B x. ( * ` C ) ) ) )
299	31 22 24	subdid	|- ( ph -> ( ( * ` A ) x. ( B - D ) ) = ( ( ( * ` A ) x. B ) - ( ( * ` A ) x. D ) ) )
300	31 22	mulcomd	|- ( ph -> ( ( * ` A ) x. B ) = ( B x. ( * ` A ) ) )
301	300	oveq1d	|- ( ph -> ( ( ( * ` A ) x. B ) - ( ( * ` A ) x. D ) ) = ( ( B x. ( * ` A ) ) - ( ( * ` A ) x. D ) ) )
302	299 301	eqtrd	|- ( ph -> ( ( * ` A ) x. ( B - D ) ) = ( ( B x. ( * ` A ) ) - ( ( * ` A ) x. D ) ) )
303	298 302	oveq12d	|- ( ph -> ( ( B x. ( * ` ( A - C ) ) ) - ( ( * ` A ) x. ( B - D ) ) ) = ( ( ( B x. ( * ` A ) ) - ( B x. ( * ` C ) ) ) - ( ( B x. ( * ` A ) ) - ( ( * ` A ) x. D ) ) ) )
304	22 31	mulcld	|- ( ph -> ( B x. ( * ` A ) ) e. CC )
305	304 37 105	nnncan1d	|- ( ph -> ( ( ( B x. ( * ` A ) ) - ( B x. ( * ` C ) ) ) - ( ( B x. ( * ` A ) ) - ( ( * ` A ) x. D ) ) ) = ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) )
306	303 305	eqtrd	|- ( ph -> ( ( B x. ( * ` ( A - C ) ) ) - ( ( * ` A ) x. ( B - D ) ) ) = ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) )
307	306	oveq1d	|- ( ph -> ( ( ( B x. ( * ` ( A - C ) ) ) - ( ( * ` A ) x. ( B - D ) ) ) / M ) = ( ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) / M ) )
308	293 307	eqtr3d	|- ( ph -> ( ( ( B x. ( * ` ( A - C ) ) ) / M ) - ( ( ( * ` A ) x. ( B - D ) ) / M ) ) = ( ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) / M ) )
309	22 290 195 196	divassd	|- ( ph -> ( ( B x. ( * ` ( A - C ) ) ) / M ) = ( B x. ( ( * ` ( A - C ) ) / M ) ) )
310	254 195 196	cjdivd	|- ( ph -> ( * ` ( ( A - C ) / M ) ) = ( ( * ` ( A - C ) ) / ( * ` M ) ) )
311	265	oveq2d	|- ( ph -> ( ( * ` ( A - C ) ) / ( * ` M ) ) = ( ( * ` ( A - C ) ) / M ) )
312	310 311	eqtrd	|- ( ph -> ( * ` ( ( A - C ) / M ) ) = ( ( * ` ( A - C ) ) / M ) )
313	312	oveq2d	|- ( ph -> ( B x. ( * ` ( ( A - C ) / M ) ) ) = ( B x. ( ( * ` ( A - C ) ) / M ) ) )
314	309 313	eqtr4d	|- ( ph -> ( ( B x. ( * ` ( A - C ) ) ) / M ) = ( B x. ( * ` ( ( A - C ) / M ) ) ) )
315	31 256 195 196	divassd	|- ( ph -> ( ( ( * ` A ) x. ( B - D ) ) / M ) = ( ( * ` A ) x. ( ( B - D ) / M ) ) )
316	314 315	oveq12d	|- ( ph -> ( ( ( B x. ( * ` ( A - C ) ) ) / M ) - ( ( ( * ` A ) x. ( B - D ) ) / M ) ) = ( ( B x. ( * ` ( ( A - C ) / M ) ) ) - ( ( * ` A ) x. ( ( B - D ) / M ) ) ) )
317	308 316	eqtr3d	|- ( ph -> ( ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) / M ) = ( ( B x. ( * ` ( ( A - C ) / M ) ) ) - ( ( * ` A ) x. ( ( B - D ) / M ) ) ) )
318		gzcjcl	|- ( ( ( A - C ) / M ) e. Z[i] -> ( * ` ( ( A - C ) / M ) ) e. Z[i] )
319	9 318	syl	|- ( ph -> ( * ` ( ( A - C ) / M ) ) e. Z[i] )
320		gzmulcl	|- ( ( B e. Z[i] /\ ( * ` ( ( A - C ) / M ) ) e. Z[i] ) -> ( B x. ( * ` ( ( A - C ) / M ) ) ) e. Z[i] )
321	3 319 320	syl2anc	|- ( ph -> ( B x. ( * ` ( ( A - C ) / M ) ) ) e. Z[i] )
322		gzmulcl	|- ( ( ( * ` A ) e. Z[i] /\ ( ( B - D ) / M ) e. Z[i] ) -> ( ( * ` A ) x. ( ( B - D ) / M ) ) e. Z[i] )
323	278 10 322	syl2anc	|- ( ph -> ( ( * ` A ) x. ( ( B - D ) / M ) ) e. Z[i] )
324		gzsubcl	|- ( ( ( B x. ( * ` ( ( A - C ) / M ) ) ) e. Z[i] /\ ( ( * ` A ) x. ( ( B - D ) / M ) ) e. Z[i] ) -> ( ( B x. ( * ` ( ( A - C ) / M ) ) ) - ( ( * ` A ) x. ( ( B - D ) / M ) ) ) e. Z[i] )
325	321 323 324	syl2anc	|- ( ph -> ( ( B x. ( * ` ( ( A - C ) / M ) ) ) - ( ( * ` A ) x. ( ( B - D ) / M ) ) ) e. Z[i] )
326	317 325	eqeltrd	|- ( ph -> ( ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) / M ) e. Z[i] )
327	1	4sqlem4a	|- ( ( ( ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) / M ) e. Z[i] /\ ( ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) / M ) e. Z[i] ) -> ( ( ( abs ` ( ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) / M ) ) ^ 2 ) + ( ( abs ` ( ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) / M ) ) ^ 2 ) ) e. S )
328	289 326 327	syl2anc	|- ( ph -> ( ( ( abs ` ( ( ( ( * ` A ) x. C ) + ( B x. ( * ` D ) ) ) / M ) ) ^ 2 ) + ( ( abs ` ( ( ( ( * ` A ) x. D ) - ( B x. ( * ` C ) ) ) / M ) ) ^ 2 ) ) e. S )
329	236 328	eqeltrrd	|- ( ph -> ( ( X / M ) x. ( Y / M ) ) e. S )