Metamath Proof Explorer

Theorem isthincd2lem2

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

Ref Expression
Hypotheses isthincd2lem2.1 
|- ( ph -> X e. B )
isthincd2lem2.2 
|- ( ph -> Y e. B )
isthincd2lem2.3 
|- ( ph -> Z e. B )
isthincd2lem2.4 
|- ( ph -> F e. ( X H Y ) )
isthincd2lem2.5 
|- ( ph -> G e. ( Y H Z ) )
isthincd2lem2.6 
|- ( ph -> A. x e. B A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) )
Assertion isthincd2lem2 
|- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X H Z ) )

Proof

Step Hyp Ref Expression
1 isthincd2lem2.1 
 |-  ( ph -> X e. B )
2 isthincd2lem2.2 
 |-  ( ph -> Y e. B )
3 isthincd2lem2.3 
 |-  ( ph -> Z e. B )
4 isthincd2lem2.4 
 |-  ( ph -> F e. ( X H Y ) )
5 isthincd2lem2.5 
 |-  ( ph -> G e. ( Y H Z ) )
6 isthincd2lem2.6 
 |-  ( ph -> A. x e. B A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. .x. z ) f ) e. ( 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 >. .x. z ) = ( <. w , y >. .x. z ) )
10 9 oveqd 
 |-  ( x = w -> ( g ( <. x , y >. .x. z ) f ) = ( g ( <. w , y >. .x. z ) f ) )
11 oveq1 
 |-  ( x = w -> ( x H z ) = ( w H z ) )
12 10 11 eleq12d 
 |-  ( x = w -> ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) <-> ( g ( <. w , y >. .x. z ) f ) e. ( w H z ) ) )
13 12 ralbidv 
 |-  ( x = w -> ( A. g e. ( y H z ) ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) <-> A. g e. ( y H z ) ( g ( <. w , y >. .x. z ) f ) e. ( w H z ) ) )
14 7 13 raleqbidv 
 |-  ( x = w -> ( A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) <-> A. f e. ( w H y ) A. g e. ( y H z ) ( g ( <. w , y >. .x. z ) f ) e. ( 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 >. .x. z ) = ( <. w , v >. .x. z ) )
19 18 oveqd 
 |-  ( y = v -> ( g ( <. w , y >. .x. z ) f ) = ( g ( <. w , v >. .x. z ) f ) )
20 19 eleq1d 
 |-  ( y = v -> ( ( g ( <. w , y >. .x. z ) f ) e. ( w H z ) <-> ( g ( <. w , v >. .x. z ) f ) e. ( w H z ) ) )
21 16 20 raleqbidv 
 |-  ( y = v -> ( A. g e. ( y H z ) ( g ( <. w , y >. .x. z ) f ) e. ( w H z ) <-> A. g e. ( v H z ) ( g ( <. w , v >. .x. z ) f ) e. ( w H z ) ) )
22 15 21 raleqbidv 
 |-  ( y = v -> ( A. f e. ( w H y ) A. g e. ( y H z ) ( g ( <. w , y >. .x. z ) f ) e. ( w H z ) <-> A. f e. ( w H v ) A. g e. ( v H z ) ( g ( <. w , v >. .x. z ) f ) e. ( w H z ) ) )
23 oveq2 
 |-  ( z = u -> ( v H z ) = ( v H u ) )
24 oveq2 
 |-  ( z = u -> ( <. w , v >. .x. z ) = ( <. w , v >. .x. u ) )
25 24 oveqd 
 |-  ( z = u -> ( g ( <. w , v >. .x. z ) f ) = ( g ( <. w , v >. .x. u ) f ) )
26 oveq2 
 |-  ( z = u -> ( w H z ) = ( w H u ) )
27 25 26 eleq12d 
 |-  ( z = u -> ( ( g ( <. w , v >. .x. z ) f ) e. ( w H z ) <-> ( g ( <. w , v >. .x. u ) f ) e. ( w H u ) ) )
28 23 27 raleqbidv 
 |-  ( z = u -> ( A. g e. ( v H z ) ( g ( <. w , v >. .x. z ) f ) e. ( w H z ) <-> A. g e. ( v H u ) ( g ( <. w , v >. .x. u ) f ) e. ( w H u ) ) )
