Metamath Proof Explorer


Theorem h1de2ctlem

Description: Lemma for h1de2ci . (Contributed by NM, 19-Jul-2001) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses h1de2.1 A
h1de2.2 B
Assertion h1de2ctlem A B x A = x B

Proof

Step Hyp Ref Expression
1 h1de2.1 A
2 h1de2.2 B
3 sneq B = 0 B = 0
4 3 fveq2d B = 0 B = 0
5 4 fveq2d B = 0 B = 0
6 5 eleq2d B = 0 A B A 0
7 1 elexi A V
8 7 elsn A 0 A = 0
9 hsn0elch 0 C
10 9 ococi 0 = 0
11 10 eleq2i A 0 A 0
12 ax-hvmul0 B 0 B = 0
13 2 12 ax-mp 0 B = 0
14 13 eqeq2i A = 0 B A = 0
15 8 11 14 3bitr4ri A = 0 B A 0
16 6 15 syl6rbbr B = 0 A = 0 B A B
17 0cn 0
18 oveq1 x = 0 x B = 0 B
19 18 rspceeqv 0 A = 0 B x A = x B
20 17 19 mpan A = 0 B x A = x B
21 16 20 syl6bir B = 0 A B x A = x B
22 1 2 h1de2bi B 0 A B A = A ih B B ih B B
23 his6 B B ih B = 0 B = 0
24 2 23 ax-mp B ih B = 0 B = 0
25 24 necon3bii B ih B 0 B 0
26 1 2 hicli A ih B
27 2 2 hicli B ih B
28 26 27 divclzi B ih B 0 A ih B B ih B
29 25 28 sylbir B 0 A ih B B ih B
30 oveq1 x = A ih B B ih B x B = A ih B B ih B B
31 30 rspceeqv A ih B B ih B A = A ih B B ih B B x A = x B
32 29 31 sylan B 0 A = A ih B B ih B B x A = x B
33 32 ex B 0 A = A ih B B ih B B x A = x B
34 22 33 sylbid B 0 A B x A = x B
35 21 34 pm2.61ine A B x A = x B
36 snssi B B
37 occl B B C
38 2 36 37 mp2b B C
39 38 choccli B C
40 39 chshii B S
41 h1did B B B
42 2 41 ax-mp B B
43 shmulcl B S x B B x B B
44 40 42 43 mp3an13 x x B B
45 eleq1 A = x B A B x B B
46 44 45 syl5ibrcom x A = x B A B
47 46 rexlimiv x A = x B A B
48 35 47 impbii A B x A = x B