Metamath Proof Explorer

Theorem hhssabloilem

Description: Lemma for hhssabloi . Formerly part of proof for hhssabloi which was based on the deprecated definition "SubGrpOp" for subgroups. (Contributed by NM, 9-Apr-2008) (Revised by Mario Carneiro, 23-Dec-2013) (Revised by AV, 27-Aug-2021) (New usage is discouraged.)

Ref Expression
Hypothesis hhssabl.1 ⊢ 𝐻 ∈ Sℋ
Assertion hhssabloilem ( +ℎ ∈ GrpOp ∧ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ∈ GrpOp ∧ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ⊆ +ℎ )

Proof

Step Hyp Ref Expression
1 hhssabl.1 ⊢ 𝐻 ∈ Sℋ
2 hilablo ⊢ +ℎ ∈ AbelOp
3 ablogrpo ⊢ ( +ℎ ∈ AbelOp → +ℎ ∈ GrpOp )
4 2 3 ax-mp ⊢ +ℎ ∈ GrpOp
5 1 elexi ⊢ 𝐻 ∈ V
6 eqid ⊢ ran +ℎ = ran +ℎ
7 6 grpofo ⊢ ( +ℎ ∈ GrpOp → +ℎ : ( ran +ℎ × ran +ℎ ) –onto→ ran +ℎ )
8 fof ⊢ ( +ℎ : ( ran +ℎ × ran +ℎ ) –onto→ ran +ℎ → +ℎ : ( ran +ℎ × ran +ℎ ) ⟶ ran +ℎ )
9 4 7 8 mp2b ⊢ +ℎ : ( ran +ℎ × ran +ℎ ) ⟶ ran +ℎ
10 1 shssii ⊢ 𝐻 ⊆ ℋ
11 df-hba ⊢ ℋ = ( BaseSet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
12 eqid ⊢ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
13 12 hhva ⊢ +ℎ = ( +𝑣 ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
14 11 13 bafval ⊢ ℋ = ran +ℎ
15 10 14 sseqtri ⊢ 𝐻 ⊆ ran +ℎ
16 xpss12 ⊢ ( ( 𝐻 ⊆ ran +ℎ ∧ 𝐻 ⊆ ran +ℎ ) → ( 𝐻 × 𝐻 ) ⊆ ( ran +ℎ × ran +ℎ ) )
17 15 15 16 mp2an ⊢ ( 𝐻 × 𝐻 ) ⊆ ( ran +ℎ × ran +ℎ )
18 fssres ⊢ ( ( +ℎ : ( ran +ℎ × ran +ℎ ) ⟶ ran +ℎ ∧ ( 𝐻 × 𝐻 ) ⊆ ( ran +ℎ × ran +ℎ ) ) → ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) : ( 𝐻 × 𝐻 ) ⟶ ran +ℎ )
19 9 17 18 mp2an ⊢ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) : ( 𝐻 × 𝐻 ) ⟶ ran +ℎ
20 ffn ⊢ ( ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) : ( 𝐻 × 𝐻 ) ⟶ ran +ℎ → ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) Fn ( 𝐻 × 𝐻 ) )
21 19 20 ax-mp ⊢ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) Fn ( 𝐻 × 𝐻 )
22 ovres ⊢ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) → ( 𝑥 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑦 ) = ( 𝑥 +ℎ 𝑦 ) )
23 shaddcl ⊢ ( ( 𝐻 ∈ Sℋ ∧ 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) → ( 𝑥 +ℎ 𝑦 ) ∈ 𝐻 )
24 1 23 mp3an1 ⊢ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) → ( 𝑥 +ℎ 𝑦 ) ∈ 𝐻 )
25 22 24 eqeltrd ⊢ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) → ( 𝑥 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑦 ) ∈ 𝐻 )
26 25 rgen2 ⊢ ∀ 𝑥 ∈ 𝐻 ∀ 𝑦 ∈ 𝐻 ( 𝑥 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑦 ) ∈ 𝐻
27 ffnov ⊢ ( ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) : ( 𝐻 × 𝐻 ) ⟶ 𝐻 ↔ ( ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) Fn ( 𝐻 × 𝐻 ) ∧ ∀ 𝑥 ∈ 𝐻 ∀ 𝑦 ∈ 𝐻 ( 𝑥 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑦 ) ∈ 𝐻 ) )
28 21 26 27 mpbir2an ⊢ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) : ( 𝐻 × 𝐻 ) ⟶ 𝐻
29 22 oveq1d ⊢ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) → ( ( 𝑥 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑦 ) +ℎ 𝑧 ) = ( ( 𝑥 +ℎ 𝑦 ) +ℎ 𝑧 ) )
30 29 3adant3 ⊢ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) → ( ( 𝑥 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑦 ) +ℎ 𝑧 ) = ( ( 𝑥 +ℎ 𝑦 ) +ℎ 𝑧 ) )
31 ovres ⊢ ( ( ( 𝑥 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑦 ) ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) → ( ( 𝑥 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑦 ) ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑧 ) = ( ( 𝑥 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑦 ) +ℎ 𝑧 ) )
32 25 31 stoic3 ⊢ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) → ( ( 𝑥 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑦 ) ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑧 ) = ( ( 𝑥 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑦 ) +ℎ 𝑧 ) )
33 ovres ⊢ ( ( 𝑦 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) → ( 𝑦 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑧 ) = ( 𝑦 +ℎ 𝑧 ) )
34 33 oveq2d ⊢ ( ( 𝑦 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) → ( 𝑥 +ℎ ( 𝑦 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑧 ) ) = ( 𝑥 +ℎ ( 𝑦 +ℎ 𝑧 ) ) )
35 34 3adant1 ⊢ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) → ( 𝑥 +ℎ ( 𝑦 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑧 ) ) = ( 𝑥 +ℎ ( 𝑦 +ℎ 𝑧 ) ) )
36 28 fovcl ⊢ ( ( 𝑦 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) → ( 𝑦 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑧 ) ∈ 𝐻 )
37 ovres ⊢ ( ( 𝑥 ∈ 𝐻 ∧ ( 𝑦 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑧 ) ∈ 𝐻 ) → ( 𝑥 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ( 𝑦 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑧 ) ) = ( 𝑥 +ℎ ( 𝑦 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑧 ) ) )
38 36 37 sylan2 ⊢ ( ( 𝑥 ∈ 𝐻 ∧ ( 𝑦 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) ) → ( 𝑥 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ( 𝑦 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑧 ) ) = ( 𝑥 +ℎ ( 𝑦 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑧 ) ) )
39 38 3impb ⊢ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) → ( 𝑥 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ( 𝑦 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑧 ) ) = ( 𝑥 +ℎ ( 𝑦 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑧 ) ) )
40 15 sseli ⊢ ( 𝑥 ∈ 𝐻 → 𝑥 ∈ ran +ℎ )
41 15 sseli ⊢ ( 𝑦 ∈ 𝐻 → 𝑦 ∈ ran +ℎ )
42 15 sseli ⊢ ( 𝑧 ∈ 𝐻 → 𝑧 ∈ ran +ℎ )
43 6 grpoass ⊢ ( ( +ℎ ∈ GrpOp ∧ ( 𝑥 ∈ ran +ℎ ∧ 𝑦 ∈ ran +ℎ ∧ 𝑧 ∈ ran +ℎ ) ) → ( ( 𝑥 +ℎ 𝑦 ) +ℎ 𝑧 ) = ( 𝑥 +ℎ ( 𝑦 +ℎ 𝑧 ) ) )
44 4 43 mpan ⊢ ( ( 𝑥 ∈ ran +ℎ ∧ 𝑦 ∈ ran +ℎ ∧ 𝑧 ∈ ran +ℎ ) → ( ( 𝑥 +ℎ 𝑦 ) +ℎ 𝑧 ) = ( 𝑥 +ℎ ( 𝑦 +ℎ 𝑧 ) ) )
45 40 41 42 44 syl3an ⊢ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) → ( ( 𝑥 +ℎ 𝑦 ) +ℎ 𝑧 ) = ( 𝑥 +ℎ ( 𝑦 +ℎ 𝑧 ) ) )
46 35 39 45 3eqtr4d ⊢ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) → ( 𝑥 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ( 𝑦 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑧 ) ) = ( ( 𝑥 +ℎ 𝑦 ) +ℎ 𝑧 ) )
47 30 32 46 3eqtr4d ⊢ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) → ( ( 𝑥 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑦 ) ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑧 ) = ( 𝑥 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ( 𝑦 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑧 ) ) )
48 hilid ⊢ ( GId ‘ +ℎ ) = 0ℎ
49 sh0 ⊢ ( 𝐻 ∈ Sℋ → 0ℎ ∈ 𝐻 )
50 1 49 ax-mp ⊢ 0ℎ ∈ 𝐻
51 48 50 eqeltri ⊢ ( GId ‘ +ℎ ) ∈ 𝐻
52 ovres ⊢ ( ( ( GId ‘ +ℎ ) ∈ 𝐻 ∧ 𝑥 ∈ 𝐻 ) → ( ( GId ‘ +ℎ ) ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑥 ) = ( ( GId ‘ +ℎ ) +ℎ 𝑥 ) )
53 51 52 mpan ⊢ ( 𝑥 ∈ 𝐻 → ( ( GId ‘ +ℎ ) ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑥 ) = ( ( GId ‘ +ℎ ) +ℎ 𝑥 ) )
54 eqid ⊢ ( GId ‘ +ℎ ) = ( GId ‘ +ℎ )
55 6 54 grpolid ⊢ ( ( +ℎ ∈ GrpOp ∧ 𝑥 ∈ ran +ℎ ) → ( ( GId ‘ +ℎ ) +ℎ 𝑥 ) = 𝑥 )
56 4 40 55 sylancr ⊢ ( 𝑥 ∈ 𝐻 → ( ( GId ‘ +ℎ ) +ℎ 𝑥 ) = 𝑥 )
57 53 56 eqtrd ⊢ ( 𝑥 ∈ 𝐻 → ( ( GId ‘ +ℎ ) ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑥 ) = 𝑥 )
58 12 hhnv ⊢ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ∈ NrmCVec
59 12 hhsm ⊢ ·ℎ = ( ·𝑠OLD ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
60 eqid ⊢ ( ·ℎ ∘ ◡ ( 2nd ↾ ( { - 1 } × V ) ) ) = ( ·ℎ ∘ ◡ ( 2nd ↾ ( { - 1 } × V ) ) )
61 13 59 60 nvinvfval ⊢ ( ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ∈ NrmCVec → ( ·ℎ ∘ ◡ ( 2nd ↾ ( { - 1 } × V ) ) ) = ( inv ‘ +ℎ ) )
62 58 61 ax-mp ⊢ ( ·ℎ ∘ ◡ ( 2nd ↾ ( { - 1 } × V ) ) ) = ( inv ‘ +ℎ )
63 62 eqcomi ⊢ ( inv ‘ +ℎ ) = ( ·ℎ ∘ ◡ ( 2nd ↾ ( { - 1 } × V ) ) )
64 63 fveq1i ⊢ ( ( inv ‘ +ℎ ) ‘ 𝑥 ) = ( ( ·ℎ ∘ ◡ ( 2nd ↾ ( { - 1 } × V ) ) ) ‘ 𝑥 )
65 ax-hfvmul ⊢ ·ℎ : ( ℂ × ℋ ) ⟶ ℋ
66 ffn ⊢ ( ·ℎ : ( ℂ × ℋ ) ⟶ ℋ → ·ℎ Fn ( ℂ × ℋ ) )
67 65 66 ax-mp ⊢ ·ℎ Fn ( ℂ × ℋ )
68 neg1cn ⊢ - 1 ∈ ℂ
69 60 curry1val ⊢ ( ( ·ℎ Fn ( ℂ × ℋ ) ∧ - 1 ∈ ℂ ) → ( ( ·ℎ ∘ ◡ ( 2nd ↾ ( { - 1 } × V ) ) ) ‘ 𝑥 ) = ( - 1 ·ℎ 𝑥 ) )
70 67 68 69 mp2an ⊢ ( ( ·ℎ ∘ ◡ ( 2nd ↾ ( { - 1 } × V ) ) ) ‘ 𝑥 ) = ( - 1 ·ℎ 𝑥 )
71 shmulcl ⊢ ( ( 𝐻 ∈ Sℋ ∧ - 1 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ) → ( - 1 ·ℎ 𝑥 ) ∈ 𝐻 )
72 1 68 71 mp3an12 ⊢ ( 𝑥 ∈ 𝐻 → ( - 1 ·ℎ 𝑥 ) ∈ 𝐻 )
73 70 72 eqeltrid ⊢ ( 𝑥 ∈ 𝐻 → ( ( ·ℎ ∘ ◡ ( 2nd ↾ ( { - 1 } × V ) ) ) ‘ 𝑥 ) ∈ 𝐻 )
74 64 73 eqeltrid ⊢ ( 𝑥 ∈ 𝐻 → ( ( inv ‘ +ℎ ) ‘ 𝑥 ) ∈ 𝐻 )
75 ovres ⊢ ( ( ( ( inv ‘ +ℎ ) ‘ 𝑥 ) ∈ 𝐻 ∧ 𝑥 ∈ 𝐻 ) → ( ( ( inv ‘ +ℎ ) ‘ 𝑥 ) ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑥 ) = ( ( ( inv ‘ +ℎ ) ‘ 𝑥 ) +ℎ 𝑥 ) )
76 74 75 mpancom ⊢ ( 𝑥 ∈ 𝐻 → ( ( ( inv ‘ +ℎ ) ‘ 𝑥 ) ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑥 ) = ( ( ( inv ‘ +ℎ ) ‘ 𝑥 ) +ℎ 𝑥 ) )
77 eqid ⊢ ( inv ‘ +ℎ ) = ( inv ‘ +ℎ )
78 6 54 77 grpolinv ⊢ ( ( +ℎ ∈ GrpOp ∧ 𝑥 ∈ ran +ℎ ) → ( ( ( inv ‘ +ℎ ) ‘ 𝑥 ) +ℎ 𝑥 ) = ( GId ‘ +ℎ ) )
79 4 40 78 sylancr ⊢ ( 𝑥 ∈ 𝐻 → ( ( ( inv ‘ +ℎ ) ‘ 𝑥 ) +ℎ 𝑥 ) = ( GId ‘ +ℎ ) )
80 76 79 eqtrd ⊢ ( 𝑥 ∈ 𝐻 → ( ( ( inv ‘ +ℎ ) ‘ 𝑥 ) ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑥 ) = ( GId ‘ +ℎ ) )
81 5 28 47 51 57 74 80 isgrpoi ⊢ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ∈ GrpOp
82 resss ⊢ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ⊆ +ℎ
83 4 81 82 3pm3.2i ⊢ ( +ℎ ∈ GrpOp ∧ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ∈ GrpOp ∧ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ⊆ +ℎ )