29 28 ralbidv 
 |-  ( z = u -> ( A. f e. ( w H v ) A. g e. ( v H z ) ( g ( <. w , v >. .x. z ) f ) e. ( w H z ) <-> A. f e. ( w H v ) A. g e. ( v H u ) ( g ( <. w , v >. .x. u ) f ) e. ( w H u ) ) )
30 oveq2 
 |-  ( f = k -> ( g ( <. w , v >. .x. u ) f ) = ( g ( <. w , v >. .x. u ) k ) )
31 30 eleq1d 
 |-  ( f = k -> ( ( g ( <. w , v >. .x. u ) f ) e. ( w H u ) <-> ( g ( <. w , v >. .x. u ) k ) e. ( w H u ) ) )
32 oveq1 
 |-  ( g = l -> ( g ( <. w , v >. .x. u ) k ) = ( l ( <. w , v >. .x. u ) k ) )
33 32 eleq1d 
 |-  ( g = l -> ( ( g ( <. w , v >. .x. u ) k ) e. ( w H u ) <-> ( l ( <. w , v >. .x. u ) k ) e. ( w H u ) ) )
34 31 33 cbvral2vw 
 |-  ( A. f e. ( w H v ) A. g e. ( v H u ) ( g ( <. w , v >. .x. u ) f ) e. ( w H u ) <-> A. k e. ( w H v ) A. l e. ( v H u ) ( l ( <. w , v >. .x. u ) k ) e. ( w H u ) )
35 29 34 bitrdi 
 |-  ( z = u -> ( A. f e. ( w H v ) A. g e. ( v H z ) ( g ( <. w , v >. .x. z ) f ) e. ( w H z ) <-> A. k e. ( w H v ) A. l e. ( v H u ) ( l ( <. w , v >. .x. u ) k ) e. ( w H u ) ) )
36 14 22 35 cbvral3vw 
 |-  ( A. x e. B A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) <-> A. w e. B A. v e. B A. u e. B A. k e. ( w H v ) A. l e. ( v H u ) ( l ( <. w , v >. .x. u ) k ) e. ( w H u ) )
37 6 36 sylib 
 |-  ( ph -> A. w e. B A. v e. B A. u e. B A. k e. ( w H v ) A. l e. ( v H u ) ( l ( <. w , v >. .x. u ) k ) e. ( 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 >. .x. u ) = ( <. X , v >. .x. u ) )
41 40 oveqd 
 |-  ( w = X -> ( l ( <. w , v >. .x. u ) k ) = ( l ( <. X , v >. .x. u ) k ) )
42 oveq1 
 |-  ( w = X -> ( w H u ) = ( X H u ) )
43 41 42 eleq12d 
 |-  ( w = X -> ( ( l ( <. w , v >. .x. u ) k ) e. ( w H u ) <-> ( l ( <. X , v >. .x. u ) k ) e. ( X H u ) ) )
44 43 ralbidv 
 |-  ( w = X -> ( A. l e. ( v H u ) ( l ( <. w , v >. .x. u ) k ) e. ( w H u ) <-> A. l e. ( v H u ) ( l ( <. X , v >. .x. u ) k ) e. ( X H u ) ) )
