Metamath Proof Explorer

Theorem xmulass

Description: Associativity of the extended real multiplication operation. Surprisingly, there are no restrictions on the values, unlike xaddass which has to avoid the "undefined" combinations +oo +e -oo and -oo +e +oo . The equivalent "undefined" expression here would be 0 *e +oo , but since this is defined to equal 0 any zeroes in the expression make the whole thing evaluate to zero (on both sides), thus establishing the identity in this case. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xmulass ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→A⋅𝑒B⋅𝑒C=A⋅𝑒B⋅𝑒C

Proof

Step Hyp Ref Expression
1 oveq1 ⊢x=A→x⋅𝑒B=A⋅𝑒B
2 1 oveq1d ⊢x=A→x⋅𝑒B⋅𝑒C=A⋅𝑒B⋅𝑒C
3 oveq1 ⊢x=A→x⋅𝑒B⋅𝑒C=A⋅𝑒B⋅𝑒C
4 2 3 eqeq12d ⊢x=A→x⋅𝑒B⋅𝑒C=x⋅𝑒B⋅𝑒C↔A⋅𝑒B⋅𝑒C=A⋅𝑒B⋅𝑒C
5 oveq1 ⊢x=−A→x⋅𝑒B=−A⋅𝑒B
6 5 oveq1d ⊢x=−A→x⋅𝑒B⋅𝑒C=−A⋅𝑒B⋅𝑒C
7 oveq1 ⊢x=−A→x⋅𝑒B⋅𝑒C=−A⋅𝑒B⋅𝑒C
8 6 7 eqeq12d ⊢x=−A→x⋅𝑒B⋅𝑒C=x⋅𝑒B⋅𝑒C↔−A⋅𝑒B⋅𝑒C=−A⋅𝑒B⋅𝑒C
9 xmulcl ⊢A∈ℝ*∧B∈ℝ*→A⋅𝑒B∈ℝ*
10 xmulcl ⊢A⋅𝑒B∈ℝ*∧C∈ℝ*→A⋅𝑒B⋅𝑒C∈ℝ*
11 9 10 stoic3 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→A⋅𝑒B⋅𝑒C∈ℝ*
12 simp1 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→A∈ℝ*
13 xmulcl ⊢B∈ℝ*∧C∈ℝ*→B⋅𝑒C∈ℝ*
14 13 3adant1 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→B⋅𝑒C∈ℝ*
15 xmulcl ⊢A∈ℝ*∧B⋅𝑒C∈ℝ*→A⋅𝑒B⋅𝑒C∈ℝ*
16 12 14 15 syl2anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→A⋅𝑒B⋅𝑒C∈ℝ*
17 oveq2 ⊢y=B→x⋅𝑒y=x⋅𝑒B
18 17 oveq1d ⊢y=B→x⋅𝑒y⋅𝑒C=x⋅𝑒B⋅𝑒C
19 oveq1 ⊢y=B→y⋅𝑒C=B⋅𝑒C
20 19 oveq2d ⊢y=B→x⋅𝑒y⋅𝑒C=x⋅𝑒B⋅𝑒C
21 18 20 eqeq12d ⊢y=B→x⋅𝑒y⋅𝑒C=x⋅𝑒y⋅𝑒C↔x⋅𝑒B⋅𝑒C=x⋅𝑒B⋅𝑒C
22 oveq2 ⊢y=−B→x⋅𝑒y=x⋅𝑒−B
23 22 oveq1d ⊢y=−B→x⋅𝑒y⋅𝑒C=x⋅𝑒−B⋅𝑒C
24 oveq1 ⊢y=−B→y⋅𝑒C=−B⋅𝑒C
25 24 oveq2d ⊢y=−B→x⋅𝑒y⋅𝑒C=x⋅𝑒−B⋅𝑒C
26 23 25 eqeq12d ⊢y=−B→x⋅𝑒y⋅𝑒C=x⋅𝑒y⋅𝑒C↔x⋅𝑒−B⋅𝑒C=x⋅𝑒−B⋅𝑒C
27 simprl ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x→x∈ℝ*
28 simpl2 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x→B∈ℝ*
29 xmulcl ⊢x∈ℝ*∧B∈ℝ*→x⋅𝑒B∈ℝ*
30 27 28 29 syl2anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x→x⋅𝑒B∈ℝ*
31 simpl3 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x→C∈ℝ*
32 xmulcl ⊢x⋅𝑒B∈ℝ*∧C∈ℝ*→x⋅𝑒B⋅𝑒C∈ℝ*
33 30 31 32 syl2anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x→x⋅𝑒B⋅𝑒C∈ℝ*
34 14 adantr ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x→B⋅𝑒C∈ℝ*
35 xmulcl ⊢x∈ℝ*∧B⋅𝑒C∈ℝ*→x⋅𝑒B⋅𝑒C∈ℝ*
36 27 34 35 syl2anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x→x⋅𝑒B⋅𝑒C∈ℝ*
37 oveq2 ⊢z=C→x⋅𝑒y⋅𝑒z=x⋅𝑒y⋅𝑒C
38 oveq2 ⊢z=C→y⋅𝑒z=y⋅𝑒C
39 38 oveq2d ⊢z=C→x⋅𝑒y⋅𝑒z=x⋅𝑒y⋅𝑒C
40 37 39 eqeq12d ⊢z=C→x⋅𝑒y⋅𝑒z=x⋅𝑒y⋅𝑒z↔x⋅𝑒y⋅𝑒C=x⋅𝑒y⋅𝑒C
41 oveq2 ⊢z=−C→x⋅𝑒y⋅𝑒z=x⋅𝑒y⋅𝑒−C
42 oveq2 ⊢z=−C→y⋅𝑒z=y⋅𝑒−C
43 42 oveq2d ⊢z=−C→x⋅𝑒y⋅𝑒z=x⋅𝑒y⋅𝑒−C
44 41 43 eqeq12d ⊢z=−C→x⋅𝑒y⋅𝑒z=x⋅𝑒y⋅𝑒z↔x⋅𝑒y⋅𝑒−C=x⋅𝑒y⋅𝑒−C
45 27 adantr ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x∧y∈ℝ*∧0<y→x∈ℝ*
46 simprl ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x∧y∈ℝ*∧0<y→y∈ℝ*
47 xmulcl ⊢x∈ℝ*∧y∈ℝ*→x⋅𝑒y∈ℝ*
48 45 46 47 syl2anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x∧y∈ℝ*∧0<y→x⋅𝑒y∈ℝ*
49 31 adantr ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x∧y∈ℝ*∧0<y→C∈ℝ*
50 xmulcl ⊢x⋅𝑒y∈ℝ*∧C∈ℝ*→x⋅𝑒y⋅𝑒C∈ℝ*
51 48 49 50 syl2anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x∧y∈ℝ*∧0<y→x⋅𝑒y⋅𝑒C∈ℝ*
52 xmulcl ⊢y∈ℝ*∧C∈ℝ*→y⋅𝑒C∈ℝ*
53 46 49 52 syl2anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x∧y∈ℝ*∧0<y→y⋅𝑒C∈ℝ*
54 xmulcl ⊢x∈ℝ*∧y⋅𝑒C∈ℝ*→x⋅𝑒y⋅𝑒C∈ℝ*
55 45 53 54 syl2anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x∧y∈ℝ*∧0<y→x⋅𝑒y⋅𝑒C∈ℝ*
56 xmulasslem3 ⊢x∈ℝ*∧0<x∧y∈ℝ*∧0<y∧z∈ℝ*∧0<z→x⋅𝑒y⋅𝑒z=x⋅𝑒y⋅𝑒z
57 56 ad4ant234 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x∧y∈ℝ*∧0<y∧z∈ℝ*∧0<z→x⋅𝑒y⋅𝑒z=x⋅𝑒y⋅𝑒z
58 xmul01 ⊢x⋅𝑒y∈ℝ*→x⋅𝑒y⋅𝑒0=0
59 48 58 syl ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x∧y∈ℝ*∧0<y→x⋅𝑒y⋅𝑒0=0
60 xmul01 ⊢x∈ℝ*→x⋅𝑒0=0
61 45 60 syl ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x∧y∈ℝ*∧0<y→x⋅𝑒0=0
62 59 61 eqtr4d ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x∧y∈ℝ*∧0<y→x⋅𝑒y⋅𝑒0=x⋅𝑒0
63 xmul01 ⊢y∈ℝ*→y⋅𝑒0=0
64 63 ad2antrl ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x∧y∈ℝ*∧0<y→y⋅𝑒0=0
65 64 oveq2d ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x∧y∈ℝ*∧0<y→x⋅𝑒y⋅𝑒0=x⋅𝑒0
66 62 65 eqtr4d ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x∧y∈ℝ*∧0<y→x⋅𝑒y⋅𝑒0=x⋅𝑒y⋅𝑒0
67 oveq2 ⊢z=0→x⋅𝑒y⋅𝑒z=x⋅𝑒y⋅𝑒0
68 oveq2 ⊢z=0→y⋅𝑒z=y⋅𝑒0
69 68 oveq2d ⊢z=0→x⋅𝑒y⋅𝑒z=x⋅𝑒y⋅𝑒0
70 67 69 eqeq12d ⊢z=0→x⋅𝑒y⋅𝑒z=x⋅𝑒y⋅𝑒z↔x⋅𝑒y⋅𝑒0=x⋅𝑒y⋅𝑒0
71 66 70 syl5ibrcom ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x∧y∈ℝ*∧0<y→z=0→x⋅𝑒y⋅𝑒z=x⋅𝑒y⋅𝑒z
72 xmulneg2 ⊢x⋅𝑒y∈ℝ*∧C∈ℝ*→x⋅𝑒y⋅𝑒−C=−x⋅𝑒y⋅𝑒C
73 48 49 72 syl2anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x∧y∈ℝ*∧0<y→x⋅𝑒y⋅𝑒−C=−x⋅𝑒y⋅𝑒C
74 xmulneg2 ⊢y∈ℝ*∧C∈ℝ*→y⋅𝑒−C=−y⋅𝑒C
75 46 49 74 syl2anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x∧y∈ℝ*∧0<y→y⋅𝑒−C=−y⋅𝑒C
76 75 oveq2d ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x∧y∈ℝ*∧0<y→x⋅𝑒y⋅𝑒−C=x⋅𝑒−y⋅𝑒C
77 xmulneg2 ⊢x∈ℝ*∧y⋅𝑒C∈ℝ*→x⋅𝑒−y⋅𝑒C=−x⋅𝑒y⋅𝑒C
78 45 53 77 syl2anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x∧y∈ℝ*∧0<y→x⋅𝑒−y⋅𝑒C=−x⋅𝑒y⋅𝑒C
79 76 78 eqtrd ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x∧y∈ℝ*∧0<y→x⋅𝑒y⋅𝑒−C=−x⋅𝑒y⋅𝑒C
80 40 44 51 55 49 57 71 73 79 xmulasslem ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x∧y∈ℝ*∧0<y→x⋅𝑒y⋅𝑒C=x⋅𝑒y⋅𝑒C
81 xmul02 ⊢C∈ℝ*→0⋅𝑒C=0
82 81 3ad2ant3 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→0⋅𝑒C=0
83 82 adantr ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x→0⋅𝑒C=0
84 60 ad2antrl ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x→x⋅𝑒0=0
85 83 84 eqtr4d ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x→0⋅𝑒C=x⋅𝑒0
86 84 oveq1d ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x→x⋅𝑒0⋅𝑒C=0⋅𝑒C
87 83 oveq2d ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x→x⋅𝑒0⋅𝑒C=x⋅𝑒0
88 85 86 87 3eqtr4d ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x→x⋅𝑒0⋅𝑒C=x⋅𝑒0⋅𝑒C
89 oveq2 ⊢y=0→x⋅𝑒y=x⋅𝑒0
90 89 oveq1d ⊢y=0→x⋅𝑒y⋅𝑒C=x⋅𝑒0⋅𝑒C
91 oveq1 ⊢y=0→y⋅𝑒C=0⋅𝑒C
92 91 oveq2d ⊢y=0→x⋅𝑒y⋅𝑒C=x⋅𝑒0⋅𝑒C
93 90 92 eqeq12d ⊢y=0→x⋅𝑒y⋅𝑒C=x⋅𝑒y⋅𝑒C↔x⋅𝑒0⋅𝑒C=x⋅𝑒0⋅𝑒C
94 88 93 syl5ibrcom ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x→y=0→x⋅𝑒y⋅𝑒C=x⋅𝑒y⋅𝑒C
95 xmulneg2 ⊢x∈ℝ*∧B∈ℝ*→x⋅𝑒−B=−x⋅𝑒B
96 27 28 95 syl2anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x→x⋅𝑒−B=−x⋅𝑒B
97 96 oveq1d ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x→x⋅𝑒−B⋅𝑒C=−x⋅𝑒B⋅𝑒C
98 xmulneg1 ⊢x⋅𝑒B∈ℝ*∧C∈ℝ*→−x⋅𝑒B⋅𝑒C=−x⋅𝑒B⋅𝑒C
99 30 31 98 syl2anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x→−x⋅𝑒B⋅𝑒C=−x⋅𝑒B⋅𝑒C
100 97 99 eqtrd ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x→x⋅𝑒−B⋅𝑒C=−x⋅𝑒B⋅𝑒C
101 xmulneg1 ⊢B∈ℝ*∧C∈ℝ*→−B⋅𝑒C=−B⋅𝑒C
102 28 31 101 syl2anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x→−B⋅𝑒C=−B⋅𝑒C
103 102 oveq2d ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x→x⋅𝑒−B⋅𝑒C=x⋅𝑒−B⋅𝑒C
104 xmulneg2 ⊢x∈ℝ*∧B⋅𝑒C∈ℝ*→x⋅𝑒−B⋅𝑒C=−x⋅𝑒B⋅𝑒C
105 27 34 104 syl2anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x→x⋅𝑒−B⋅𝑒C=−x⋅𝑒B⋅𝑒C
106 103 105 eqtrd ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x→x⋅𝑒−B⋅𝑒C=−x⋅𝑒B⋅𝑒C
107 21 26 33 36 28 80 94 100 106 xmulasslem ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧x∈ℝ*∧0<x→x⋅𝑒B⋅𝑒C=x⋅𝑒B⋅𝑒C
108 xmul02 ⊢B∈ℝ*→0⋅𝑒B=0
109 108 3ad2ant2 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→0⋅𝑒B=0
110 109 oveq1d ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→0⋅𝑒B⋅𝑒C=0⋅𝑒C
111 xmul02 ⊢B⋅𝑒C∈ℝ*→0⋅𝑒B⋅𝑒C=0
112 14 111 syl ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→0⋅𝑒B⋅𝑒C=0
113 82 110 112 3eqtr4d ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→0⋅𝑒B⋅𝑒C=0⋅𝑒B⋅𝑒C
114 oveq1 ⊢x=0→x⋅𝑒B=0⋅𝑒B
115 114 oveq1d ⊢x=0→x⋅𝑒B⋅𝑒C=0⋅𝑒B⋅𝑒C
116 oveq1 ⊢x=0→x⋅𝑒B⋅𝑒C=0⋅𝑒B⋅𝑒C
117 115 116 eqeq12d ⊢x=0→x⋅𝑒B⋅𝑒C=x⋅𝑒B⋅𝑒C↔0⋅𝑒B⋅𝑒C=0⋅𝑒B⋅𝑒C
118 113 117 syl5ibrcom ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→x=0→x⋅𝑒B⋅𝑒C=x⋅𝑒B⋅𝑒C
119 xmulneg1 ⊢A∈ℝ*∧B∈ℝ*→−A⋅𝑒B=−A⋅𝑒B
120 119 3adant3 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→−A⋅𝑒B=−A⋅𝑒B
121 120 oveq1d ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→−A⋅𝑒B⋅𝑒C=−A⋅𝑒B⋅𝑒C
122 xmulneg1 ⊢A⋅𝑒B∈ℝ*∧C∈ℝ*→−A⋅𝑒B⋅𝑒C=−A⋅𝑒B⋅𝑒C
123 9 122 stoic3 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→−A⋅𝑒B⋅𝑒C=−A⋅𝑒B⋅𝑒C
124 121 123 eqtrd ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→−A⋅𝑒B⋅𝑒C=−A⋅𝑒B⋅𝑒C
125 xmulneg1 ⊢A∈ℝ*∧B⋅𝑒C∈ℝ*→−A⋅𝑒B⋅𝑒C=−A⋅𝑒B⋅𝑒C
126 12 14 125 syl2anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→−A⋅𝑒B⋅𝑒C=−A⋅𝑒B⋅𝑒C
127 4 8 11 16 12 107 118 124 126 xmulasslem ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→A⋅𝑒B⋅𝑒C=A⋅𝑒B⋅𝑒C