Metamath Proof Explorer

Theorem addsdilem4

Description: Lemma for addsdi . Show one of the equalities involved in the final expression. (Contributed by Scott Fenton, 9-Mar-2025)

Ref Expression
Hypotheses addsdilem4.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
addsdilem4.2 ⊢ ( 𝜑 → 𝐵 ∈ No )
addsdilem4.3 ⊢ ( 𝜑 → 𝐶 ∈ No )
addsdilem4.4 ⊢ ( 𝜑 → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ( 𝑥𝑂 ·s ( 𝐵 +s 𝐶 ) ) = ( ( 𝑥𝑂 ·s 𝐵 ) +s ( 𝑥𝑂 ·s 𝐶 ) ) )
addsdilem4.5 ⊢ ( 𝜑 → ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝐶 ) ∪ ( R ‘ 𝐶 ) ) ( 𝐴 ·s ( 𝐵 +s 𝑧𝑂 ) ) = ( ( 𝐴 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧𝑂 ) ) )
addsdilem4.6 ⊢ ( 𝜑 → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝐶 ) ∪ ( R ‘ 𝐶 ) ) ( 𝑥𝑂 ·s ( 𝐵 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝐵 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) )
addsdilem4.7 ⊢ ( 𝜓 → 𝑋 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
addsdilem4.8 ⊢ ( 𝜓 → 𝑍 ∈ ( ( L ‘ 𝐶 ) ∪ ( R ‘ 𝐶 ) ) )
Assertion addsdilem4 ( ( 𝜑 ∧ 𝜓 ) → ( ( ( 𝑋 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑍 ) ) ) -s ( 𝑋 ·s ( 𝐵 +s 𝑍 ) ) ) = ( ( 𝐴 ·s 𝐵 ) +s ( ( ( 𝑋 ·s 𝐶 ) +s ( 𝐴 ·s 𝑍 ) ) -s ( 𝑋 ·s 𝑍 ) ) ) )

Proof

