Metamath Proof Explorer

Theorem isthincd2lem2

Description: Lemma for isthincd2 . (Contributed by Zhi Wang, 17-Sep-2024)

Ref Expression
Hypotheses isthincd2lem2.1 ⊢ φ → X ∈ B
isthincd2lem2.2 ⊢ φ → Y ∈ B
isthincd2lem2.3 ⊢ φ → Z ∈ B
isthincd2lem2.4 ⊢ φ → F ∈ X H Y
isthincd2lem2.5 ⊢ φ → G ∈ Y H Z
isthincd2lem2.6 ⊢ φ → ∀ x ∈ B ∀ y ∈ B ∀ z ∈ B ∀ f ∈ x H y ∀ g ∈ y H z g x y · ˙ z f ∈ x H z
Assertion isthincd2lem2 ⊢ φ → G X Y · ˙ Z F ∈ X H Z

Proof

Step Hyp Ref Expression
1 isthincd2lem2.1 ⊢ φ → X ∈ B
2 isthincd2lem2.2 ⊢ φ → Y ∈ B
3 isthincd2lem2.3 ⊢ φ → Z ∈ B
4 isthincd2lem2.4 ⊢ φ → F ∈ X H Y
5 isthincd2lem2.5 ⊢ φ → G ∈ Y H Z
6 isthincd2lem2.6 ⊢ φ → ∀ x ∈ B ∀ y ∈ B ∀ z ∈ B ∀ f ∈ x H y ∀ g ∈ y H z g x y · ˙ z f ∈ x H z
7 oveq1 ⊢ x = w → x H y = w H y
8 opeq1 ⊢ x = w → x y = w y
9 8 oveq1d ⊢ x = w → x y · ˙ z = w y · ˙ z
10 9 oveqd ⊢ x = w → g x y · ˙ z f = g w y · ˙ z f
11 oveq1 ⊢ x = w → x H z = w H z
12 10 11 eleq12d ⊢ x = w → g x y · ˙ z f ∈ x H z ↔ g w y · ˙ z f ∈ w H z
13 12 ralbidv ⊢ x = w → ∀ g ∈ y H z g x y · ˙ z f ∈ x H z ↔ ∀ g ∈ y H z g w y · ˙ z f ∈ w H z
14 7 13 raleqbidv ⊢ x = w → ∀ f ∈ x H y ∀ g ∈ y H z g x y · ˙ z f ∈ x H z ↔ ∀ f ∈ w H y ∀ g ∈ y H z g w y · ˙ z f ∈ w H z
15 oveq2 ⊢ y = v → w H y = w H v
16 oveq1 ⊢ y = v → y H z = v H z
17 opeq2 ⊢ y = v → w y = w v
18 17 oveq1d ⊢ y = v → w y · ˙ z = w v · ˙ z
19 18 oveqd ⊢ y = v → g w y · ˙ z f = g w v · ˙ z f
20 19 eleq1d ⊢ y = v → g w y · ˙ z f ∈ w H z ↔ g w v · ˙ z f ∈ w H z
21 16 20 raleqbidv ⊢ y = v → ∀ g ∈ y H z g w y · ˙ z f ∈ w H z ↔ ∀ g ∈ v H z g w v · ˙ z f ∈ w H z
22 15 21 raleqbidv ⊢ y = v → ∀ f ∈ w H y ∀ g ∈ y H z g w y · ˙ z f ∈ w H z ↔ ∀ f ∈ w H v ∀ g ∈ v H z g w v · ˙ z f ∈ w H z
23 oveq2 ⊢ z = u → v H z = v H u
24 oveq2 ⊢ z = u → w v · ˙ z = w v · ˙ u
25 24 oveqd ⊢ z = u → g w v · ˙ z f = g w v · ˙ u f
26 oveq2 ⊢ z = u → w H z = w H u
27 25 26 eleq12d ⊢ z = u → g w v · ˙ z f ∈ w H z ↔ g w v · ˙ u f ∈ w H u
28 23 27 raleqbidv ⊢ z = u → ∀ g ∈ v H z g w v · ˙ z f ∈ w H z ↔ ∀ g ∈ v H u g w v · ˙ u f ∈ w H u
29 28 ralbidv ⊢ z = u → ∀ f ∈ w H v ∀ g ∈ v H z g w v · ˙ z f ∈ w H z ↔ ∀ f ∈ w H v ∀ g ∈ v H u g w v · ˙ u f ∈ w H u
30 oveq2 ⊢ f = k → g w v · ˙ u f = g w v · ˙ u k
31 30 eleq1d ⊢ f = k → g w v · ˙ u f ∈ w H u ↔ g w v · ˙ u k ∈ w H u
32 oveq1 ⊢ g = l → g w v · ˙ u k = l w v · ˙ u k
33 32 eleq1d ⊢ g = l → g w v · ˙ u k ∈ w H u ↔ l w v · ˙ u k ∈ w H u
34 31 33 cbvral2vw ⊢ ∀ f ∈ w H v ∀ g ∈ v H u g w v · ˙ u f ∈ w H u ↔ ∀ k ∈ w H v ∀ l ∈ v H u l w v · ˙ u k ∈ w H u
35 29 34 bitrdi ⊢ z = u → ∀ f ∈ w H v ∀ g ∈ v H z g w v · ˙ z f ∈ w H z ↔ ∀ k ∈ w H v ∀ l ∈ v H u l w v · ˙ u k ∈ w H u
36 14 22 35 cbvral3vw ⊢ ∀ x ∈ B ∀ y ∈ B ∀ z ∈ B ∀ f ∈ x H y ∀ g ∈ y H z g x y · ˙ z f ∈ x H z ↔ ∀ w ∈ B ∀ v ∈ B ∀ u ∈ B ∀ k ∈ w H v ∀ l ∈ v H u l w v · ˙ u k ∈ w H u
37 6 36 sylib ⊢ φ → ∀ w ∈ B ∀ v ∈ B ∀ u ∈ B ∀ k ∈ w H v ∀ l ∈ v H u l w v · ˙ u k ∈ w H u
38 oveq1 ⊢ w = X → w H v = X H v
39 opeq1 ⊢ w = X → w v = X v
40 39 oveq1d ⊢ w = X → w v · ˙ u = X v · ˙ u
41 40 oveqd ⊢ w = X → l w v · ˙ u k = l X v · ˙ u k
42 oveq1 ⊢ w = X → w H u = X H u
43 41 42 eleq12d ⊢ w = X → l w v · ˙ u k ∈ w H u ↔ l X v · ˙ u k ∈ X H u
44 43 ralbidv ⊢ w = X → ∀ l ∈ v H u l w v · ˙ u k ∈ w H u ↔ ∀ l ∈ v H u l X v · ˙ u k ∈ X H u
45 38 44 raleqbidv ⊢ w = X → ∀ k ∈ w H v ∀ l ∈ v H u l w v · ˙ u k ∈ w H u ↔ ∀ k ∈ X H v ∀ l ∈ v H u l X v · ˙ u k ∈ X H u
46 oveq2 ⊢ v = Y → X H v = X H Y
47 oveq1 ⊢ v = Y → v H u = Y H u
48 opeq2 ⊢ v = Y → X v = X Y
49 48 oveq1d ⊢ v = Y → X v · ˙ u = X Y · ˙ u
50 49 oveqd ⊢ v = Y → l X v · ˙ u k = l X Y · ˙ u k
51 50 eleq1d ⊢ v = Y → l X v · ˙ u k ∈ X H u ↔ l X Y · ˙ u k ∈ X H u
52 47 51 raleqbidv ⊢ v = Y → ∀ l ∈ v H u l X v · ˙ u k ∈ X H u ↔ ∀ l ∈ Y H u l X Y · ˙ u k ∈ X H u
53 46 52 raleqbidv ⊢ v = Y → ∀ k ∈ X H v ∀ l ∈ v H u l X v · ˙ u k ∈ X H u ↔ ∀ k ∈ X H Y ∀ l ∈ Y H u l X Y · ˙ u k ∈ X H u
54 oveq2 ⊢ u = Z → Y H u = Y H Z
55 oveq2 ⊢ u = Z → X Y · ˙ u = X Y · ˙ Z
56 55 oveqd ⊢ u = Z → l X Y · ˙ u k = l X Y · ˙ Z k
57 oveq2 ⊢ u = Z → X H u = X H Z
58 56 57 eleq12d ⊢ u = Z → l X Y · ˙ u k ∈ X H u ↔ l X Y · ˙ Z k ∈ X H Z
59 54 58 raleqbidv ⊢ u = Z → ∀ l ∈ Y H u l X Y · ˙ u k ∈ X H u ↔ ∀ l ∈ Y H Z l X Y · ˙ Z k ∈ X H Z
60 59 ralbidv ⊢ u = Z → ∀ k ∈ X H Y ∀ l ∈ Y H u l X Y · ˙ u k ∈ X H u ↔ ∀ k ∈ X H Y ∀ l ∈ Y H Z l X Y · ˙ Z k ∈ X H Z
61 45 53 60 rspc3v ⊢ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → ∀ w ∈ B ∀ v ∈ B ∀ u ∈ B ∀ k ∈ w H v ∀ l ∈ v H u l w v · ˙ u k ∈ w H u → ∀ k ∈ X H Y ∀ l ∈ Y H Z l X Y · ˙ Z k ∈ X H Z
62 1 2 3 61 syl3anc ⊢ φ → ∀ w ∈ B ∀ v ∈ B ∀ u ∈ B ∀ k ∈ w H v ∀ l ∈ v H u l w v · ˙ u k ∈ w H u → ∀ k ∈ X H Y ∀ l ∈ Y H Z l X Y · ˙ Z k ∈ X H Z
63 37 62 mpd ⊢ φ → ∀ k ∈ X H Y ∀ l ∈ Y H Z l X Y · ˙ Z k ∈ X H Z
64 oveq2 ⊢ k = F → l X Y · ˙ Z k = l X Y · ˙ Z F
65 64 eleq1d ⊢ k = F → l X Y · ˙ Z k ∈ X H Z ↔ l X Y · ˙ Z F ∈ X H Z
66 oveq1 ⊢ l = G → l X Y · ˙ Z F = G X Y · ˙ Z F
67 66 eleq1d ⊢ l = G → l X Y · ˙ Z F ∈ X H Z ↔ G X Y · ˙ Z F ∈ X H Z
68 65 67 rspc2v ⊢ F ∈ X H Y ∧ G ∈ Y H Z → ∀ k ∈ X H Y ∀ l ∈ Y H Z l X Y · ˙ Z k ∈ X H Z → G X Y · ˙ Z F ∈ X H Z
69 4 5 68 syl2anc ⊢ φ → ∀ k ∈ X H Y ∀ l ∈ Y H Z l X Y · ˙ Z k ∈ X H Z → G X Y · ˙ Z F ∈ X H Z
70 63 69 mpd ⊢ φ → G X Y · ˙ Z F ∈ X H Z