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 e. ~H
h1de2.2 
|- B e. ~H
Assertion h1de2ctlem 
|- ( A e. ( _|_ ` ( _|_ ` { B } ) ) <-> E. x e. CC A = ( x .h B ) )

Proof

Step Hyp Ref Expression
1 h1de2.1 
 |-  A e. ~H
2 h1de2.2 
 |-  B e. ~H
3 1 elexi 
 |-  A e. _V
4 3 elsn 
 |-  ( A e. { 0h } <-> A = 0h )
5 hsn0elch 
 |-  { 0h } e. CH
6 5 ococi 
 |-  ( _|_ ` ( _|_ ` { 0h } ) ) = { 0h }
7 6 eleq2i 
 |-  ( A e. ( _|_ ` ( _|_ ` { 0h } ) ) <-> A e. { 0h } )
8 ax-hvmul0 
 |-  ( B e. ~H -> ( 0 .h B ) = 0h )
9 2 8 ax-mp 
 |-  ( 0 .h B ) = 0h
10 9 eqeq2i 
 |-  ( A = ( 0 .h B ) <-> A = 0h )
11 4 7 10 3bitr4ri 
 |-  ( A = ( 0 .h B ) <-> A e. ( _|_ ` ( _|_ ` { 0h } ) ) )
12 sneq 
 |-  ( B = 0h -> { B } = { 0h } )
13 12 fveq2d 
 |-  ( B = 0h -> ( _|_ ` { B } ) = ( _|_ ` { 0h } ) )
14 13 fveq2d 
 |-  ( B = 0h -> ( _|_ ` ( _|_ ` { B } ) ) = ( _|_ ` ( _|_ ` { 0h } ) ) )
15 14 eleq2d 
 |-  ( B = 0h -> ( A e. ( _|_ ` ( _|_ ` { B } ) ) <-> A e. ( _|_ ` ( _|_ ` { 0h } ) ) ) )
16 11 15 bitr4id 
 |-  ( B = 0h -> ( A = ( 0 .h B ) <-> A e. ( _|_ ` ( _|_ ` { B } ) ) ) )
17 0cn 
 |-  0 e. CC
18 oveq1 
 |-  ( x = 0 -> ( x .h B ) = ( 0 .h B ) )
19 18 rspceeqv 
 |-  ( ( 0 e. CC /\ A = ( 0 .h B ) ) -> E. x e. CC A = ( x .h B ) )
20 17 19 mpan 
 |-  ( A = ( 0 .h B ) -> E. x e. CC A = ( x .h B ) )
21 16 20 biimtrrdi 
 |-  ( B = 0h -> ( A e. ( _|_ ` ( _|_ ` { B } ) ) -> E. x e. CC A = ( x .h B ) ) )
22 1 2 h1de2bi 
 |-  ( B =/= 0h -> ( A e. ( _|_ ` ( _|_ ` { B } ) ) <-> A = ( ( ( A .ih B ) / ( B .ih B ) ) .h B ) ) )
23 his6 
 |-  ( B e. ~H -> ( ( B .ih B ) = 0 <-> B = 0h ) )
24 2 23 ax-mp 
 |-  ( ( B .ih B ) = 0 <-> B = 0h )
25 24 necon3bii 
 |-  ( ( B .ih B ) =/= 0 <-> B =/= 0h )
26 1 2 hicli 
 |-  ( A .ih B ) e. CC
27 2 2 hicli 
 |-  ( B .ih B ) e. CC
28 26 27 divclzi 
 |-  ( ( B .ih B ) =/= 0 -> ( ( A .ih B ) / ( B .ih B ) ) e. CC )
29 25 28 sylbir 
 |-  ( B =/= 0h -> ( ( A .ih B ) / ( B .ih B ) ) e. CC )
30 oveq1 
 |-  ( x = ( ( A .ih B ) / ( B .ih B ) ) -> ( x .h B ) = ( ( ( A .ih B ) / ( B .ih B ) ) .h B ) )
31 30 rspceeqv 
 |-  ( ( ( ( A .ih B ) / ( B .ih B ) ) e. CC /\ A = ( ( ( A .ih B ) / ( B .ih B ) ) .h B ) ) -> E. x e. CC A = ( x .h B ) )
32 29 31 sylan 
 |-  ( ( B =/= 0h /\ A = ( ( ( A .ih B ) / ( B .ih B ) ) .h B ) ) -> E. x e. CC A = ( x .h B ) )
33 32 ex 
 |-  ( B =/= 0h -> ( A = ( ( ( A .ih B ) / ( B .ih B ) ) .h B ) -> E. x e. CC A = ( x .h B ) ) )
34 22 33 sylbid 
 |-  ( B =/= 0h -> ( A e. ( _|_ ` ( _|_ ` { B } ) ) -> E. x e. CC A = ( x .h B ) ) )
35 21 34 pm2.61ine 
 |-  ( A e. ( _|_ ` ( _|_ ` { B } ) ) -> E. x e. CC A = ( x .h B ) )
36 snssi 
 |-  ( B e. ~H -> { B } C_ ~H )
37 occl 
 |-  ( { B } C_ ~H -> ( _|_ ` { B } ) e. CH )
38 2 36 37 mp2b 
 |-  ( _|_ ` { B } ) e. CH
39 38 choccli 
 |-  ( _|_ ` ( _|_ ` { B } ) ) e. CH
40 39 chshii 
 |-  ( _|_ ` ( _|_ ` { B } ) ) e. SH
41 h1did 
 |-  ( B e. ~H -> B e. ( _|_ ` ( _|_ ` { B } ) ) )
42 2 41 ax-mp 
 |-  B e. ( _|_ ` ( _|_ ` { B } ) )
43 shmulcl 
 |-  ( ( ( _|_ ` ( _|_ ` { B } ) ) e. SH /\ x e. CC /\ B e. ( _|_ ` ( _|_ ` { B } ) ) ) -> ( x .h B ) e. ( _|_ ` ( _|_ ` { B } ) ) )
44 40 42 43 mp3an13 
 |-  ( x e. CC -> ( x .h B ) e. ( _|_ ` ( _|_ ` { B } ) ) )
45 eleq1 
 |-  ( A = ( x .h B ) -> ( A e. ( _|_ ` ( _|_ ` { B } ) ) <-> ( x .h B ) e. ( _|_ ` ( _|_ ` { B } ) ) ) )
46 44 45 syl5ibrcom 
 |-  ( x e. CC -> ( A = ( x .h B ) -> A e. ( _|_ ` ( _|_ ` { B } ) ) ) )
47 46 rexlimiv 
 |-  ( E. x e. CC A = ( x .h B ) -> A e. ( _|_ ` ( _|_ ` { B } ) ) )
48 35 47 impbii 
 |-  ( A e. ( _|_ ` ( _|_ ` { B } ) ) <-> E. x e. CC A = ( x .h B ) )