Step Hyp Ref Expression
1 addsdilem4.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
2 addsdilem4.2 ⊢ ( 𝜑 → 𝐵 ∈ No )
3 addsdilem4.3 ⊢ ( 𝜑 → 𝐶 ∈ No )
4 addsdilem4.4 ⊢ ( 𝜑 → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ( 𝑥𝑂 ·s ( 𝐵 +s 𝐶 ) ) = ( ( 𝑥𝑂 ·s 𝐵 ) +s ( 𝑥𝑂 ·s 𝐶 ) ) )
5 addsdilem4.5 ⊢ ( 𝜑 → ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝐶 ) ∪ ( R ‘ 𝐶 ) ) ( 𝐴 ·s ( 𝐵 +s 𝑧𝑂 ) ) = ( ( 𝐴 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧𝑂 ) ) )
6 addsdilem4.6 ⊢ ( 𝜑 → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝐶 ) ∪ ( R ‘ 𝐶 ) ) ( 𝑥𝑂 ·s ( 𝐵 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝐵 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) )
7 addsdilem4.7 ⊢ ( 𝜓 → 𝑋 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
8 addsdilem4.8 ⊢ ( 𝜓 → 𝑍 ∈ ( ( L ‘ 𝐶 ) ∪ ( R ‘ 𝐶 ) ) )
9 oveq1 ⊢ ( 𝑥𝑂 = 𝑋 → ( 𝑥𝑂 ·s ( 𝐵 +s 𝐶 ) ) = ( 𝑋 ·s ( 𝐵 +s 𝐶 ) ) )
10 oveq1 ⊢ ( 𝑥𝑂 = 𝑋 → ( 𝑥𝑂 ·s 𝐵 ) = ( 𝑋 ·s 𝐵 ) )
11 oveq1 ⊢ ( 𝑥𝑂 = 𝑋 → ( 𝑥𝑂 ·s 𝐶 ) = ( 𝑋 ·s 𝐶 ) )
12 10 11 oveq12d ⊢ ( 𝑥𝑂 = 𝑋 → ( ( 𝑥𝑂 ·s 𝐵 ) +s ( 𝑥𝑂 ·s 𝐶 ) ) = ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) )
13 9 12 eqeq12d ⊢ ( 𝑥𝑂 = 𝑋 → ( ( 𝑥𝑂 ·s ( 𝐵 +s 𝐶 ) ) = ( ( 𝑥𝑂 ·s 𝐵 ) +s ( 𝑥𝑂 ·s 𝐶 ) ) ↔ ( 𝑋 ·s ( 𝐵 +s 𝐶 ) ) = ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) ) )
14 4 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ( 𝑥𝑂 ·s ( 𝐵 +s 𝐶 ) ) = ( ( 𝑥𝑂 ·s 𝐵 ) +s ( 𝑥𝑂 ·s 𝐶 ) ) )
15 7 adantl ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑋 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
16 13 14 15 rspcdva ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑋 ·s ( 𝐵 +s 𝐶 ) ) = ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) )
17 oveq2 ⊢ ( 𝑧𝑂 = 𝑍 → ( 𝐵 +s 𝑧𝑂 ) = ( 𝐵 +s 𝑍 ) )
18 17 oveq2d ⊢ ( 𝑧𝑂 = 𝑍 → ( 𝐴 ·s ( 𝐵 +s 𝑧𝑂 ) ) = ( 𝐴 ·s ( 𝐵 +s 𝑍 ) ) )
19 oveq2 ⊢ ( 𝑧𝑂 = 𝑍 → ( 𝐴 ·s 𝑧𝑂 ) = ( 𝐴 ·s 𝑍 ) )
20 19 oveq2d ⊢ ( 𝑧𝑂 = 𝑍 → ( ( 𝐴 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧𝑂 ) ) = ( ( 𝐴 ·s 𝐵 ) +s ( 𝐴 ·s 𝑍 ) ) )
21 18 20 eqeq12d ⊢ ( 𝑧𝑂 = 𝑍 → ( ( 𝐴 ·s ( 𝐵 +s 𝑧𝑂 ) ) = ( ( 𝐴 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧𝑂 ) ) ↔ ( 𝐴 ·s ( 𝐵 +s 𝑍 ) ) = ( ( 𝐴 ·s 𝐵 ) +s ( 𝐴 ·s 𝑍 ) ) ) )
22 5 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝐶 ) ∪ ( R ‘ 𝐶 ) ) ( 𝐴 ·s ( 𝐵 +s 𝑧𝑂 ) ) = ( ( 𝐴 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧𝑂 ) ) )
23 8 adantl ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑍 ∈ ( ( L ‘ 𝐶 ) ∪ ( R ‘ 𝐶 ) ) )
24 21 22 23 rspcdva ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐴 ·s ( 𝐵 +s 𝑍 ) ) = ( ( 𝐴 ·s 𝐵 ) +s ( 𝐴 ·s 𝑍 ) ) )
25 16 24 oveq12d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑋 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑍 ) ) ) = ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) +s ( ( 𝐴 ·s 𝐵 ) +s ( 𝐴 ·s 𝑍 ) ) ) )
26 oveq1 ⊢ ( 𝑥𝑂 = 𝑋 → ( 𝑥𝑂 ·s ( 𝐵 +s 𝑧𝑂 ) ) = ( 𝑋 ·s ( 𝐵 +s 𝑧𝑂 ) ) )
27 oveq1 ⊢ ( 𝑥𝑂 = 𝑋 → ( 𝑥𝑂 ·s 𝑧𝑂 ) = ( 𝑋 ·s 𝑧𝑂 ) )
28 10 27 oveq12d ⊢ ( 𝑥𝑂 = 𝑋 → ( ( 𝑥𝑂 ·s 𝐵 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) = ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝑧𝑂 ) ) )
29 26 28 eqeq12d ⊢ ( 𝑥𝑂 = 𝑋 → ( ( 𝑥𝑂 ·s ( 𝐵 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝐵 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) ↔ ( 𝑋 ·s ( 𝐵 +s 𝑧𝑂 ) ) = ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝑧𝑂 ) ) ) )
30 17 oveq2d ⊢ ( 𝑧𝑂 = 𝑍 → ( 𝑋 ·s ( 𝐵 +s 𝑧𝑂 ) ) = ( 𝑋 ·s ( 𝐵 +s 𝑍 ) ) )
31 oveq2 ⊢ ( 𝑧𝑂 = 𝑍 → ( 𝑋 ·s 𝑧𝑂 ) = ( 𝑋 ·s 𝑍 ) )
32 31 oveq2d ⊢ ( 𝑧𝑂 = 𝑍 → ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝑧𝑂 ) ) = ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝑍 ) ) )
33 30 32 eqeq12d ⊢ ( 𝑧𝑂 = 𝑍 → ( ( 𝑋 ·s ( 𝐵 +s 𝑧𝑂 ) ) = ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝑧𝑂 ) ) ↔ ( 𝑋 ·s ( 𝐵 +s 𝑍 ) ) = ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝑍 ) ) ) )
34 6 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∀ 𝑧𝑂 ∈ ( ( L ‘ 𝐶 ) ∪ ( R ‘ 𝐶 ) ) ( 𝑥𝑂 ·s ( 𝐵 +s 𝑧𝑂 ) ) = ( ( 𝑥𝑂 ·s 𝐵 ) +s ( 𝑥𝑂 ·s 𝑧𝑂 ) ) )
35 29 33 34 15 23 rspc2dv ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑋 ·s ( 𝐵 +s 𝑍 ) ) = ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝑍 ) ) )
36 25 35 oveq12d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( 𝑋 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑍 ) ) ) -s ( 𝑋 ·s ( 𝐵 +s 𝑍 ) ) ) = ( ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) +s ( ( 𝐴 ·s 𝐵 ) +s ( 𝐴 ·s 𝑍 ) ) ) -s ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝑍 ) ) ) )
37 leftssno ⊢ ( L ‘ 𝐴 ) ⊆ No
38 rightssno ⊢ ( R ‘ 𝐴 ) ⊆ No
39 37 38 unssi ⊢ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ⊆ No
40 39 7 sselid ⊢ ( 𝜓 → 𝑋 ∈ No )
41 40 adantl ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑋 ∈ No )
42 2 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐵 ∈ No )
43 41 42 mulscld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑋 ·s 𝐵 ) ∈ No )
44 3 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐶 ∈ No )
45 41 44 mulscld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑋 ·s 𝐶 ) ∈ No )
46 43 45 addscld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) ∈ No )
47 1 2 mulscld ⊢ ( 𝜑 → ( 𝐴 ·s 𝐵 ) ∈ No )
48 47 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐴 ·s 𝐵 ) ∈ No )
49 1 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐴 ∈ No )
50 leftssno ⊢ ( L ‘ 𝐶 ) ⊆ No
51 rightssno ⊢ ( R ‘ 𝐶 ) ⊆ No
52 50 51 unssi ⊢ ( ( L ‘ 𝐶 ) ∪ ( R ‘ 𝐶 ) ) ⊆ No
53 52 8 sselid ⊢ ( 𝜓 → 𝑍 ∈ No )
54 53 adantl ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑍 ∈ No )
55 49 54 mulscld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐴 ·s 𝑍 ) ∈ No )
56 48 55 addscld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝐴 ·s 𝐵 ) +s ( 𝐴 ·s 𝑍 ) ) ∈ No )
57 46 56 addscld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) +s ( ( 𝐴 ·s 𝐵 ) +s ( 𝐴 ·s 𝑍 ) ) ) ∈ No )
58 41 54 mulscld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑋 ·s 𝑍 ) ∈ No )
59 57 43 58 subsubs4d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) +s ( ( 𝐴 ·s 𝐵 ) +s ( 𝐴 ·s 𝑍 ) ) ) -s ( 𝑋 ·s 𝐵 ) ) -s ( 𝑋 ·s 𝑍 ) ) = ( ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) +s ( ( 𝐴 ·s 𝐵 ) +s ( 𝐴 ·s 𝑍 ) ) ) -s ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝑍 ) ) ) )
60 46 56 43 addsubsd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) +s ( ( 𝐴 ·s 𝐵 ) +s ( 𝐴 ·s 𝑍 ) ) ) -s ( 𝑋 ·s 𝐵 ) ) = ( ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) -s ( 𝑋 ·s 𝐵 ) ) +s ( ( 𝐴 ·s 𝐵 ) +s ( 𝐴 ·s 𝑍 ) ) ) )
61 43 45 addscomd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) = ( ( 𝑋 ·s 𝐶 ) +s ( 𝑋 ·s 𝐵 ) ) )
62 61 oveq1d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) -s ( 𝑋 ·s 𝐵 ) ) = ( ( ( 𝑋 ·s 𝐶 ) +s ( 𝑋 ·s 𝐵 ) ) -s ( 𝑋 ·s 𝐵 ) ) )
63 pncans ⊢ ( ( ( 𝑋 ·s 𝐶 ) ∈ No ∧ ( 𝑋 ·s 𝐵 ) ∈ No ) → ( ( ( 𝑋 ·s 𝐶 ) +s ( 𝑋 ·s 𝐵 ) ) -s ( 𝑋 ·s 𝐵 ) ) = ( 𝑋 ·s 𝐶 ) )
64 45 43 63 syl2anc ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( 𝑋 ·s 𝐶 ) +s ( 𝑋 ·s 𝐵 ) ) -s ( 𝑋 ·s 𝐵 ) ) = ( 𝑋 ·s 𝐶 ) )
65 62 64 eqtrd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) -s ( 𝑋 ·s 𝐵 ) ) = ( 𝑋 ·s 𝐶 ) )
66 65 oveq1d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) -s ( 𝑋 ·s 𝐵 ) ) +s ( ( 𝐴 ·s 𝐵 ) +s ( 𝐴 ·s 𝑍 ) ) ) = ( ( 𝑋 ·s 𝐶 ) +s ( ( 𝐴 ·s 𝐵 ) +s ( 𝐴 ·s 𝑍 ) ) ) )
67 45 48 55 adds12d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑋 ·s 𝐶 ) +s ( ( 𝐴 ·s 𝐵 ) +s ( 𝐴 ·s 𝑍 ) ) ) = ( ( 𝐴 ·s 𝐵 ) +s ( ( 𝑋 ·s 𝐶 ) +s ( 𝐴 ·s 𝑍 ) ) ) )
68 60 66 67 3eqtrd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) +s ( ( 𝐴 ·s 𝐵 ) +s ( 𝐴 ·s 𝑍 ) ) ) -s ( 𝑋 ·s 𝐵 ) ) = ( ( 𝐴 ·s 𝐵 ) +s ( ( 𝑋 ·s 𝐶 ) +s ( 𝐴 ·s 𝑍 ) ) ) )
69 68 oveq1d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) +s ( ( 𝐴 ·s 𝐵 ) +s ( 𝐴 ·s 𝑍 ) ) ) -s ( 𝑋 ·s 𝐵 ) ) -s ( 𝑋 ·s 𝑍 ) ) = ( ( ( 𝐴 ·s 𝐵 ) +s ( ( 𝑋 ·s 𝐶 ) +s ( 𝐴 ·s 𝑍 ) ) ) -s ( 𝑋 ·s 𝑍 ) ) )
70 45 55 addscld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑋 ·s 𝐶 ) +s ( 𝐴 ·s 𝑍 ) ) ∈ No )
71 48 70 58 addsubsassd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( 𝐴 ·s 𝐵 ) +s ( ( 𝑋 ·s 𝐶 ) +s ( 𝐴 ·s 𝑍 ) ) ) -s ( 𝑋 ·s 𝑍 ) ) = ( ( 𝐴 ·s 𝐵 ) +s ( ( ( 𝑋 ·s 𝐶 ) +s ( 𝐴 ·s 𝑍 ) ) -s ( 𝑋 ·s 𝑍 ) ) ) )
72 69 71 eqtrd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( ( ( 𝑋 ·s 𝐵 ) +s ( 𝑋 ·s 𝐶 ) ) +s ( ( 𝐴 ·s 𝐵 ) +s ( 𝐴 ·s 𝑍 ) ) ) -s ( 𝑋 ·s 𝐵 ) ) -s ( 𝑋 ·s 𝑍 ) ) = ( ( 𝐴 ·s 𝐵 ) +s ( ( ( 𝑋 ·s 𝐶 ) +s ( 𝐴 ·s 𝑍 ) ) -s ( 𝑋 ·s 𝑍 ) ) ) )
73 36 59 72 3eqtr2d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( 𝑋 ·s ( 𝐵 +s 𝐶 ) ) +s ( 𝐴 ·s ( 𝐵 +s 𝑍 ) ) ) -s ( 𝑋 ·s ( 𝐵 +s 𝑍 ) ) ) = ( ( 𝐴 ·s 𝐵 ) +s ( ( ( 𝑋 ·s 𝐶 ) +s ( 𝐴 ·s 𝑍 ) ) -s ( 𝑋 ·s 𝑍 ) ) ) )