45 38 44 raleqbidv 
 |-  ( w = X -> ( A. k e. ( w H v ) A. l e. ( v H u ) ( l ( <. w , v >. .x. u ) k ) e. ( w H u ) <-> A. k e. ( X H v ) A. l e. ( v H u ) ( l ( <. X , v >. .x. u ) k ) e. ( 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 >. .x. u ) = ( <. X , Y >. .x. u ) )
50 49 oveqd 
 |-  ( v = Y -> ( l ( <. X , v >. .x. u ) k ) = ( l ( <. X , Y >. .x. u ) k ) )
51 50 eleq1d 
 |-  ( v = Y -> ( ( l ( <. X , v >. .x. u ) k ) e. ( X H u ) <-> ( l ( <. X , Y >. .x. u ) k ) e. ( X H u ) ) )
52 47 51 raleqbidv 
 |-  ( v = Y -> ( A. l e. ( v H u ) ( l ( <. X , v >. .x. u ) k ) e. ( X H u ) <-> A. l e. ( Y H u ) ( l ( <. X , Y >. .x. u ) k ) e. ( X H u ) ) )
53 46 52 raleqbidv 
 |-  ( v = Y -> ( A. k e. ( X H v ) A. l e. ( v H u ) ( l ( <. X , v >. .x. u ) k ) e. ( X H u ) <-> A. k e. ( X H Y ) A. l e. ( Y H u ) ( l ( <. X , Y >. .x. u ) k ) e. ( X H u ) ) )
54 oveq2 
 |-  ( u = Z -> ( Y H u ) = ( Y H Z ) )
55 oveq2 
 |-  ( u = Z -> ( <. X , Y >. .x. u ) = ( <. X , Y >. .x. Z ) )
56 55 oveqd 
 |-  ( u = Z -> ( l ( <. X , Y >. .x. u ) k ) = ( l ( <. X , Y >. .x. Z ) k ) )
57 oveq2 
 |-  ( u = Z -> ( X H u ) = ( X H Z ) )
58 56 57 eleq12d 
 |-  ( u = Z -> ( ( l ( <. X , Y >. .x. u ) k ) e. ( X H u ) <-> ( l ( <. X , Y >. .x. Z ) k ) e. ( X H Z ) ) )
59 54 58 raleqbidv 
 |-  ( u = Z -> ( A. l e. ( Y H u ) ( l ( <. X , Y >. .x. u ) k ) e. ( X H u ) <-> A. l e. ( Y H Z ) ( l ( <. X , Y >. .x. Z ) k ) e. ( X H Z ) ) )
60 59 ralbidv 
 |-  ( u = Z -> ( A. k e. ( X H Y ) A. l e. ( Y H u ) ( l ( <. X , Y >. .x. u ) k ) e. ( X H u ) <-> A. k e. ( X H Y ) A. l e. ( Y H Z ) ( l ( <. X , Y >. .x. Z ) k ) e. ( X H Z ) ) )
61 45 53 60 rspc3v 
 |-  ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( A. w e. B A. v e. B A. u e. B A. k e. ( w H v ) A. l e. ( v H u ) ( l ( <. w , v >. .x. u ) k ) e. ( w H u ) -> A. k e. ( X H Y ) A. l e. ( Y H Z ) ( l ( <. X , Y >. .x. Z ) k ) e. ( X H Z ) ) )
62 1 2 3 61 syl3anc 
 |-  ( ph -> ( A. w e. B A. v e. B A. u e. B A. k e. ( w H v ) A. l e. ( v H u ) ( l ( <. w , v >. .x. u ) k ) e. ( w H u ) -> A. k e. ( X H Y ) A. l e. ( Y H Z ) ( l ( <. X , Y >. .x. Z ) k ) e. ( X H Z ) ) )
63 37 62 mpd 
 |-  ( ph -> A. k e. ( X H Y ) A. l e. ( Y H Z ) ( l ( <. X , Y >. .x. Z ) k ) e. ( X H Z ) )
64 oveq2 
 |-  ( k = F -> ( l ( <. X , Y >. .x. Z ) k ) = ( l ( <. X , Y >. .x. Z ) F ) )
65 64 eleq1d 
 |-  ( k = F -> ( ( l ( <. X , Y >. .x. Z ) k ) e. ( X H Z ) <-> ( l ( <. X , Y >. .x. Z ) F ) e. ( X H Z ) ) )
66 oveq1 
 |-  ( l = G -> ( l ( <. X , Y >. .x. Z ) F ) = ( G ( <. X , Y >. .x. Z ) F ) )
67 66 eleq1d 
 |-  ( l = G -> ( ( l ( <. X , Y >. .x. Z ) F ) e. ( X H Z ) <-> ( G ( <. X , Y >. .x. Z ) F ) e. ( X H Z ) ) )
68 65 67 rspc2v 
 |-  ( ( F e. ( X H Y ) /\ G e. ( Y H Z ) ) -> ( A. k e. ( X H Y ) A. l e. ( Y H Z ) ( l ( <. X , Y >. .x. Z ) k ) e. ( X H Z ) -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X H Z ) ) )
69 4 5 68 syl2anc 
 |-  ( ph -> ( A. k e. ( X H Y ) A. l e. ( Y H Z ) ( l ( <. X , Y >. .x. Z ) k ) e. ( X H Z ) -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X H Z ) ) )
70 63 69 mpd 
 |-  ( ph -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X H Z ) )