Metamath Proof Explorer


Theorem mulsproplemcbv

Description: Lemma for surreal multiplication. Change some bound variables for later use. (Contributed by Scott Fenton, 5-Mar-2025)

Ref Expression
Hypothesis mulsproplem.1 φ a No b No c No d No e No f No bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e
Assertion mulsproplemcbv φ g No h No i No j No k No l No bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E g s h No i < s j k < s l i s l - s i s k < s j s l - s j s k

Proof

Step Hyp Ref Expression
1 mulsproplem.1 φ a No b No c No d No e No f No bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e
2 fveq2 a = g bday a = bday g
3 2 oveq1d a = g bday a + bday b = bday g + bday b
4 3 uneq1d a = g bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e = bday g + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e
5 4 eleq1d a = g bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E bday g + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
6 oveq1 a = g a s b = g s b
7 6 eleq1d a = g a s b No g s b No
8 7 anbi1d a = g a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e g s b No c < s d e < s f c s f - s c s e < s d s f - s d s e
9 5 8 imbi12d a = g bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e bday g + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E g s b No c < s d e < s f c s f - s c s e < s d s f - s d s e
10 fveq2 b = h bday b = bday h
11 10 oveq2d b = h bday g + bday b = bday g + bday h
12 11 uneq1d b = h bday g + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e = bday g + bday h bday c + bday e bday d + bday f bday c + bday f bday d + bday e
13 12 eleq1d b = h bday g + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E bday g + bday h bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
14 oveq2 b = h g s b = g s h
15 14 eleq1d b = h g s b No g s h No
16 15 anbi1d b = h g s b No c < s d e < s f c s f - s c s e < s d s f - s d s e g s h No c < s d e < s f c s f - s c s e < s d s f - s d s e
17 13 16 imbi12d b = h bday g + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E g s b No c < s d e < s f c s f - s c s e < s d s f - s d s e bday g + bday h bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E g s h No c < s d e < s f c s f - s c s e < s d s f - s d s e
18 fveq2 c = i bday c = bday i
19 18 oveq1d c = i bday c + bday e = bday i + bday e
20 19 uneq1d c = i bday c + bday e bday d + bday f = bday i + bday e bday d + bday f
21 18 oveq1d c = i bday c + bday f = bday i + bday f
22 21 uneq1d c = i bday c + bday f bday d + bday e = bday i + bday f bday d + bday e
23 20 22 uneq12d c = i bday c + bday e bday d + bday f bday c + bday f bday d + bday e = bday i + bday e bday d + bday f bday i + bday f bday d + bday e
24 23 uneq2d c = i bday g + bday h bday c + bday e bday d + bday f bday c + bday f bday d + bday e = bday g + bday h bday i + bday e bday d + bday f bday i + bday f bday d + bday e
25 24 eleq1d c = i bday g + bday h bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E bday g + bday h bday i + bday e bday d + bday f bday i + bday f bday d + bday e bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
26 breq1 c = i c < s d i < s d
27 26 anbi1d c = i c < s d e < s f i < s d e < s f
28 oveq1 c = i c s f = i s f
29 oveq1 c = i c s e = i s e
30 28 29 oveq12d c = i c s f - s c s e = i s f - s i s e
31 30 breq1d c = i c s f - s c s e < s d s f - s d s e i s f - s i s e < s d s f - s d s e
32 27 31 imbi12d c = i c < s d e < s f c s f - s c s e < s d s f - s d s e i < s d e < s f i s f - s i s e < s d s f - s d s e
33 32 anbi2d c = i g s h No c < s d e < s f c s f - s c s e < s d s f - s d s e g s h No i < s d e < s f i s f - s i s e < s d s f - s d s e
34 25 33 imbi12d c = i bday g + bday h bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E g s h No c < s d e < s f c s f - s c s e < s d s f - s d s e bday g + bday h bday i + bday e bday d + bday f bday i + bday f bday d + bday e bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E g s h No i < s d e < s f i s f - s i s e < s d s f - s d s e
35 fveq2 d = j bday d = bday j
36 35 oveq1d d = j bday d + bday f = bday j + bday f
37 36 uneq2d d = j bday i + bday e bday d + bday f = bday i + bday e bday j + bday f
38 35 oveq1d d = j bday d + bday e = bday j + bday e
39 38 uneq2d d = j bday i + bday f bday d + bday e = bday i + bday f bday j + bday e
40 37 39 uneq12d d = j bday i + bday e bday d + bday f bday i + bday f bday d + bday e = bday i + bday e bday j + bday f bday i + bday f bday j + bday e
41 40 uneq2d d = j bday g + bday h bday i + bday e bday d + bday f bday i + bday f bday d + bday e = bday g + bday h bday i + bday e bday j + bday f bday i + bday f bday j + bday e
42 41 eleq1d d = j bday g + bday h bday i + bday e bday d + bday f bday i + bday f bday d + bday e bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E bday g + bday h bday i + bday e bday j + bday f bday i + bday f bday j + bday e bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
43 breq2 d = j i < s d i < s j
44 43 anbi1d d = j i < s d e < s f i < s j e < s f
45 oveq1 d = j d s f = j s f
46 oveq1 d = j d s e = j s e
47 45 46 oveq12d d = j d s f - s d s e = j s f - s j s e
48 47 breq2d d = j i s f - s i s e < s d s f - s d s e i s f - s i s e < s j s f - s j s e
49 44 48 imbi12d d = j i < s d e < s f i s f - s i s e < s d s f - s d s e i < s j e < s f i s f - s i s e < s j s f - s j s e
50 49 anbi2d d = j g s h No i < s d e < s f i s f - s i s e < s d s f - s d s e g s h No i < s j e < s f i s f - s i s e < s j s f - s j s e
51 42 50 imbi12d d = j bday g + bday h bday i + bday e bday d + bday f bday i + bday f bday d + bday e bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E g s h No i < s d e < s f i s f - s i s e < s d s f - s d s e bday g + bday h bday i + bday e bday j + bday f bday i + bday f bday j + bday e bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E g s h No i < s j e < s f i s f - s i s e < s j s f - s j s e
52 fveq2 e = k bday e = bday k
53 52 oveq2d e = k bday i + bday e = bday i + bday k
54 53 uneq1d e = k bday i + bday e bday j + bday f = bday i + bday k bday j + bday f
55 52 oveq2d e = k bday j + bday e = bday j + bday k
56 55 uneq2d e = k bday i + bday f bday j + bday e = bday i + bday f bday j + bday k
57 54 56 uneq12d e = k bday i + bday e bday j + bday f bday i + bday f bday j + bday e = bday i + bday k bday j + bday f bday i + bday f bday j + bday k
58 57 uneq2d e = k bday g + bday h bday i + bday e bday j + bday f bday i + bday f bday j + bday e = bday g + bday h bday i + bday k bday j + bday f bday i + bday f bday j + bday k
59 58 eleq1d e = k bday g + bday h bday i + bday e bday j + bday f bday i + bday f bday j + bday e bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E bday g + bday h bday i + bday k bday j + bday f bday i + bday f bday j + bday k bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
60 breq1 e = k e < s f k < s f
61 60 anbi2d e = k i < s j e < s f i < s j k < s f
62 oveq2 e = k i s e = i s k
63 62 oveq2d e = k i s f - s i s e = i s f - s i s k
64 oveq2 e = k j s e = j s k
65 64 oveq2d e = k j s f - s j s e = j s f - s j s k
66 63 65 breq12d e = k i s f - s i s e < s j s f - s j s e i s f - s i s k < s j s f - s j s k
67 61 66 imbi12d e = k i < s j e < s f i s f - s i s e < s j s f - s j s e i < s j k < s f i s f - s i s k < s j s f - s j s k
68 67 anbi2d e = k g s h No i < s j e < s f i s f - s i s e < s j s f - s j s e g s h No i < s j k < s f i s f - s i s k < s j s f - s j s k
69 59 68 imbi12d e = k bday g + bday h bday i + bday e bday j + bday f bday i + bday f bday j + bday e bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E g s h No i < s j e < s f i s f - s i s e < s j s f - s j s e bday g + bday h bday i + bday k bday j + bday f bday i + bday f bday j + bday k bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E g s h No i < s j k < s f i s f - s i s k < s j s f - s j s k
70 fveq2 f = l bday f = bday l
71 70 oveq2d f = l bday j + bday f = bday j + bday l
72 71 uneq2d f = l bday i + bday k bday j + bday f = bday i + bday k bday j + bday l
73 70 oveq2d f = l bday i + bday f = bday i + bday l
74 73 uneq1d f = l bday i + bday f bday j + bday k = bday i + bday l bday j + bday k
75 72 74 uneq12d f = l bday i + bday k bday j + bday f bday i + bday f bday j + bday k = bday i + bday k bday j + bday l bday i + bday l bday j + bday k
76 75 uneq2d f = l bday g + bday h bday i + bday k bday j + bday f bday i + bday f bday j + bday k = bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k
77 76 eleq1d f = l bday g + bday h bday i + bday k bday j + bday f bday i + bday f bday j + bday k bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
78 breq2 f = l k < s f k < s l
79 78 anbi2d f = l i < s j k < s f i < s j k < s l
80 oveq2 f = l i s f = i s l
81 80 oveq1d f = l i s f - s i s k = i s l - s i s k
82 oveq2 f = l j s f = j s l
83 82 oveq1d f = l j s f - s j s k = j s l - s j s k
84 81 83 breq12d f = l i s f - s i s k < s j s f - s j s k i s l - s i s k < s j s l - s j s k
85 79 84 imbi12d f = l i < s j k < s f i s f - s i s k < s j s f - s j s k i < s j k < s l i s l - s i s k < s j s l - s j s k
86 85 anbi2d f = l g s h No i < s j k < s f i s f - s i s k < s j s f - s j s k g s h No i < s j k < s l i s l - s i s k < s j s l - s j s k
87 77 86 imbi12d f = l bday g + bday h bday i + bday k bday j + bday f bday i + bday f bday j + bday k bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E g s h No i < s j k < s f i s f - s i s k < s j s f - s j s k bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E g s h No i < s j k < s l i s l - s i s k < s j s l - s j s k
88 9 17 34 51 69 87 cbvral6vw a No b No c No d No e No f No bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e g No h No i No j No k No l No bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E g s h No i < s j k < s l i s l - s i s k < s j s l - s j s k
89 1 88 sylib φ g No h No i No j No k No l No bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E g s h No i < s j k < s l i s l - s i s k < s j s l - s j s k