| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elin 3967 | . . . 4
⊢ (𝑧 ∈ (( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) ↔ (𝑧 ∈ ( 0 𝑆𝑅) ∧ 𝑧 ∈ (𝑋𝐿𝑌))) | 
| 2 |  | itsclinecirc0b.i | . . . . 5
⊢ 𝐼 = {1, 2} | 
| 3 |  | itsclinecirc0b.e | . . . . 5
⊢ 𝐸 = (ℝ^‘𝐼) | 
| 4 |  | itsclinecirc0b.p | . . . . 5
⊢ 𝑃 = (ℝ ↑m
𝐼) | 
| 5 |  | itsclinecirc0b.s | . . . . 5
⊢ 𝑆 = (Sphere‘𝐸) | 
| 6 |  | itsclinecirc0b.0 | . . . . 5
⊢  0 = (𝐼 × {0}) | 
| 7 |  | itsclinecirc0b.q | . . . . 5
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) | 
| 8 |  | itsclinecirc0b.d | . . . . 5
⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) | 
| 9 |  | itsclinecirc0b.l | . . . . 5
⊢ 𝐿 = (LineM‘𝐸) | 
| 10 |  | itsclinecirc0b.a | . . . . 5
⊢ 𝐴 = ((𝑋‘2) − (𝑌‘2)) | 
| 11 |  | itsclinecirc0b.b | . . . . 5
⊢ 𝐵 = ((𝑌‘1) − (𝑋‘1)) | 
| 12 |  | itsclinecirc0b.c | . . . . 5
⊢ 𝐶 = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) | 
| 13 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 | itsclinecirc0b 48695 | . . . 4
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → ((𝑧 ∈ ( 0 𝑆𝑅) ∧ 𝑧 ∈ (𝑋𝐿𝑌)) ↔ (𝑧 ∈ 𝑃 ∧ (((𝑧‘1) = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑧‘2) = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ ((𝑧‘1) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑧‘2) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))))) | 
| 14 | 1, 13 | bitrid 283 | . . 3
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (𝑧 ∈ (( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) ↔ (𝑧 ∈ 𝑃 ∧ (((𝑧‘1) = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑧‘2) = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ ((𝑧‘1) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑧‘2) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))))) | 
| 15 | 2, 4 | rrx2pyel 48633 | . . . . . . . . . . 11
⊢ (𝑋 ∈ 𝑃 → (𝑋‘2) ∈ ℝ) | 
| 16 | 15 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (𝑋‘2) ∈ ℝ) | 
| 17 | 2, 4 | rrx2pyel 48633 | . . . . . . . . . . 11
⊢ (𝑌 ∈ 𝑃 → (𝑌‘2) ∈ ℝ) | 
| 18 | 17 | adantl 481 | . . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (𝑌‘2) ∈ ℝ) | 
| 19 | 16, 18 | resubcld 11691 | . . . . . . . . 9
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → ((𝑋‘2) − (𝑌‘2)) ∈ ℝ) | 
| 20 | 10, 19 | eqeltrid 2845 | . . . . . . . 8
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → 𝐴 ∈ ℝ) | 
| 21 | 20 | 3adant3 1133 | . . . . . . 7
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → 𝐴 ∈ ℝ) | 
| 22 | 21 | adantr 480 | . . . . . 6
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → 𝐴 ∈
ℝ) | 
| 23 | 2, 4 | rrx2pxel 48632 | . . . . . . . . . . 11
⊢ (𝑌 ∈ 𝑃 → (𝑌‘1) ∈ ℝ) | 
| 24 | 23 | adantl 481 | . . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (𝑌‘1) ∈ ℝ) | 
| 25 | 2, 4 | rrx2pxel 48632 | . . . . . . . . . . 11
⊢ (𝑋 ∈ 𝑃 → (𝑋‘1) ∈ ℝ) | 
| 26 | 25 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (𝑋‘1) ∈ ℝ) | 
| 27 | 24, 26 | resubcld 11691 | . . . . . . . . 9
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → ((𝑌‘1) − (𝑋‘1)) ∈ ℝ) | 
| 28 | 11, 27 | eqeltrid 2845 | . . . . . . . 8
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → 𝐵 ∈ ℝ) | 
| 29 | 28 | 3adant3 1133 | . . . . . . 7
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → 𝐵 ∈ ℝ) | 
| 30 | 29 | adantr 480 | . . . . . 6
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → 𝐵 ∈
ℝ) | 
| 31 | 16, 24 | remulcld 11291 | . . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → ((𝑋‘2) · (𝑌‘1)) ∈ ℝ) | 
| 32 | 26, 18 | remulcld 11291 | . . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → ((𝑋‘1) · (𝑌‘2)) ∈ ℝ) | 
| 33 | 31, 32 | resubcld 11691 | . . . . . . . . 9
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) ∈ ℝ) | 
| 34 | 12, 33 | eqeltrid 2845 | . . . . . . . 8
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → 𝐶 ∈ ℝ) | 
| 35 | 34 | 3adant3 1133 | . . . . . . 7
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → 𝐶 ∈ ℝ) | 
| 36 | 35 | adantr 480 | . . . . . 6
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → 𝐶 ∈
ℝ) | 
| 37 | 22, 30, 36 | 3jca 1129 | . . . . 5
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈
ℝ)) | 
| 38 | 21, 29, 35 | 3jca 1129 | . . . . . . 7
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) | 
| 39 |  | rpre 13043 | . . . . . . . 8
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
ℝ) | 
| 40 | 39 | adantr 480 | . . . . . . 7
⊢ ((𝑅 ∈ ℝ+
∧ 0 ≤ 𝐷) →
𝑅 ∈
ℝ) | 
| 41 | 7, 8 | itsclc0lem3 48679 | . . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ) → 𝐷 ∈
ℝ) | 
| 42 | 38, 40, 41 | syl2an 596 | . . . . . 6
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → 𝐷 ∈
ℝ) | 
| 43 |  | simprr 773 | . . . . . 6
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → 0 ≤ 𝐷) | 
| 44 | 42, 43 | jca 511 | . . . . 5
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (𝐷 ∈ ℝ ∧ 0 ≤
𝐷)) | 
| 45 | 20, 28 | jca 511 | . . . . . . . . 9
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) | 
| 46 | 7 | resum2sqcl 48627 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑄 ∈
ℝ) | 
| 47 | 45, 46 | syl 17 | . . . . . . . 8
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → 𝑄 ∈ ℝ) | 
| 48 | 47 | 3adant3 1133 | . . . . . . 7
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → 𝑄 ∈ ℝ) | 
| 49 | 2, 4, 11, 10 | rrx2pnedifcoorneorr 48638 | . . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝐵 ≠ 0 ∨ 𝐴 ≠ 0)) | 
| 50 | 49 | orcomd 872 | . . . . . . . . 9
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)) | 
| 51 | 7 | resum2sqorgt0 48630 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)) → 0 < 𝑄) | 
| 52 | 21, 29, 50, 51 | syl3anc 1373 | . . . . . . . 8
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → 0 < 𝑄) | 
| 53 | 52 | gt0ne0d 11827 | . . . . . . 7
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → 𝑄 ≠ 0) | 
| 54 | 48, 53 | jca 511 | . . . . . 6
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝑄 ∈ ℝ ∧ 𝑄 ≠ 0)) | 
| 55 | 54 | adantr 480 | . . . . 5
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (𝑄 ∈ ℝ ∧ 𝑄 ≠ 0)) | 
| 56 |  | itsclc0lem1 48677 | . . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐷 ∈ ℝ ∧ 0 ≤
𝐷) ∧ (𝑄 ∈ ℝ ∧ 𝑄 ≠ 0)) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ) | 
| 57 | 37, 44, 55, 56 | syl3anc 1373 | . . . 4
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ) | 
| 58 | 30, 22, 36 | 3jca 1129 | . . . . 5
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐶 ∈
ℝ)) | 
| 59 | 48 | adantr 480 | . . . . . 6
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → 𝑄 ∈
ℝ) | 
| 60 | 53 | adantr 480 | . . . . . 6
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → 𝑄 ≠ 0) | 
| 61 | 59, 60 | jca 511 | . . . . 5
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (𝑄 ∈ ℝ ∧ 𝑄 ≠ 0)) | 
| 62 |  | itsclc0lem2 48678 | . . . . 5
⊢ (((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐷 ∈ ℝ ∧ 0 ≤
𝐷) ∧ (𝑄 ∈ ℝ ∧ 𝑄 ≠ 0)) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ) | 
| 63 | 58, 44, 61, 62 | syl3anc 1373 | . . . 4
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ) | 
| 64 |  | itsclc0lem2 48678 | . . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐷 ∈ ℝ ∧ 0 ≤
𝐷) ∧ (𝑄 ∈ ℝ ∧ 𝑄 ≠ 0)) → (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ) | 
| 65 | 37, 44, 61, 64 | syl3anc 1373 | . . . 4
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ) | 
| 66 |  | itsclc0lem1 48677 | . . . . 5
⊢ (((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐷 ∈ ℝ ∧ 0 ≤
𝐷) ∧ (𝑄 ∈ ℝ ∧ 𝑄 ≠ 0)) → (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ) | 
| 67 | 58, 44, 61, 66 | syl3anc 1373 | . . . 4
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ) | 
| 68 | 2, 4 | prelrrx2b 48635 | . . . 4
⊢
((((((𝐴 ·
𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ ∧ (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ) ∧ ((((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∈ ℝ ∧ (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄) ∈ ℝ)) → ((𝑧 ∈ 𝑃 ∧ (((𝑧‘1) = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑧‘2) = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ ((𝑧‘1) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑧‘2) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))) ↔ 𝑧 ∈ {{〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉}, {〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉}})) | 
| 69 | 57, 63, 65, 67, 68 | syl22anc 839 | . . 3
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → ((𝑧 ∈ 𝑃 ∧ (((𝑧‘1) = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑧‘2) = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ ((𝑧‘1) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑧‘2) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))) ↔ 𝑧 ∈ {{〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉}, {〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉}})) | 
| 70 | 14, 69 | bitrd 279 | . 2
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (𝑧 ∈ (( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) ↔ 𝑧 ∈ {{〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉}, {〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉}})) | 
| 71 | 70 | eqrdv 2735 | 1
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (( 0 𝑆𝑅) ∩ (𝑋𝐿𝑌)) = {{〈1, (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)〉}, {〈1, (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄)〉, 〈2, (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)〉}}) |