Nuprl - Proof: graph-isomorphic inversion 1 1

(3steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc

1. G: Graph
2. H: Graph
3. vmap: Vertices(G)Vertices(H)
4. emap: Edges(G)Edges(H)
5. Bij(Vertices(G); Vertices(H); vmap)
6. Bij(Edges(G); Edges(H); emap)
7. (vmap,vmap) o Incidence(G) = Incidence(H) o emap
8. g1: Edges(H)Edges(G)
9. Bij(Edges(H); Edges(G); g1)
10. g1 o emap = Id
11. emap o g1 = Id
12. g: Vertices(H)Vertices(G)
13. Bij(Vertices(H); Vertices(G); g)
14. g o vmap = Id
15. vmap o g = Id

(g,g) o Incidence(H) = Incidence(G) o g1

By: RW (AddrC [2] (RevLemmaC Thm* f:(AB). f o Id = f)) 0 THEN SubstFor Id 0 THEN RWO Thm* f:(AB), g:(BC), h:(CD). h o (g o f) = (h o g) o f AD 0 THEN RWO "comp2_comp_assoc < " 0 THEN SubstFor (Incidence(H) o emap) 0 THEN RWO Thm* h:(A'A1A2), g1:(A1B), g2:(A2C), f1:(BB'), f2:(CC'). (f1,f2) o (g1,g2) o h = (f1 o g1,f2 o g2) o h 0 THEN SubstFor (g o vmap) 0 THEN RWO Thm* g:(ABC). (Id,Id) o g = g 0

Generated subgoals:

None

About:

(3steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc